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

Metamath Proof Explorer

Theorem uhgr0vusgr

Description: The null graph, with no vertices, represented by a hypergraph, is a simple graph. (Contributed by AV, 5-Dec-2020)

Ref Expression
Assertion uhgr0vusgr ( ( 𝐺 ∈ UHGraph ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ USGraph )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ UHGraph )
2 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
4 2 3 uhgr0v0e ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( Edg ‘ 𝐺 ) = ∅ )
5 uhgriedg0edg0 ⊢ ( 𝐺 ∈ UHGraph → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
6 5 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) )
7 4 6 mpbid ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → ( iEdg ‘ 𝐺 ) = ∅ )
8 1 7 usgr0e ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( Vtx ‘ 𝐺 ) = ∅ ) → 𝐺 ∈ USGraph )