Metamath Proof Explorer

Theorem usgrumgruspgr

Description: A graph is a simple graph iff it is a multigraph and a simple pseudograph. (Contributed by AV, 30-Nov-2020)

Ref Expression
Assertion usgrumgruspgr ⊢G∈USGraph↔G∈UMGraph∧G∈USHGraph

Proof

Step Hyp Ref Expression
1 usgrumgr ⊢G∈USGraph→G∈UMGraph
2 usgruspgr ⊢G∈USGraph→G∈USHGraph
3 1 2 jca ⊢G∈USGraph→G∈UMGraph∧G∈USHGraph
4 eqid ⊢Vtx⁡G=Vtx⁡G
5 eqid ⊢iEdg⁡G=iEdg⁡G
6 4 5 uspgrf ⊢G∈USHGraph→iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2
7 umgredgss ⊢G∈UMGraph→Edg⁡G⊆x∈𝒫Vtx⁡G|x=2
8 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
9 prprrab ⊢x∈𝒫Vtx⁡G∖∅|x=2=x∈𝒫Vtx⁡G|x=2
10 9 eqcomi ⊢x∈𝒫Vtx⁡G|x=2=x∈𝒫Vtx⁡G∖∅|x=2
11 7 8 10 3sstr3g ⊢G∈UMGraph→ran⁡iEdg⁡G⊆x∈𝒫Vtx⁡G∖∅|x=2
12 f1ssr ⊢iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x≤2∧ran⁡iEdg⁡G⊆x∈𝒫Vtx⁡G∖∅|x=2→iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x=2
13 6 11 12 syl2anr ⊢G∈UMGraph∧G∈USHGraph→iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x=2
14 4 5 isusgr ⊢G∈UMGraph→G∈USGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x=2
15 14 adantr ⊢G∈UMGraph∧G∈USHGraph→G∈USGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶1-1x∈𝒫Vtx⁡G∖∅|x=2
16 13 15 mpbird ⊢G∈UMGraph∧G∈USHGraph→G∈USGraph
17 3 16 impbii ⊢G∈USGraph↔G∈UMGraph∧G∈USHGraph