Theorem fusgrregdegfi

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

	Ref	Expression
Hypotheses	isrusgr0.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	isrusgr0.d	$$⊢D=\mathrm{VtxDeg}\left(G\right)$$
Assertion	fusgrregdegfi	$$⊢\left(G\in \mathrm{FinUSGraph}\wedge V\ne \varnothing \right)\to \left(\forall v\in VD\left(v\right)=K\to K\in {\mathbb{N}}_0\right)$$

Proof

Step	Hyp	Ref	Expression
1		isrusgr0.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		isrusgr0.d	$$⊢D=\mathrm{VtxDeg}\left(G\right)$$
3	1	vtxdgfusgr	$$⊢G\in \mathrm{FinUSGraph}\to \forall v\in V\mathrm{VtxDeg}\left(G\right)\left(v\right)\in {\mathbb{N}}_0$$
4		r19.26	$$⊢\forall v\in V\left(\mathrm{VtxDeg}\left(G\right)\left(v\right)\in {\mathbb{N}}_0\wedge D\left(v\right)=K\right)\leftrightarrow \left(\forall v\in V\mathrm{VtxDeg}\left(G\right)\left(v\right)\in {\mathbb{N}}_0\wedge \forall v\in VD\left(v\right)=K\right)$$
5	2	fveq1i	$$⊢D\left(v\right)=\mathrm{VtxDeg}\left(G\right)\left(v\right)$$
6	5	eqeq1i	$$⊢D\left(v\right)=K\leftrightarrow \mathrm{VtxDeg}\left(G\right)\left(v\right)=K$$
7		eleq1	$$⊢\mathrm{VtxDeg}\left(G\right)\left(v\right)=K\to \left(\mathrm{VtxDeg}\left(G\right)\left(v\right)\in {\mathbb{N}}_0\leftrightarrow K\in {\mathbb{N}}_0\right)$$
8	6 7	sylbi	$$⊢D\left(v\right)=K\to \left(\mathrm{VtxDeg}\left(G\right)\left(v\right)\in {\mathbb{N}}_0\leftrightarrow K\in {\mathbb{N}}_0\right)$$
9	8	biimpac	$$⊢\left(\mathrm{VtxDeg}\left(G\right)\left(v\right)\in {\mathbb{N}}_0\wedge D\left(v\right)=K\right)\to K\in {\mathbb{N}}_0$$
10	9	ralimi	$$⊢\forall v\in V\left(\mathrm{VtxDeg}\left(G\right)\left(v\right)\in {\mathbb{N}}_0\wedge D\left(v\right)=K\right)\to \forall v\in VK\in {\mathbb{N}}_0$$
11		rspn0	$$⊢V\ne \varnothing \to \left(\forall v\in VK\in {\mathbb{N}}_0\to K\in {\mathbb{N}}_0\right)$$
12	10 11	syl5com	$$⊢\forall v\in V\left(\mathrm{VtxDeg}\left(G\right)\left(v\right)\in {\mathbb{N}}_0\wedge D\left(v\right)=K\right)\to \left(V\ne \varnothing \to K\in {\mathbb{N}}_0\right)$$
13	4 12	sylbir	$$⊢\left(\forall v\in V\mathrm{VtxDeg}\left(G\right)\left(v\right)\in {\mathbb{N}}_0\wedge \forall v\in VD\left(v\right)=K\right)\to \left(V\ne \varnothing \to K\in {\mathbb{N}}_0\right)$$
14	13	ex	$$⊢\forall v\in V\mathrm{VtxDeg}\left(G\right)\left(v\right)\in {\mathbb{N}}_0\to \left(\forall v\in VD\left(v\right)=K\to \left(V\ne \varnothing \to K\in {\mathbb{N}}_0\right)\right)$$
15	14	com23	$$⊢\forall v\in V\mathrm{VtxDeg}\left(G\right)\left(v\right)\in {\mathbb{N}}_0\to \left(V\ne \varnothing \to \left(\forall v\in VD\left(v\right)=K\to K\in {\mathbb{N}}_0\right)\right)$$
16	3 15	syl	$$⊢G\in \mathrm{FinUSGraph}\to \left(V\ne \varnothing \to \left(\forall v\in VD\left(v\right)=K\to K\in {\mathbb{N}}_0\right)\right)$$
17	16	imp	$$⊢\left(G\in \mathrm{FinUSGraph}\wedge V\ne \varnothing \right)\to \left(\forall v\in VD\left(v\right)=K\to K\in {\mathbb{N}}_0\right)$$