| Step | Hyp | Ref
| Expression |
| 1 | | funrel 6583 |
. . . . 5
⊢ (Fun
𝐹 → Rel 𝐹) |
| 2 | | funrel 6583 |
. . . . 5
⊢ (Fun
𝐺 → Rel 𝐺) |
| 3 | 1, 2 | anim12i 613 |
. . . 4
⊢ ((Fun
𝐹 ∧ Fun 𝐺) → (Rel 𝐹 ∧ Rel 𝐺)) |
| 4 | | relun 5821 |
. . . 4
⊢ (Rel
(𝐹 ∪ 𝐺) ↔ (Rel 𝐹 ∧ Rel 𝐺)) |
| 5 | 3, 4 | sylibr 234 |
. . 3
⊢ ((Fun
𝐹 ∧ Fun 𝐺) → Rel (𝐹 ∪ 𝐺)) |
| 6 | 5 | adantr 480 |
. 2
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Rel (𝐹 ∪ 𝐺)) |
| 7 | | elun 4153 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ (𝐹 ∪ 𝐺) ↔ (〈𝑥, 𝑦〉 ∈ 𝐹 ∨ 〈𝑥, 𝑦〉 ∈ 𝐺)) |
| 8 | | elun 4153 |
. . . . . . . 8
⊢
(〈𝑥, 𝑧〉 ∈ (𝐹 ∪ 𝐺) ↔ (〈𝑥, 𝑧〉 ∈ 𝐹 ∨ 〈𝑥, 𝑧〉 ∈ 𝐺)) |
| 9 | 7, 8 | anbi12i 628 |
. . . . . . 7
⊢
((〈𝑥, 𝑦〉 ∈ (𝐹 ∪ 𝐺) ∧ 〈𝑥, 𝑧〉 ∈ (𝐹 ∪ 𝐺)) ↔ ((〈𝑥, 𝑦〉 ∈ 𝐹 ∨ 〈𝑥, 𝑦〉 ∈ 𝐺) ∧ (〈𝑥, 𝑧〉 ∈ 𝐹 ∨ 〈𝑥, 𝑧〉 ∈ 𝐺))) |
| 10 | | anddi 1013 |
. . . . . . 7
⊢
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∨ 〈𝑥, 𝑦〉 ∈ 𝐺) ∧ (〈𝑥, 𝑧〉 ∈ 𝐹 ∨ 〈𝑥, 𝑧〉 ∈ 𝐺)) ↔ (((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) ∨ ((〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)))) |
| 11 | 9, 10 | bitri 275 |
. . . . . 6
⊢
((〈𝑥, 𝑦〉 ∈ (𝐹 ∪ 𝐺) ∧ 〈𝑥, 𝑧〉 ∈ (𝐹 ∪ 𝐺)) ↔ (((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) ∨ ((〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)))) |
| 12 | | disj1 4452 |
. . . . . . . . . . . . 13
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ ↔ ∀𝑥(𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺)) |
| 13 | 12 | biimpi 216 |
. . . . . . . . . . . 12
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → ∀𝑥(𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺)) |
| 14 | 13 | 19.21bi 2189 |
. . . . . . . . . . 11
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → (𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺)) |
| 15 | | imnan 399 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺) ↔ ¬ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺)) |
| 16 | 14, 15 | sylib 218 |
. . . . . . . . . 10
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → ¬ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺)) |
| 17 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
| 18 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
| 19 | 17, 18 | opeldm 5918 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ 𝐹 → 𝑥 ∈ dom 𝐹) |
| 20 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
| 21 | 17, 20 | opeldm 5918 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑧〉 ∈ 𝐺 → 𝑥 ∈ dom 𝐺) |
| 22 | 19, 21 | anim12i 613 |
. . . . . . . . . 10
⊢
((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) → (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺)) |
| 23 | 16, 22 | nsyl 140 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → ¬
(〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) |
| 24 | | orel2 891 |
. . . . . . . . 9
⊢ (¬
(〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) → (((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) → (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹))) |
| 25 | 23, 24 | syl 17 |
. . . . . . . 8
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ →
(((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) → (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹))) |
| 26 | 14 | con2d 134 |
. . . . . . . . . . 11
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → (𝑥 ∈ dom 𝐺 → ¬ 𝑥 ∈ dom 𝐹)) |
| 27 | | imnan 399 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ dom 𝐺 → ¬ 𝑥 ∈ dom 𝐹) ↔ ¬ (𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ dom 𝐹)) |
| 28 | 26, 27 | sylib 218 |
. . . . . . . . . 10
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → ¬ (𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ dom 𝐹)) |
| 29 | 17, 18 | opeldm 5918 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ 𝐺 → 𝑥 ∈ dom 𝐺) |
| 30 | 17, 20 | opeldm 5918 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑥 ∈ dom 𝐹) |
| 31 | 29, 30 | anim12i 613 |
. . . . . . . . . 10
⊢
((〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → (𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ dom 𝐹)) |
| 32 | 28, 31 | nsyl 140 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → ¬
(〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹)) |
| 33 | | orel1 889 |
. . . . . . . . 9
⊢ (¬
(〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → (((〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) → (〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺))) |
| 34 | 32, 33 | syl 17 |
. . . . . . . 8
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ →
(((〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) → (〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺))) |
| 35 | 25, 34 | orim12d 967 |
. . . . . . 7
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ →
((((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) ∨ ((〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺))) → ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)))) |
| 36 | 35 | adantl 481 |
. . . . . 6
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) ∨ ((〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺))) → ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)))) |
| 37 | 11, 36 | biimtrid 242 |
. . . . 5
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((〈𝑥, 𝑦〉 ∈ (𝐹 ∪ 𝐺) ∧ 〈𝑥, 𝑧〉 ∈ (𝐹 ∪ 𝐺)) → ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)))) |
| 38 | | dffun4 6577 |
. . . . . . . . . 10
⊢ (Fun
𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧))) |
| 39 | 38 | simprbi 496 |
. . . . . . . . 9
⊢ (Fun
𝐹 → ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
| 40 | 39 | 19.21bi 2189 |
. . . . . . . 8
⊢ (Fun
𝐹 → ∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
| 41 | 40 | 19.21bbi 2190 |
. . . . . . 7
⊢ (Fun
𝐹 → ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑦 = 𝑧)) |
| 42 | | dffun4 6577 |
. . . . . . . . . 10
⊢ (Fun
𝐺 ↔ (Rel 𝐺 ∧ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) → 𝑦 = 𝑧))) |
| 43 | 42 | simprbi 496 |
. . . . . . . . 9
⊢ (Fun
𝐺 → ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) → 𝑦 = 𝑧)) |
| 44 | 43 | 19.21bi 2189 |
. . . . . . . 8
⊢ (Fun
𝐺 → ∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) → 𝑦 = 𝑧)) |
| 45 | 44 | 19.21bbi 2190 |
. . . . . . 7
⊢ (Fun
𝐺 → ((〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) → 𝑦 = 𝑧)) |
| 46 | 41, 45 | jaao 957 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ Fun 𝐺) → (((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) → 𝑦 = 𝑧)) |
| 47 | 46 | adantr 480 |
. . . . 5
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → (((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) ∨ (〈𝑥, 𝑦〉 ∈ 𝐺 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) → 𝑦 = 𝑧)) |
| 48 | 37, 47 | syld 47 |
. . . 4
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((〈𝑥, 𝑦〉 ∈ (𝐹 ∪ 𝐺) ∧ 〈𝑥, 𝑧〉 ∈ (𝐹 ∪ 𝐺)) → 𝑦 = 𝑧)) |
| 49 | 48 | alrimiv 1927 |
. . 3
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀𝑧((〈𝑥, 𝑦〉 ∈ (𝐹 ∪ 𝐺) ∧ 〈𝑥, 𝑧〉 ∈ (𝐹 ∪ 𝐺)) → 𝑦 = 𝑧)) |
| 50 | 49 | alrimivv 1928 |
. 2
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ (𝐹 ∪ 𝐺) ∧ 〈𝑥, 𝑧〉 ∈ (𝐹 ∪ 𝐺)) → 𝑦 = 𝑧)) |
| 51 | | dffun4 6577 |
. 2
⊢ (Fun
(𝐹 ∪ 𝐺) ↔ (Rel (𝐹 ∪ 𝐺) ∧ ∀𝑥∀𝑦∀𝑧((〈𝑥, 𝑦〉 ∈ (𝐹 ∪ 𝐺) ∧ 〈𝑥, 𝑧〉 ∈ (𝐹 ∪ 𝐺)) → 𝑦 = 𝑧))) |
| 52 | 6, 50, 51 | sylanbrc 583 |
1
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹 ∪ 𝐺)) |