Proof 01. 1 ⊢ function f, hypo. 02. 2 ⊢ function g, hypo. 03. 3 ⊢ dom f ∩ dom g = ∅, hypo. 04. 4 ⊢ (x, y1) ∈ f ∪ g, hypo. 05. 5 ⊢ (x, y2) ∈ f ∪ g, hypo. 06. 4 ⊢ (x, y1) ∈ f ∨ (x, y1) ∈ g, union_elim 4. 07. 5 ⊢ (x, y2) ∈ f ∨ (x, y2) ∈ g, union_elim 5. 08. 4 ⊢ x ∈ dom (f ∪ g), dom_intro 4. 09. ⊢ dom (f ∪ g) = dom f ∪ dom g, dom_union. 10. 4 ⊢ x ∈ dom f ∪ dom g, eq_subst 9 8, P u ↔ x ∈ u. 11. 11 ⊢ (x, y1) ∈ f, hypo. 12. 12 ⊢ (x, y2) ∈ f, hypo. 13. 1, 11, 12 ⊢ y1 = y2, fn_unique_value 1 11 12. 14. 14 ⊢ (x, y2) ∈ g, hypo. 15. 11 ⊢ x ∈ dom f, dom_intro 11. 16. 14 ⊢ x ∈ dom g, dom_intro 14. 17. 3, 11, 14 ⊢ ⊥, disjoint_property 3 15 16. 18. 3, 11, 14 ⊢ y1 = y2, efq 17. 19. 1, 3, 5, 11 ⊢ y1 = y2, disj_elim 7 13 18. 20. 20 ⊢ (x, y1) ∈ g, hypo. 21. 21 ⊢ (x, y2) ∈ f, hypo. 22. 21 ⊢ x ∈ dom f, dom_intro 21. 23. 20 ⊢ x ∈ dom g, dom_intro 20. 24. 3, 20, 21 ⊢ ⊥, disjoint_property 3 22 23. 25. 3, 20, 21 ⊢ y1 = y2, efq 24. 26. 26 ⊢ (x, y2) ∈ g, hypo. 27. 2, 20, 26 ⊢ y1 = y2, fn_unique_value 2 20 26. 28. 2, 3, 5, 20 ⊢ y1 = y2, disj_elim 7 25 27. 29. 1, 2, 3, 4, 5 ⊢ y1 = y2, disj_elim 6 19 28. 30. 1, 2, 3 ⊢ (x, y1) ∈ f ∪ g → (x, y2) ∈ f ∪ g → y1 = y2, subj_intro_ii 29. 31. 1, 2, 3 ⊢ ∀y2. (x, y1) ∈ f ∪ g → (x, y2) ∈ f ∪ g → y1 = y2, uq_intro 30. 32. 1, 2, 3 ⊢ ∀y1. ∀y2. (x, y1) ∈ f ∪ g → (x, y2) ∈ f ∪ g → y1 = y2, uq_intro 31. 33. 1, 2, 3 ⊢ ∀x. ∀y1. ∀y2. (x, y1) ∈ f ∪ g → (x, y2) ∈ f ∪ g → y1 = y2, uq_intro 32. 34. 1 ⊢ relation f, fn_is_rel 1. 35. 2 ⊢ relation g, fn_is_rel 2. 36. 1, 2 ⊢ relation (f ∪ g), relation_union 34 35. 37. 1, 2, 3 ⊢ function (f ∪ g), function_intro 36 33. function_union. ⊢ function f → function g → dom f ∩ dom g = ∅ → function (f ∪ g), subj_intro_iii 37.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.