Theorem vtxdgfusgr

Description: In a finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 10-Mar-2018) (Revised by AV, 12-Dec-2020)

	Ref	Expression
Hypothesis	vtxdgfusgrf.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	vtxdgfusgr	$$⊢G\in \mathrm{FinUSGraph}\to \forall v\in V\mathrm{VtxDeg}\left(G\right)\left(v\right)\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		vtxdgfusgrf.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	vtxdgfusgrf	$$⊢G\in \mathrm{FinUSGraph}\to \mathrm{VtxDeg}\left(G\right):V⟶{\mathbb{N}}_0$$
3	2	ffvelcdmda	$$⊢\left(G\in \mathrm{FinUSGraph}\wedge v\in V\right)\to \mathrm{VtxDeg}\left(G\right)\left(v\right)\in {\mathbb{N}}_0$$
4	3	ralrimiva	$$⊢G\in \mathrm{FinUSGraph}\to \forall v\in V\mathrm{VtxDeg}\left(G\right)\left(v\right)\in {\mathbb{N}}_0$$