Metamath Proof Explorer

Theorem uspgrushgr

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

Ref Expression
Assertion uspgrushgr ⊢ G ∈ USHGraph → G ∈ USHGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 1 2 isuspgr ⊢ G ∈ USHGraph → G ∈ USHGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2
4 ssrab2 ⊢ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 ⊆ 𝒫 Vtx ⁡ G ∖ ∅
5 f1ss ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 ∧ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 ⊆ 𝒫 Vtx ⁡ G ∖ ∅ → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 𝒫 Vtx ⁡ G ∖ ∅
6 4 5 mpan2 ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x ≤ 2 → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 𝒫 Vtx ⁡ G ∖ ∅
7 3 6 biimtrdi ⊢ G ∈ USHGraph → G ∈ USHGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 𝒫 Vtx ⁡ G ∖ ∅
8 1 2 isushgr ⊢ G ∈ USHGraph → G ∈ USHGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 𝒫 Vtx ⁡ G ∖ ∅
9 7 8 sylibrd ⊢ G ∈ USHGraph → G ∈ USHGraph → G ∈ USHGraph
10 9 pm2.43i ⊢ G ∈ USHGraph → G ∈ USHGraph