Theorem frusgrnn0

Description: In a nonempty finite k-regular simple graph, the degree of each vertex is finite. (Contributed by AV, 7-May-2021)

	Ref	Expression
Hypothesis	frusgrnn0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	frusgrnn0	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅ ) → 𝐾 ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		frusgrnn0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		3simpb	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅ ) → ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) )
3		eqid	⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
4	1 3	rusgrprop0	⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) )
5	4	simp3d	⊢ ( 𝐺 RegUSGraph 𝐾 → ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 )
6	5	3ad2ant2	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅ ) → ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 )
7	1 3	fusgrregdegfi	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → 𝐾 ∈ ℕ0 ) )
8	2 6 7	sylc	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅ ) → 𝐾 ∈ ℕ0 )