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 )