Theorem vtxdumgrval

Description: The value of the vertex degree function for a multigraph. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 23-Feb-2021)

	Ref	Expression
Hypotheses	vtxdlfgrval.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	vtxdlfgrval.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	vtxdlfgrval.a	$$⊢A=\mathrm{dom}I$$
	vtxdlfgrval.d	$$⊢D=\mathrm{VtxDeg}\left(G\right)$$
Assertion	vtxdumgrval	$$⊢\left(G\in \mathrm{UMGraph}\wedge U\in V\right)\to D\left(U\right)=\left|\left\{x\in A|U\in I\left(x\right)\right\}\right|$$

Proof

Step	Hyp	Ref	Expression
1		vtxdlfgrval.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		vtxdlfgrval.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		vtxdlfgrval.a	$$⊢A=\mathrm{dom}I$$
4		vtxdlfgrval.d	$$⊢D=\mathrm{VtxDeg}\left(G\right)$$
5	1 2	umgrislfupgr	$$⊢G\in \mathrm{UMGraph}\leftrightarrow \left(G\in \mathrm{UPGraph}\wedge I:\mathrm{dom}I⟶\left\{x\in 𝒫V|2\le \left|x\right|\right\}\right)$$
6	3	eqcomi	$$⊢\mathrm{dom}I=A$$
7	6	feq2i	$$⊢I:\mathrm{dom}I⟶\left\{x\in 𝒫V|2\le \left|x\right|\right\}\leftrightarrow I:A⟶\left\{x\in 𝒫V|2\le \left|x\right|\right\}$$
8	7	biimpi	$$⊢I:\mathrm{dom}I⟶\left\{x\in 𝒫V|2\le \left|x\right|\right\}\to I:A⟶\left\{x\in 𝒫V|2\le \left|x\right|\right\}$$
9	5 8	simplbiim	$$⊢G\in \mathrm{UMGraph}\to I:A⟶\left\{x\in 𝒫V|2\le \left|x\right|\right\}$$
10	1 2 3 4	vtxdlfgrval	$$⊢\left(I:A⟶\left\{x\in 𝒫V|2\le \left|x\right|\right\}\wedge U\in V\right)\to D\left(U\right)=\left|\left\{x\in A|U\in I\left(x\right)\right\}\right|$$
11	9 10	sylan	$$⊢\left(G\in \mathrm{UMGraph}\wedge U\in V\right)\to D\left(U\right)=\left|\left\{x\in A|U\in I\left(x\right)\right\}\right|$$