Proof 01. 1 ⊢ y ∈ rng (R ∪ Q), hypo. 02. 1 ⊢ ∃x. (x, y) ∈ R ∪ Q, rng_elim 1. 03. 3 ⊢ (x, y) ∈ R ∪ Q, hypo. 04. 3 ⊢ (x, y) ∈ R ∨ (x, y) ∈ Q, union_elim 3. 05. 5 ⊢ (x, y) ∈ R, hypo. 06. 5 ⊢ y ∈ rng R, rng_intro 5. 07. 5 ⊢ y ∈ rng R ∪ rng Q, union_introl 6. 08. 8 ⊢ (x, y) ∈ Q, hypo. 09. 8 ⊢ y ∈ rng Q, rng_intro 8. 10. 8 ⊢ y ∈ rng R ∪ rng Q, union_intror 9. 11. 3 ⊢ y ∈ rng R ∪ rng Q, disj_elim 4 7 10. 12. 1 ⊢ y ∈ rng R ∪ rng Q, ex_elim 2 11. 13. ⊢ y ∈ rng (R ∪ Q) → y ∈ rng R ∪ rng Q, subj_intro 12. 14. 14 ⊢ y ∈ rng R ∪ rng Q, hypo. 15. 14 ⊢ y ∈ rng R ∨ y ∈ rng Q, union_elim 14. 16. 16 ⊢ y ∈ rng R, hypo. 17. 16 ⊢ ∃x. (x, y) ∈ R, rng_elim 16. 18. 18 ⊢ (x, y) ∈ R, hypo. 19. 18 ⊢ (x, y) ∈ R ∪ Q, union_introl 18. 20. 18 ⊢ y ∈ rng (R ∪ Q), rng_intro 19. 21. 16 ⊢ y ∈ rng (R ∪ Q), ex_elim 17 20. 22. 22 ⊢ y ∈ rng Q, hypo. 23. 22 ⊢ ∃x. (x, y) ∈ Q, rng_elim 22. 24. 24 ⊢ (x, y) ∈ Q, hypo. 25. 24 ⊢ (x, y) ∈ R ∪ Q, union_intror 24. 26. 24 ⊢ y ∈ rng (R ∪ Q), rng_intro 25. 27. 22 ⊢ y ∈ rng (R ∪ Q), ex_elim 23 26. 28. 14 ⊢ y ∈ rng (R ∪ Q), disj_elim 15 21 27. 29. ⊢ y ∈ rng R ∪ rng Q → y ∈ rng (R ∪ Q), subj_intro 28. 30. ⊢ y ∈ rng (R ∪ Q) ↔ y ∈ rng R ∪ rng Q, bij_intro 13 29. 31. ⊢ ∀y. y ∈ rng (R ∪ Q) ↔ y ∈ rng R ∪ rng Q, uq_intro 30. rng_union. ⊢ rng (R ∪ Q) = rng R ∪ rng Q, ext 31.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.