Theorem umgredg2

Description: An edge of a multigraph has exactly two ends. (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	umgredg2	$$⊢\left(G\in \mathrm{UMGraph}\wedge X\in \mathrm{dom}E\right)\to \left|E\left(X\right)\right|=2$$

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	umgrf	$$⊢G\in \mathrm{UMGraph}\to E:\mathrm{dom}E⟶\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
4	3	ffvelrnda	$$⊢\left(G\in \mathrm{UMGraph}\wedge X\in \mathrm{dom}E\right)\to E\left(X\right)\in \left\{x\in 𝒫V|\left|x\right|=2\right\}$$
5		fveqeq2	$$⊢x=E\left(X\right)\to \left(\left|x\right|=2\leftrightarrow \left|E\left(X\right)\right|=2\right)$$
6	5	elrab	$$⊢E\left(X\right)\in \left\{x\in 𝒫V|\left|x\right|=2\right\}\leftrightarrow \left(E\left(X\right)\in 𝒫V\wedge \left|E\left(X\right)\right|=2\right)$$
7	6	simprbi	$$⊢E\left(X\right)\in \left\{x\in 𝒫V|\left|x\right|=2\right\}\to \left|E\left(X\right)\right|=2$$
8	4 7	syl	$$⊢\left(G\in \mathrm{UMGraph}\wedge X\in \mathrm{dom}E\right)\to \left|E\left(X\right)\right|=2$$