Proof of Theorem uhgruhgra
Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | | eqid 2610 |
. . . . 5
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
3 | 1, 2 | uhgrf 25728 |
. . . 4
⊢ (𝐺 ∈ UHGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖
{∅})) |
4 | 3 | 3ad2ant1 1075 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = (Vtx‘𝐺) ∧ 𝐸 = (iEdg‘𝐺)) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫 (Vtx‘𝐺) ∖
{∅})) |
5 | | simp3 1056 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = (Vtx‘𝐺) ∧ 𝐸 = (iEdg‘𝐺)) → 𝐸 = (iEdg‘𝐺)) |
6 | 5 | dmeqd 5248 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = (Vtx‘𝐺) ∧ 𝐸 = (iEdg‘𝐺)) → dom 𝐸 = dom (iEdg‘𝐺)) |
7 | | pweq 4111 |
. . . . . 6
⊢ (𝑉 = (Vtx‘𝐺) → 𝒫 𝑉 = 𝒫 (Vtx‘𝐺)) |
8 | 7 | 3ad2ant2 1076 |
. . . . 5
⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = (Vtx‘𝐺) ∧ 𝐸 = (iEdg‘𝐺)) → 𝒫 𝑉 = 𝒫 (Vtx‘𝐺)) |
9 | 8 | difeq1d 3689 |
. . . 4
⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = (Vtx‘𝐺) ∧ 𝐸 = (iEdg‘𝐺)) → (𝒫 𝑉 ∖ {∅}) = (𝒫
(Vtx‘𝐺) ∖
{∅})) |
10 | 5, 6, 9 | feq123d 5947 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = (Vtx‘𝐺) ∧ 𝐸 = (iEdg‘𝐺)) → (𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}) ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶(𝒫
(Vtx‘𝐺) ∖
{∅}))) |
11 | 4, 10 | mpbird 246 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = (Vtx‘𝐺) ∧ 𝐸 = (iEdg‘𝐺)) → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})) |
12 | | fvex 6113 |
. . . . . 6
⊢
(Vtx‘𝐺) ∈
V |
13 | | eleq1 2676 |
. . . . . 6
⊢ (𝑉 = (Vtx‘𝐺) → (𝑉 ∈ V ↔ (Vtx‘𝐺) ∈ V)) |
14 | 12, 13 | mpbiri 247 |
. . . . 5
⊢ (𝑉 = (Vtx‘𝐺) → 𝑉 ∈ V) |
15 | | fvex 6113 |
. . . . . 6
⊢
(iEdg‘𝐺)
∈ V |
16 | | eleq1 2676 |
. . . . . 6
⊢ (𝐸 = (iEdg‘𝐺) → (𝐸 ∈ V ↔ (iEdg‘𝐺) ∈ V)) |
17 | 15, 16 | mpbiri 247 |
. . . . 5
⊢ (𝐸 = (iEdg‘𝐺) → 𝐸 ∈ V) |
18 | 14, 17 | anim12i 588 |
. . . 4
⊢ ((𝑉 = (Vtx‘𝐺) ∧ 𝐸 = (iEdg‘𝐺)) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
19 | 18 | 3adant1 1072 |
. . 3
⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = (Vtx‘𝐺) ∧ 𝐸 = (iEdg‘𝐺)) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
20 | | isuhgra 25827 |
. . 3
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 UHGrph 𝐸 ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) |
21 | 19, 20 | syl 17 |
. 2
⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = (Vtx‘𝐺) ∧ 𝐸 = (iEdg‘𝐺)) → (𝑉 UHGrph 𝐸 ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) |
22 | 11, 21 | mpbird 246 |
1
⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = (Vtx‘𝐺) ∧ 𝐸 = (iEdg‘𝐺)) → 𝑉 UHGrph 𝐸) |