Theorem vtxdgelxnn0

Description: The degree of a vertex is either a nonnegative integer or positive infinity. (Contributed by Alexander van der Vekens, 30-Dec-2017) (Revised by AV, 10-Dec-2020) (Revised by AV, 22-Mar-2021)

	Ref	Expression
Hypothesis	vtxdgf.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	vtxdgelxnn0	$$⊢X\in V\to \mathrm{VtxDeg}\left(G\right)\left(X\right)\in {\mathbb{N}}_0^{*}$$

Proof

Step	Hyp	Ref	Expression
1		vtxdgf.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	1vgrex	$$⊢X\in V\to G\in \mathrm{V}$$
3	1	vtxdgf	$$⊢G\in \mathrm{V}\to \mathrm{VtxDeg}\left(G\right):V⟶{\mathbb{N}}_0^{*}$$
4	3	ffvelrnda	$$⊢\left(G\in \mathrm{V}\wedge X\in V\right)\to \mathrm{VtxDeg}\left(G\right)\left(X\right)\in {\mathbb{N}}_0^{*}$$
5	2 4	mpancom	$$⊢X\in V\to \mathrm{VtxDeg}\left(G\right)\left(X\right)\in {\mathbb{N}}_0^{*}$$