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}\leftrightarrow 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}\leftrightarrow 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\}\leftrightarrow 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}\leftrightarrow E:\mathrm{dom}E⟶\left\{x\in 𝒫V|\left|x\right|=2\right\}\right)$$