Metamath Proof Explorer


Theorem uhgr0

Description: The null graph represented by an empty set is a hypergraph. (Contributed by AV, 9-Oct-2020)

Ref Expression
Assertion uhgr0 ∅ ∈ UHGraph

Proof

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