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

Metamath Proof Explorer

Theorem uhgr0e

Description: The empty graph, with vertices but no edges, is a hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 25-Nov-2020)

Ref Expression
Hypotheses uhgr0e.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
uhgr0e.e ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = ∅ )
Assertion uhgr0e ( 𝜑 → 𝐺 ∈ UHGraph )

Proof

Step Hyp Ref Expression
1 uhgr0e.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
2 uhgr0e.e ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = ∅ )
3 f0 ⊢ ∅ : ∅ ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } )
4 dm0 ⊢ dom ∅ = ∅
5 4 feq2i ⊢ ( ∅ : dom ∅ ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ↔ ∅ : ∅ ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
6 3 5 mpbir ⊢ ∅ : dom ∅ ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } )
7 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
8 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
9 7 8 isuhgr ⊢ ( 𝐺 ∈ 𝑊 → ( 𝐺 ∈ UHGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) )
10 1 9 syl ⊢ ( 𝜑 → ( 𝐺 ∈ UHGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) )
11 id ⊢ ( ( iEdg ‘ 𝐺 ) = ∅ → ( iEdg ‘ 𝐺 ) = ∅ )
12 dmeq ⊢ ( ( iEdg ‘ 𝐺 ) = ∅ → dom ( iEdg ‘ 𝐺 ) = dom ∅ )
13 11 12 feq12d ⊢ ( ( iEdg ‘ 𝐺 ) = ∅ → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ↔ ∅ : dom ∅ ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) )
14 2 13 syl ⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ↔ ∅ : dom ∅ ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) )
15 10 14 bitrd ⊢ ( 𝜑 → ( 𝐺 ∈ UHGraph ↔ ∅ : dom ∅ ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) )
16 6 15 mpbiri ⊢ ( 𝜑 → 𝐺 ∈ UHGraph )