Proof of Theorem uhgraun
Step | Hyp | Ref
| Expression |
1 | | uhgraun.ge |
. . . . . 6
⊢ (𝜑 → 𝑉 UHGrph 𝐸) |
2 | | uhgraf 25828 |
. . . . . 6
⊢ (𝑉 UHGrph 𝐸 → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})) |
4 | | uhgraun.e |
. . . . 5
⊢ (𝜑 → 𝐸 Fn 𝐴) |
5 | | fndm 5904 |
. . . . . . 7
⊢ (𝐸 Fn 𝐴 → dom 𝐸 = 𝐴) |
6 | 5 | feq2d 5944 |
. . . . . 6
⊢ (𝐸 Fn 𝐴 → (𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}) ↔ 𝐸:𝐴⟶(𝒫 𝑉 ∖ {∅}))) |
7 | 6 | biimpac 502 |
. . . . 5
⊢ ((𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}) ∧ 𝐸 Fn 𝐴) → 𝐸:𝐴⟶(𝒫 𝑉 ∖ {∅})) |
8 | 3, 4, 7 | syl2anc 691 |
. . . 4
⊢ (𝜑 → 𝐸:𝐴⟶(𝒫 𝑉 ∖ {∅})) |
9 | | uhgraun.gf |
. . . . . 6
⊢ (𝜑 → 𝑉 UHGrph 𝐹) |
10 | | uhgraf 25828 |
. . . . . 6
⊢ (𝑉 UHGrph 𝐹 → 𝐹:dom 𝐹⟶(𝒫 𝑉 ∖ {∅})) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹:dom 𝐹⟶(𝒫 𝑉 ∖ {∅})) |
12 | | uhgraun.f |
. . . . 5
⊢ (𝜑 → 𝐹 Fn 𝐵) |
13 | | fndm 5904 |
. . . . . . 7
⊢ (𝐹 Fn 𝐵 → dom 𝐹 = 𝐵) |
14 | 13 | feq2d 5944 |
. . . . . 6
⊢ (𝐹 Fn 𝐵 → (𝐹:dom 𝐹⟶(𝒫 𝑉 ∖ {∅}) ↔ 𝐹:𝐵⟶(𝒫 𝑉 ∖ {∅}))) |
15 | 14 | biimpac 502 |
. . . . 5
⊢ ((𝐹:dom 𝐹⟶(𝒫 𝑉 ∖ {∅}) ∧ 𝐹 Fn 𝐵) → 𝐹:𝐵⟶(𝒫 𝑉 ∖ {∅})) |
16 | 11, 12, 15 | syl2anc 691 |
. . . 4
⊢ (𝜑 → 𝐹:𝐵⟶(𝒫 𝑉 ∖ {∅})) |
17 | | uhgraun.i |
. . . 4
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) |
18 | | fun2 5980 |
. . . 4
⊢ (((𝐸:𝐴⟶(𝒫 𝑉 ∖ {∅}) ∧ 𝐹:𝐵⟶(𝒫 𝑉 ∖ {∅})) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐸 ∪ 𝐹):(𝐴 ∪ 𝐵)⟶(𝒫 𝑉 ∖ {∅})) |
19 | 8, 16, 17, 18 | syl21anc 1317 |
. . 3
⊢ (𝜑 → (𝐸 ∪ 𝐹):(𝐴 ∪ 𝐵)⟶(𝒫 𝑉 ∖ {∅})) |
20 | | fdm 5964 |
. . . . 5
⊢ ((𝐸 ∪ 𝐹):(𝐴 ∪ 𝐵)⟶(𝒫 𝑉 ∖ {∅}) → dom (𝐸 ∪ 𝐹) = (𝐴 ∪ 𝐵)) |
21 | 19, 20 | syl 17 |
. . . 4
⊢ (𝜑 → dom (𝐸 ∪ 𝐹) = (𝐴 ∪ 𝐵)) |
22 | 21 | feq2d 5944 |
. . 3
⊢ (𝜑 → ((𝐸 ∪ 𝐹):dom (𝐸 ∪ 𝐹)⟶(𝒫 𝑉 ∖ {∅}) ↔ (𝐸 ∪ 𝐹):(𝐴 ∪ 𝐵)⟶(𝒫 𝑉 ∖ {∅}))) |
23 | 19, 22 | mpbird 246 |
. 2
⊢ (𝜑 → (𝐸 ∪ 𝐹):dom (𝐸 ∪ 𝐹)⟶(𝒫 𝑉 ∖ {∅})) |
24 | | reluhgra 25823 |
. . . 4
⊢ Rel
UHGrph |
25 | | releldm 5279 |
. . . 4
⊢ ((Rel
UHGrph ∧ 𝑉 UHGrph 𝐸) → 𝑉 ∈ dom UHGrph ) |
26 | 24, 1, 25 | sylancr 694 |
. . 3
⊢ (𝜑 → 𝑉 ∈ dom UHGrph ) |
27 | | uhgrav 25825 |
. . . . . 6
⊢ (𝑉 UHGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
28 | 27 | simprd 478 |
. . . . 5
⊢ (𝑉 UHGrph 𝐸 → 𝐸 ∈ V) |
29 | 1, 28 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ V) |
30 | | uhgrav 25825 |
. . . . . 6
⊢ (𝑉 UHGrph 𝐹 → (𝑉 ∈ V ∧ 𝐹 ∈ V)) |
31 | 30 | simprd 478 |
. . . . 5
⊢ (𝑉 UHGrph 𝐹 → 𝐹 ∈ V) |
32 | 9, 31 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ V) |
33 | | unexg 6857 |
. . . 4
⊢ ((𝐸 ∈ V ∧ 𝐹 ∈ V) → (𝐸 ∪ 𝐹) ∈ V) |
34 | 29, 32, 33 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐸 ∪ 𝐹) ∈ V) |
35 | | isuhgra 25827 |
. . 3
⊢ ((𝑉 ∈ dom UHGrph ∧ (𝐸 ∪ 𝐹) ∈ V) → (𝑉 UHGrph (𝐸 ∪ 𝐹) ↔ (𝐸 ∪ 𝐹):dom (𝐸 ∪ 𝐹)⟶(𝒫 𝑉 ∖ {∅}))) |
36 | 26, 34, 35 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝑉 UHGrph (𝐸 ∪ 𝐹) ↔ (𝐸 ∪ 𝐹):dom (𝐸 ∪ 𝐹)⟶(𝒫 𝑉 ∖ {∅}))) |
37 | 23, 36 | mpbird 246 |
1
⊢ (𝜑 → 𝑉 UHGrph (𝐸 ∪ 𝐹)) |