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 ⊢ V = Vtx ⁡ G
vtxdg0e.i ⊢ I = iEdg ⁡ G
vtxdgfisnn0.a ⊢ A = dom ⁡ I
Assertion vtxdgfisf ⊢ G ∈ W ∧ A ∈ Fin → VtxDeg ⁡ G : V ⟶ ℕ 0

Proof

Step Hyp Ref Expression
1 vtxdgf.v ⊢ V = Vtx ⁡ G
2 vtxdg0e.i ⊢ I = iEdg ⁡ G
3 vtxdgfisnn0.a ⊢ A = dom ⁡ I
4 1 vtxdgf ⊢ G ∈ W → VtxDeg ⁡ G : V ⟶ ℕ 0 *
5 4 adantr ⊢ G ∈ W ∧ A ∈ Fin → VtxDeg ⁡ G : V ⟶ ℕ 0 *
6 5 ffnd ⊢ G ∈ W ∧ A ∈ Fin → VtxDeg ⁡ G Fn V
7 1 2 3 vtxdgfisnn0 ⊢ A ∈ Fin ∧ u ∈ V → VtxDeg ⁡ G ⁡ u ∈ ℕ 0
8 7 adantll ⊢ G ∈ W ∧ A ∈ Fin ∧ u ∈ V → VtxDeg ⁡ G ⁡ u ∈ ℕ 0
9 8 ralrimiva ⊢ G ∈ W ∧ A ∈ Fin → ∀ u ∈ V VtxDeg ⁡ G ⁡ u ∈ ℕ 0
10 ffnfv ⊢ VtxDeg ⁡ G : V ⟶ ℕ 0 ↔ VtxDeg ⁡ G Fn V ∧ ∀ u ∈ V VtxDeg ⁡ G ⁡ u ∈ ℕ 0
11 6 9 10 sylanbrc ⊢ G ∈ W ∧ A ∈ Fin → VtxDeg ⁡ G : V ⟶ ℕ 0