Theorem vtxdusgrval

Description: The value of the vertex degree function for a simple graph. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 11-Dec-2020)

	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	vtxdusgrval	$$⊢\left(G\in \mathrm{USGraph}\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		usgrumgr	$$⊢G\in \mathrm{USGraph}\to G\in \mathrm{UMGraph}$$
6	1 2 3 4	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|$$
7	5 6	sylan	$$⊢\left(G\in \mathrm{USGraph}\wedge U\in V\right)\to D\left(U\right)=\left|\left\{x\in A|U\in I\left(x\right)\right\}\right|$$