Step |
Hyp |
Ref |
Expression |
1 |
|
f0 |
⊢ ∅ : ∅ ⟶ ∅ |
2 |
|
dm0 |
⊢ dom ∅ = ∅ |
3 |
|
pw0 |
⊢ 𝒫 ∅ = { ∅ } |
4 |
3
|
difeq1i |
⊢ ( 𝒫 ∅ ∖ { ∅ } ) = ( { ∅ } ∖ { ∅ } ) |
5 |
|
difid |
⊢ ( { ∅ } ∖ { ∅ } ) = ∅ |
6 |
4 5
|
eqtri |
⊢ ( 𝒫 ∅ ∖ { ∅ } ) = ∅ |
7 |
2 6
|
feq23i |
⊢ ( ∅ : dom ∅ ⟶ ( 𝒫 ∅ ∖ { ∅ } ) ↔ ∅ : ∅ ⟶ ∅ ) |
8 |
1 7
|
mpbir |
⊢ ∅ : dom ∅ ⟶ ( 𝒫 ∅ ∖ { ∅ } ) |
9 |
|
0ex |
⊢ ∅ ∈ V |
10 |
|
vtxval0 |
⊢ ( Vtx ‘ ∅ ) = ∅ |
11 |
10
|
eqcomi |
⊢ ∅ = ( Vtx ‘ ∅ ) |
12 |
|
iedgval0 |
⊢ ( iEdg ‘ ∅ ) = ∅ |
13 |
12
|
eqcomi |
⊢ ∅ = ( iEdg ‘ ∅ ) |
14 |
11 13
|
isuhgr |
⊢ ( ∅ ∈ V → ( ∅ ∈ UHGraph ↔ ∅ : dom ∅ ⟶ ( 𝒫 ∅ ∖ { ∅ } ) ) ) |
15 |
9 14
|
ax-mp |
⊢ ( ∅ ∈ UHGraph ↔ ∅ : dom ∅ ⟶ ( 𝒫 ∅ ∖ { ∅ } ) ) |
16 |
8 15
|
mpbir |
⊢ ∅ ∈ UHGraph |