This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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