Proof 01. 1 ⊢ y ∈ img (R ∪ Q) A, hypo. 02. 1 ⊢ ∃x. x in A and (x, y) ∈ R ∪ Q, img_elim 1. 03. 3 ⊢ x in A and (x, y) ∈ R ∪ Q, hypo. 04. 3 |- x in A, conj_eliml 3. 05. 3 |- (x, y) in R cup Q, conj_elimr 3. 06. 3 ⊢ (x, y) ∈ R ∨ (x, y) ∈ Q, union_elim 5. 07. 7 ⊢ (x, y) ∈ R, hypo. 08. 3, 7 ⊢ y ∈ img R A, img_intro 4 7. 09. 3, 7 ⊢ y ∈ img R A ∪ img Q A, union_introl 8. 10. 10 ⊢ (x, y) ∈ Q, hypo. 11. 3, 10 ⊢ y ∈ img Q A, img_intro 4 10. 12. 3, 10 ⊢ y ∈ img R A ∪ img Q A, union_intror 11. 13. 3 ⊢ y ∈ img R A ∪ img Q A, disj_elim 6 9 12. 14. 1 ⊢ y ∈ img R A ∪ img Q A, ex_elim 2 13. 15. ⊢ y ∈ img (R ∪ Q) A → y ∈ img R A ∪ img Q A, subj_intro 14. 16. 16 ⊢ y ∈ img R A ∪ img Q A, hypo. 17. 16 ⊢ y ∈ img R A ∨ y ∈ img Q A, union_elim 16. 18. 18 ⊢ y ∈ img R A, hypo. 19. 18 ⊢ ∃x. x in A and (x, y) ∈ R, img_elim 18. 20. 20 ⊢ x in A and (x, y) ∈ R, hypo. 21. 20 |- x in A, conj_eliml 20. 22. 20 |- (x, y) in R, conj_elimr 20. 23. 20 ⊢ (x, y) ∈ R ∪ Q, union_introl 22. 24. 20 ⊢ y ∈ img (R ∪ Q) A, img_intro 21 23. 25. 18 ⊢ y ∈ img (R ∪ Q) A, ex_elim 19 24. 26. 26 ⊢ y ∈ img Q A, hypo. 27. 26 ⊢ ∃x. x in A and (x, y) ∈ Q, img_elim 26. 28. 28 ⊢ x in A and (x, y) ∈ Q, hypo. 29. 28 |- x in A, conj_eliml 28. 30. 28 |- (x, y) in Q, conj_elimr 28. 31. 28 ⊢ (x, y) ∈ R ∪ Q, union_intror 30. 32. 28 ⊢ y ∈ img (R ∪ Q) A, img_intro 29 31. 33. 26 ⊢ y ∈ img (R ∪ Q) A, ex_elim 27 32. 34. 16 ⊢ y ∈ img (R ∪ Q) A, disj_elim 17 25 33. 35. ⊢ y ∈ img R A ∪ img Q A → y ∈ img (R ∪ Q) A, subj_intro 34. 36. ⊢ y ∈ img (R ∪ Q) A ↔ y ∈ img R A ∪ img Q A, bij_intro 15 35. 37. ⊢ ∀y. y ∈ img (R ∪ Q) A ↔ y ∈ img R A ∪ img Q A, uq_intro 36. img_union. ⊢ img (R ∪ Q) A = img R A ∪ img Q A, ext 37.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.