# Metamath Proof Explorer

## Theorem umgredgss

Description: The set of edges of a multigraph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 25-Nov-2020)

Ref Expression
Assertion umgredgss ${⊢}{G}\in \mathrm{UMGraph}\to \mathrm{Edg}\left({G}\right)\subseteq \left\{{x}\in 𝒫\mathrm{Vtx}\left({G}\right)|\left|{x}\right|=2\right\}$

### Proof

Step Hyp Ref Expression
1 edgval ${⊢}\mathrm{Edg}\left({G}\right)=\mathrm{ran}\mathrm{iEdg}\left({G}\right)$
2 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
3 eqid ${⊢}\mathrm{iEdg}\left({G}\right)=\mathrm{iEdg}\left({G}\right)$
4 2 3 umgrf ${⊢}{G}\in \mathrm{UMGraph}\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 4 frnd ${⊢}{G}\in \mathrm{UMGraph}\to \mathrm{ran}\mathrm{iEdg}\left({G}\right)\subseteq \left\{{x}\in 𝒫\mathrm{Vtx}\left({G}\right)|\left|{x}\right|=2\right\}$
6 1 5 eqsstrid ${⊢}{G}\in \mathrm{UMGraph}\to \mathrm{Edg}\left({G}\right)\subseteq \left\{{x}\in 𝒫\mathrm{Vtx}\left({G}\right)|\left|{x}\right|=2\right\}$