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

Metamath Proof Explorer

Theorem uhgr0vb

Description: The null graph, with no vertices, is a hypergraph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 27-Dec-2017) (Revised by AV, 9-Oct-2020)

Ref Expression
Assertion uhgr0vb ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ UHGraph ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3 1 2 uhgrf ⊢ ( 𝐺 ∈ UHGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
4 pweq ⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → 𝒫 ( Vtx ‘ 𝐺 ) = 𝒫 ∅ )
5 4 difeq1d ⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) = ( 𝒫 ∅ ∖ { ∅ } ) )
6 pw0 ⊢ 𝒫 ∅ = { ∅ }
7 6 difeq1i ⊢ ( 𝒫 ∅ ∖ { ∅ } ) = ( { ∅ } ∖ { ∅ } )
8 difid ⊢ ( { ∅ } ∖ { ∅ } ) = ∅
9 7 8 eqtri ⊢ ( 𝒫 ∅ ∖ { ∅ } ) = ∅
10 5 9 eqtrdi ⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) = ∅ )
11 10 adantl ⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) = ∅ )
12 11 feq3d ⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ∅ ) )
13 f00 ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ∅ ↔ ( ( iEdg ‘ 𝐺 ) = ∅ ∧ dom ( iEdg ‘ 𝐺 ) = ∅ ) )
14 13 simplbi ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ∅ → ( iEdg ‘ 𝐺 ) = ∅ )
15 12 14 biimtrdi ⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) → ( iEdg ‘ 𝐺 ) = ∅ ) )
16 3 15 syl5 ⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ UHGraph → ( iEdg ‘ 𝐺 ) = ∅ ) )
17 simpl ⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ 𝑊 )
18 simpr ⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → ( iEdg ‘ 𝐺 ) = ∅ )
19 17 18 uhgr0e ⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( iEdg ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ UHGraph )
20 19 ex ⊢ ( 𝐺 ∈ 𝑊 → ( ( iEdg ‘ 𝐺 ) = ∅ → 𝐺 ∈ UHGraph ) )
21 20 adantr ⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( ( iEdg ‘ 𝐺 ) = ∅ → 𝐺 ∈ UHGraph ) )
22 16 21 impbid ⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( 𝐺 ∈ UHGraph ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )