Theorem vtxdgfisf

Description: The vertex degree function on graphs of finite size is a function from vertices to nonnegative integers. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 11-Dec-2020)

	Ref	Expression
Hypotheses	vtxdgf.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	vtxdg0e.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	vtxdgfisnn0.a	⊢ 𝐴 = dom 𝐼
Assertion	vtxdgfisf	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐴 ∈ Fin ) → ( VtxDeg ‘ 𝐺 ) : 𝑉 ⟶ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		vtxdgf.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		vtxdg0e.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		vtxdgfisnn0.a	⊢ 𝐴 = dom 𝐼
4	1	vtxdgf	⊢ ( 𝐺 ∈ 𝑊 → ( VtxDeg ‘ 𝐺 ) : 𝑉 ⟶ ℕ0* )
5	4	adantr	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐴 ∈ Fin ) → ( VtxDeg ‘ 𝐺 ) : 𝑉 ⟶ ℕ0* )
6	5	ffnd	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐴 ∈ Fin ) → ( VtxDeg ‘ 𝐺 ) Fn 𝑉 )
7	1 2 3	vtxdgfisnn0	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑢 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) ∈ ℕ0 )
8	7	adantll	⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ 𝐴 ∈ Fin ) ∧ 𝑢 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) ∈ ℕ0 )
9	8	ralrimiva	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐴 ∈ Fin ) → ∀ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) ∈ ℕ0 )
10		ffnfv	⊢ ( ( VtxDeg ‘ 𝐺 ) : 𝑉 ⟶ ℕ0 ↔ ( ( VtxDeg ‘ 𝐺 ) Fn 𝑉 ∧ ∀ 𝑢 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑢 ) ∈ ℕ0 ) )
11	6 9 10	sylanbrc	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝐴 ∈ Fin ) → ( VtxDeg ‘ 𝐺 ) : 𝑉 ⟶ ℕ0 )