Metamath Proof Explorer

Theorem usgrumgr

Description: A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020)

Ref Expression
Assertion usgrumgr ⊢G∈USGraph→G∈UMGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 eqid ⊢iEdg⁡G=iEdg⁡G
3 1 2 usgrfs ⊢G∈USGraph→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 syl ⊢G∈USGraph→iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G|x=2
6 1 2 isumgrs ⊢G∈USGraph→G∈UMGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G|x=2
7 5 6 mpbird ⊢G∈USGraph→G∈UMGraph