Metamath Proof Explorer

Theorem usgrumgr

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

Ref Expression
Assertion usgrumgr ${⊢}{G}\in \mathrm{USGraph}\to {G}\in \mathrm{UMGraph}$

Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
2 eqid ${⊢}\mathrm{iEdg}\left({G}\right)=\mathrm{iEdg}\left({G}\right)$
3 1 2 usgrfs ${⊢}{G}\in \mathrm{USGraph}\to \mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)\underset{1-1}{⟶}\left\{{x}\in 𝒫\mathrm{Vtx}\left({G}\right)|\left|{x}\right|=2\right\}$
4 f1f ${⊢}\mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)\underset{1-1}{⟶}\left\{{x}\in 𝒫\mathrm{Vtx}\left({G}\right)|\left|{x}\right|=2\right\}\to \mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)⟶\left\{{x}\in 𝒫\mathrm{Vtx}\left({G}\right)|\left|{x}\right|=2\right\}$
5 3 4 syl ${⊢}{G}\in \mathrm{USGraph}\to \mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)⟶\left\{{x}\in 𝒫\mathrm{Vtx}\left({G}\right)|\left|{x}\right|=2\right\}$
6 1 2 isumgrs ${⊢}{G}\in \mathrm{USGraph}\to \left({G}\in \mathrm{UMGraph}↔\mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)⟶\left\{{x}\in 𝒫\mathrm{Vtx}\left({G}\right)|\left|{x}\right|=2\right\}\right)$
7 5 6 mpbird ${⊢}{G}\in \mathrm{USGraph}\to {G}\in \mathrm{UMGraph}$