Theorem vtxdgfisf

Description: The vertex degree function on graphs of finite size is a function from vertices to nonnegative integers. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 11-Dec-2020)

	Ref	Expression
Hypotheses	vtxdgf.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	vtxdg0e.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
	vtxdgfisnn0.a	$$⊢A=\mathrm{dom}I$$
Assertion	vtxdgfisf	$$⊢\left(G\in W\wedge A\in \mathrm{Fin}\right)\to \mathrm{VtxDeg}\left(G\right):V⟶{\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		vtxdgf.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		vtxdg0e.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
3		vtxdgfisnn0.a	$$⊢A=\mathrm{dom}I$$
4	1	vtxdgf	$$⊢G\in W\to \mathrm{VtxDeg}\left(G\right):V⟶{\mathbb{N}}_0^{*}$$
5	4	adantr	$$⊢\left(G\in W\wedge A\in \mathrm{Fin}\right)\to \mathrm{VtxDeg}\left(G\right):V⟶{\mathbb{N}}_0^{*}$$
6	5	ffnd	$$⊢\left(G\in W\wedge A\in \mathrm{Fin}\right)\to \mathrm{VtxDeg}\left(G\right)FnV$$
7	1 2 3	vtxdgfisnn0	$$⊢\left(A\in \mathrm{Fin}\wedge u\in V\right)\to \mathrm{VtxDeg}\left(G\right)\left(u\right)\in {\mathbb{N}}_0$$
8	7	adantll	$$⊢\left(\left(G\in W\wedge A\in \mathrm{Fin}\right)\wedge u\in V\right)\to \mathrm{VtxDeg}\left(G\right)\left(u\right)\in {\mathbb{N}}_0$$
9	8	ralrimiva	$$⊢\left(G\in W\wedge A\in \mathrm{Fin}\right)\to \forall u\in V\mathrm{VtxDeg}\left(G\right)\left(u\right)\in {\mathbb{N}}_0$$
10		ffnfv	$$⊢\mathrm{VtxDeg}\left(G\right):V⟶{\mathbb{N}}_0\leftrightarrow \left(\mathrm{VtxDeg}\left(G\right)FnV\wedge \forall u\in V\mathrm{VtxDeg}\left(G\right)\left(u\right)\in {\mathbb{N}}_0\right)$$
11	6 9 10	sylanbrc	$$⊢\left(G\in W\wedge A\in \mathrm{Fin}\right)\to \mathrm{VtxDeg}\left(G\right):V⟶{\mathbb{N}}_0$$