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

Metamath Proof Explorer

Theorem ushgruhgr

Description: An undirected simple hypergraph is an undirected hypergraph. (Contributed by AV, 19-Jan-2020) (Revised by AV, 9-Oct-2020)

Ref Expression
Assertion ushgruhgr ( 𝐺 ∈ USHGraph → 𝐺 ∈ UHGraph )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3 1 2 ushgrf ⊢ ( 𝐺 ∈ USHGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
4 f1f ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
5 3 4 syl ⊢ ( 𝐺 ∈ USHGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
6 1 2 isuhgr ⊢ ( 𝐺 ∈ USHGraph → ( 𝐺 ∈ UHGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) )
7 5 6 mpbird ⊢ ( 𝐺 ∈ USHGraph → 𝐺 ∈ UHGraph )