Metamath Proof Explorer

Theorem usgruspgr

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

Ref Expression
Assertion usgruspgr ⊢G∈USGraph→G∈USHGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 eqid ⊢iEdg⁡G=iEdg⁡G
3 1 2 isusgr ⊢G∈USGraph→G∈USGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x=2
4 2re ⊢2∈ℝ
5 4 eqlei2 ⊢x=2→x≤2
6 5 a1i ⊢x∈𝒫Vtx⁡G∖∅→x=2→x≤2
7 6 ss2rabi ⊢x∈𝒫Vtx⁡G∖∅|x=2⊆x∈𝒫Vtx⁡G∖∅|x≤2
8 f1ss ⊢iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x=2∧x∈𝒫Vtx⁡G∖∅|x=2⊆x∈𝒫Vtx⁡G∖∅|x≤2→iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2
9 7 8 mpan2 ⊢iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x=2→iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2
10 3 9 syl6bi ⊢G∈USGraph→G∈USGraph→iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2
11 1 2 isuspgr ⊢G∈USGraph→G∈USHGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2
12 10 11 sylibrd ⊢G∈USGraph→G∈USGraph→G∈USHGraph
13 12 pm2.43i ⊢G∈USGraph→G∈USHGraph