Step | Hyp | Ref
| Expression |
1 | | funrel 4862 |
. . . . 5
⊢ (Fun
𝐹 → Rel 𝐹) |
2 | | funrel 4862 |
. . . . 5
⊢ (Fun
𝐺 → Rel 𝐺) |
3 | 1, 2 | anim12i 321 |
. . . 4
⊢ ((Fun
𝐹 ∧ Fun 𝐺) → (Rel 𝐹 ∧ Rel
𝐺)) |
4 | | relun 4397 |
. . . 4
⊢ (Rel
(𝐹 ∪ 𝐺) ↔ (Rel 𝐹 ∧ Rel
𝐺)) |
5 | 3, 4 | sylibr 137 |
. . 3
⊢ ((Fun
𝐹 ∧ Fun 𝐺) → Rel (𝐹 ∪ 𝐺)) |
6 | 5 | adantr 261 |
. 2
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom
𝐹 ∩ dom 𝐺) = ∅) → Rel (𝐹 ∪ 𝐺)) |
7 | | elun 3078 |
. . . . . . . 8
⊢
(〈x, y〉 ∈ (𝐹 ∪ 𝐺) ↔ (〈x, y〉 ∈ 𝐹 ∨
〈x, y〉 ∈ 𝐺)) |
8 | | elun 3078 |
. . . . . . . 8
⊢
(〈x, z〉 ∈ (𝐹 ∪ 𝐺) ↔ (〈x, z〉 ∈ 𝐹 ∨
〈x, z〉 ∈ 𝐺)) |
9 | 7, 8 | anbi12i 433 |
. . . . . . 7
⊢
((〈x, y〉 ∈ (𝐹 ∪ 𝐺) ∧
〈x, z〉 ∈ (𝐹 ∪ 𝐺)) ↔ ((〈x, y〉 ∈ 𝐹 ∨
〈x, y〉 ∈ 𝐺) ∧ (〈x,
z〉 ∈
𝐹
∨ 〈x, z〉 ∈ 𝐺))) |
10 | | anddi 733 |
. . . . . . 7
⊢
(((〈x, y〉 ∈ 𝐹
∨ 〈x, y〉 ∈ 𝐺) ∧ (〈x,
z〉 ∈
𝐹
∨ 〈x, z〉 ∈ 𝐺)) ↔ (((〈x, y〉 ∈ 𝐹 ∧
〈x, z〉 ∈ 𝐹)
∨ (〈x, y〉 ∈ 𝐹 ∧ 〈x,
z〉 ∈
𝐺))
∨ ((〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐹)
∨ (〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐺)))) |
11 | 9, 10 | bitri 173 |
. . . . . 6
⊢
((〈x, y〉 ∈ (𝐹 ∪ 𝐺) ∧
〈x, z〉 ∈ (𝐹 ∪ 𝐺)) ↔ (((〈x, y〉 ∈ 𝐹 ∧
〈x, z〉 ∈ 𝐹)
∨ (〈x, y〉 ∈ 𝐹 ∧ 〈x,
z〉 ∈
𝐺))
∨ ((〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐹)
∨ (〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐺)))) |
12 | | disj1 3264 |
. . . . . . . . . . . . 13
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ ↔ ∀x(x ∈ dom 𝐹 → ¬ x ∈ dom 𝐺)) |
13 | 12 | biimpi 113 |
. . . . . . . . . . . 12
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → ∀x(x ∈ dom 𝐹 → ¬ x ∈ dom 𝐺)) |
14 | 13 | 19.21bi 1447 |
. . . . . . . . . . 11
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → (x ∈ dom 𝐹 → ¬ x ∈ dom 𝐺)) |
15 | | imnan 623 |
. . . . . . . . . . 11
⊢
((x ∈ dom 𝐹 → ¬ x ∈ dom 𝐺) ↔ ¬ (x ∈ dom 𝐹 ∧ x ∈ dom 𝐺)) |
16 | 14, 15 | sylib 127 |
. . . . . . . . . 10
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → ¬
(x ∈ dom
𝐹 ∧ x ∈ dom 𝐺)) |
17 | | vex 2554 |
. . . . . . . . . . . 12
⊢ x ∈
V |
18 | | vex 2554 |
. . . . . . . . . . . 12
⊢ y ∈
V |
19 | 17, 18 | opeldm 4481 |
. . . . . . . . . . 11
⊢
(〈x, y〉 ∈ 𝐹 → x ∈ dom 𝐹) |
20 | | vex 2554 |
. . . . . . . . . . . 12
⊢ z ∈
V |
21 | 17, 20 | opeldm 4481 |
. . . . . . . . . . 11
⊢
(〈x, z〉 ∈ 𝐺 → x ∈ dom 𝐺) |
22 | 19, 21 | anim12i 321 |
. . . . . . . . . 10
⊢
((〈x, y〉 ∈ 𝐹 ∧ 〈x,
z〉 ∈
𝐺) → (x ∈ dom 𝐹 ∧ x ∈ dom 𝐺)) |
23 | 16, 22 | nsyl 558 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → ¬
(〈x, y〉 ∈ 𝐹 ∧ 〈x,
z〉 ∈
𝐺)) |
24 | | orel2 644 |
. . . . . . . . 9
⊢ (¬
(〈x, y〉 ∈ 𝐹 ∧ 〈x,
z〉 ∈
𝐺) → (((〈x, y〉 ∈ 𝐹 ∧
〈x, z〉 ∈ 𝐹)
∨ (〈x, y〉 ∈ 𝐹 ∧ 〈x,
z〉 ∈
𝐺)) → (〈x, y〉 ∈ 𝐹 ∧
〈x, z〉 ∈ 𝐹))) |
25 | 23, 24 | syl 14 |
. . . . . . . 8
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ →
(((〈x, y〉 ∈ 𝐹 ∧ 〈x,
z〉 ∈
𝐹)
∨ (〈x, y〉 ∈ 𝐹 ∧ 〈x,
z〉 ∈
𝐺)) → (〈x, y〉 ∈ 𝐹 ∧
〈x, z〉 ∈ 𝐹))) |
26 | 14 | con2d 554 |
. . . . . . . . . . 11
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → (x ∈ dom 𝐺 → ¬ x ∈ dom 𝐹)) |
27 | | imnan 623 |
. . . . . . . . . . 11
⊢
((x ∈ dom 𝐺 → ¬ x ∈ dom 𝐹) ↔ ¬ (x ∈ dom 𝐺 ∧ x ∈ dom 𝐹)) |
28 | 26, 27 | sylib 127 |
. . . . . . . . . 10
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → ¬
(x ∈ dom
𝐺 ∧ x ∈ dom 𝐹)) |
29 | 17, 18 | opeldm 4481 |
. . . . . . . . . . 11
⊢
(〈x, y〉 ∈ 𝐺 → x ∈ dom 𝐺) |
30 | 17, 20 | opeldm 4481 |
. . . . . . . . . . 11
⊢
(〈x, z〉 ∈ 𝐹 → x ∈ dom 𝐹) |
31 | 29, 30 | anim12i 321 |
. . . . . . . . . 10
⊢
((〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐹) → (x ∈ dom 𝐺 ∧ x ∈ dom 𝐹)) |
32 | 28, 31 | nsyl 558 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ → ¬
(〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐹)) |
33 | | orel1 643 |
. . . . . . . . 9
⊢ (¬
(〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐹) → (((〈x, y〉 ∈ 𝐺 ∧
〈x, z〉 ∈ 𝐹)
∨ (〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐺)) → (〈x, y〉 ∈ 𝐺 ∧
〈x, z〉 ∈ 𝐺))) |
34 | 32, 33 | syl 14 |
. . . . . . . 8
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ →
(((〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐹)
∨ (〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐺)) → (〈x, y〉 ∈ 𝐺 ∧
〈x, z〉 ∈ 𝐺))) |
35 | 25, 34 | orim12d 699 |
. . . . . . 7
⊢ ((dom
𝐹 ∩ dom 𝐺) = ∅ →
((((〈x, y〉 ∈ 𝐹 ∧ 〈x,
z〉 ∈
𝐹)
∨ (〈x, y〉 ∈ 𝐹 ∧ 〈x,
z〉 ∈
𝐺))
∨ ((〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐹)
∨ (〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐺))) →
((〈x, y〉 ∈ 𝐹 ∧ 〈x,
z〉 ∈
𝐹)
∨ (〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐺)))) |
36 | 35 | adantl 262 |
. . . . . 6
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom
𝐹 ∩ dom 𝐺) = ∅) →
((((〈x, y〉 ∈ 𝐹 ∧ 〈x,
z〉 ∈
𝐹)
∨ (〈x, y〉 ∈ 𝐹 ∧ 〈x,
z〉 ∈
𝐺))
∨ ((〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐹)
∨ (〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐺))) →
((〈x, y〉 ∈ 𝐹 ∧ 〈x,
z〉 ∈
𝐹)
∨ (〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐺)))) |
37 | 11, 36 | syl5bi 141 |
. . . . 5
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom
𝐹 ∩ dom 𝐺) = ∅) →
((〈x, y〉 ∈ (𝐹 ∪ 𝐺) ∧
〈x, z〉 ∈ (𝐹 ∪ 𝐺)) → ((〈x, y〉 ∈ 𝐹 ∧
〈x, z〉 ∈ 𝐹)
∨ (〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐺)))) |
38 | | dffun4 4856 |
. . . . . . . . . 10
⊢ (Fun
𝐹 ↔ (Rel 𝐹 ∧ ∀x∀y∀z((〈x,
y〉 ∈
𝐹 ∧ 〈x,
z〉 ∈
𝐹) → y = z))) |
39 | 38 | simprbi 260 |
. . . . . . . . 9
⊢ (Fun
𝐹 → ∀x∀y∀z((〈x,
y〉 ∈
𝐹 ∧ 〈x,
z〉 ∈
𝐹) → y = z)) |
40 | 39 | 19.21bi 1447 |
. . . . . . . 8
⊢ (Fun
𝐹 → ∀y∀z((〈x,
y〉 ∈
𝐹 ∧ 〈x,
z〉 ∈
𝐹) → y = z)) |
41 | 40 | 19.21bbi 1448 |
. . . . . . 7
⊢ (Fun
𝐹 → ((〈x, y〉 ∈ 𝐹 ∧
〈x, z〉 ∈ 𝐹) → y = z)) |
42 | | dffun4 4856 |
. . . . . . . . . 10
⊢ (Fun
𝐺 ↔ (Rel 𝐺 ∧ ∀x∀y∀z((〈x,
y〉 ∈
𝐺 ∧ 〈x,
z〉 ∈
𝐺) → y = z))) |
43 | 42 | simprbi 260 |
. . . . . . . . 9
⊢ (Fun
𝐺 → ∀x∀y∀z((〈x,
y〉 ∈
𝐺 ∧ 〈x,
z〉 ∈
𝐺) → y = z)) |
44 | 43 | 19.21bi 1447 |
. . . . . . . 8
⊢ (Fun
𝐺 → ∀y∀z((〈x,
y〉 ∈
𝐺 ∧ 〈x,
z〉 ∈
𝐺) → y = z)) |
45 | 44 | 19.21bbi 1448 |
. . . . . . 7
⊢ (Fun
𝐺 → ((〈x, y〉 ∈ 𝐺 ∧
〈x, z〉 ∈ 𝐺) → y = z)) |
46 | 41, 45 | jaao 638 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ Fun 𝐺) → (((〈x, y〉 ∈ 𝐹 ∧
〈x, z〉 ∈ 𝐹)
∨ (〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐺)) → y = z)) |
47 | 46 | adantr 261 |
. . . . 5
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom
𝐹 ∩ dom 𝐺) = ∅) →
(((〈x, y〉 ∈ 𝐹 ∧ 〈x,
z〉 ∈
𝐹)
∨ (〈x, y〉 ∈ 𝐺 ∧ 〈x,
z〉 ∈
𝐺)) → y = z)) |
48 | 37, 47 | syld 40 |
. . . 4
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom
𝐹 ∩ dom 𝐺) = ∅) →
((〈x, y〉 ∈ (𝐹 ∪ 𝐺) ∧
〈x, z〉 ∈ (𝐹 ∪ 𝐺)) → y = z)) |
49 | 48 | alrimiv 1751 |
. . 3
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom
𝐹 ∩ dom 𝐺) = ∅) → ∀z((〈x,
y〉 ∈
(𝐹 ∪ 𝐺) ∧
〈x, z〉 ∈ (𝐹 ∪ 𝐺)) → y = z)) |
50 | 49 | alrimivv 1752 |
. 2
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom
𝐹 ∩ dom 𝐺) = ∅) → ∀x∀y∀z((〈x,
y〉 ∈
(𝐹 ∪ 𝐺) ∧
〈x, z〉 ∈ (𝐹 ∪ 𝐺)) → y = z)) |
51 | | dffun4 4856 |
. 2
⊢ (Fun
(𝐹 ∪ 𝐺) ↔ (Rel (𝐹 ∪ 𝐺) ∧ ∀x∀y∀z((〈x,
y〉 ∈
(𝐹 ∪ 𝐺) ∧
〈x, z〉 ∈ (𝐹 ∪ 𝐺)) → y = z))) |
52 | 6, 50, 51 | sylanbrc 394 |
1
⊢ (((Fun
𝐹 ∧ Fun 𝐺) ∧ (dom
𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹 ∪ 𝐺)) |