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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	isrusgr0.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion	fusgrregdegfi	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 → 𝐾 ∈ ℕ0 ) )

Proof

Step	Hyp	Ref	Expression
1		isrusgr0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isrusgr0.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
3	1	vtxdgfusgr	⊢ ( 𝐺 ∈ FinUSGraph → ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 )
4		r19.26	⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 ∧ ( 𝐷 ‘ 𝑣 ) = 𝐾 ) ↔ ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ) )
5	2	fveq1i	⊢ ( 𝐷 ‘ 𝑣 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 )
6	5	eqeq1i	⊢ ( ( 𝐷 ‘ 𝑣 ) = 𝐾 ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 )
7		eleq1	⊢ ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 ↔ 𝐾 ∈ ℕ0 ) )
8	6 7	sylbi	⊢ ( ( 𝐷 ‘ 𝑣 ) = 𝐾 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 ↔ 𝐾 ∈ ℕ0 ) )
9	8	biimpac	⊢ ( ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 ∧ ( 𝐷 ‘ 𝑣 ) = 𝐾 ) → 𝐾 ∈ ℕ0 )
10	9	ralimi	⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 ∧ ( 𝐷 ‘ 𝑣 ) = 𝐾 ) → ∀ 𝑣 ∈ 𝑉 𝐾 ∈ ℕ0 )
11		rspn0	⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑣 ∈ 𝑉 𝐾 ∈ ℕ0 → 𝐾 ∈ ℕ0 ) )
12	10 11	syl5com	⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 ∧ ( 𝐷 ‘ 𝑣 ) = 𝐾 ) → ( 𝑉 ≠ ∅ → 𝐾 ∈ ℕ0 ) )
13	4 12	sylbir	⊢ ( ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ) → ( 𝑉 ≠ ∅ → 𝐾 ∈ ℕ0 ) )
14	13	ex	⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 → ( 𝑉 ≠ ∅ → 𝐾 ∈ ℕ0 ) ) )
15	14	com23	⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 → ( 𝑉 ≠ ∅ → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 → 𝐾 ∈ ℕ0 ) ) )
16	3 15	syl	⊢ ( 𝐺 ∈ FinUSGraph → ( 𝑉 ≠ ∅ → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 → 𝐾 ∈ ℕ0 ) ) )
17	16	imp	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 → 𝐾 ∈ ℕ0 ) )