This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )