# Metamath Proof Explorer

## Theorem isumgrs

Description: The simplified property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020)

Ref Expression
Hypotheses isumgr.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
isumgr.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
Assertion isumgrs ${⊢}{G}\in {U}\to \left({G}\in \mathrm{UMGraph}↔{E}:\mathrm{dom}{E}⟶\left\{{x}\in 𝒫{V}|\left|{x}\right|=2\right\}\right)$

### Proof

Step Hyp Ref Expression
1 isumgr.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 isumgr.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
3 1 2 isumgr ${⊢}{G}\in {U}\to \left({G}\in \mathrm{UMGraph}↔{E}:\mathrm{dom}{E}⟶\left\{{x}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|=2\right\}\right)$
4 prprrab ${⊢}\left\{{x}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|=2\right\}=\left\{{x}\in 𝒫{V}|\left|{x}\right|=2\right\}$
5 4 a1i ${⊢}{G}\in {U}\to \left\{{x}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|=2\right\}=\left\{{x}\in 𝒫{V}|\left|{x}\right|=2\right\}$
6 5 feq3d ${⊢}{G}\in {U}\to \left({E}:\mathrm{dom}{E}⟶\left\{{x}\in \left(𝒫{V}\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|=2\right\}↔{E}:\mathrm{dom}{E}⟶\left\{{x}\in 𝒫{V}|\left|{x}\right|=2\right\}\right)$
7 3 6 bitrd ${⊢}{G}\in {U}\to \left({G}\in \mathrm{UMGraph}↔{E}:\mathrm{dom}{E}⟶\left\{{x}\in 𝒫{V}|\left|{x}\right|=2\right\}\right)$