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-1x∈𝒫Vtx⁡G∖∅|x≤2
4 ssrab2 ⊢x∈𝒫Vtx⁡G∖∅|x≤2⊆𝒫Vtx⁡G∖∅
5 f1ss ⊢iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫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-1x∈𝒫Vtx⁡G∖∅|x≤2→iEdg⁡G:dom⁡iEdg⁡G⟶1-1𝒫Vtx⁡G∖∅
7 3 6 syl6bi ⊢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