Proof 01. 1 ⊢ x ∈ dom (R ∪ Q), hypo. 02. 1 ⊢ ∃y. (x, y) ∈ R ∪ Q, dom_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 ⊢ x ∈ dom R, dom_intro 5. 07. 5 ⊢ x ∈ dom R ∪ dom Q, union_introl 6. 08. 8 ⊢ (x, y) ∈ Q, hypo. 09. 8 ⊢ x ∈ dom Q, dom_intro 8. 10. 8 ⊢ x ∈ dom R ∪ dom Q, union_intror 9. 11. 3 ⊢ x ∈ dom R ∪ dom Q, disj_elim 4 7 10. 12. 1 ⊢ x ∈ dom R ∪ dom Q, ex_elim 2 11. 13. ⊢ x ∈ dom (R ∪ Q) → x ∈ dom R ∪ dom Q, subj_intro 12. 14. 14 ⊢ x ∈ dom R ∪ dom Q, hypo. 15. 14 ⊢ x ∈ dom R ∨ x ∈ dom Q, union_elim 14. 16. 16 ⊢ x ∈ dom R, hypo. 17. 16 ⊢ ∃y. (x, y) ∈ R, dom_elim 16. 18. 18 ⊢ (x, y) ∈ R, hypo. 19. 18 ⊢ (x, y) ∈ R ∪ Q, union_introl 18. 20. 18 ⊢ x ∈ dom (R ∪ Q), dom_intro 19. 21. 16 ⊢ x ∈ dom (R ∪ Q), ex_elim 17 20. 22. 22 ⊢ x ∈ dom Q, hypo. 23. 22 ⊢ ∃y. (x, y) ∈ Q, dom_elim 22. 24. 24 ⊢ (x, y) ∈ Q, hypo. 25. 24 ⊢ (x, y) ∈ R ∪ Q, union_intror 24. 26. 24 ⊢ x ∈ dom (R ∪ Q), dom_intro 25. 27. 22 ⊢ x ∈ dom (R ∪ Q), ex_elim 23 26. 28. 14 ⊢ x ∈ dom (R ∪ Q), disj_elim 15 21 27. 29. ⊢ x ∈ dom R ∪ dom Q → x ∈ dom (R ∪ Q), subj_intro 28. 30. ⊢ x ∈ dom (R ∪ Q) ↔ x ∈ dom R ∪ dom Q, bij_intro 13 29. 31. ⊢ ∀x. x ∈ dom (R ∪ Q) ↔ x ∈ dom R ∪ dom Q, uq_intro 30. dom_union. ⊢ dom (R ∪ Q) = dom R ∪ dom Q, ext 31.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.