Metamath Proof Explorer

Theorem uspgrupgr

Description: A simple pseudograph is an undirected pseudograph. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 15-Oct-2020)

Ref Expression
Assertion uspgrupgr ⊢G∈USHGraph→G∈UPGraph

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 f1f ⊢iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2→iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x≤2
5 3 4 syl6bi ⊢G∈USHGraph→G∈USHGraph→iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x≤2
6 1 2 isupgr ⊢G∈USHGraph→G∈UPGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x≤2
7 5 6 sylibrd ⊢G∈USHGraph→G∈USHGraph→G∈UPGraph
8 7 pm2.43i ⊢G∈USHGraph→G∈UPGraph