Metamath Proof Explorer


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 )