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 ⊢ G ∈ USHGraph → G ∈ UHGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 1 2 ushgrf ⊢ G ∈ USHGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 𝒫 Vtx ⁡ G ∖ ∅
4 f1f ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 𝒫 Vtx ⁡ G ∖ ∅ → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 𝒫 Vtx ⁡ G ∖ ∅
5 3 4 syl ⊢ G ∈ USHGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 𝒫 Vtx ⁡ G ∖ ∅
6 1 2 isuhgr ⊢ G ∈ USHGraph → G ∈ UHGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 𝒫 Vtx ⁡ G ∖ ∅
7 5 6 mpbird ⊢ G ∈ USHGraph → G ∈ UHGraph