Metamath Proof Explorer

Theorem vtxdgf

Description: The vertex degree function is a function from vertices to extended nonnegative integers. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 10-Dec-2020)

Ref Expression
Hypothesis vtxdgf.v ⊢ V = Vtx ⁡ G
Assertion vtxdgf ⊢ G ∈ W → VtxDeg ⁡ G : V ⟶ ℕ 0 *

Proof

Step Hyp Ref Expression
1 vtxdgf.v ⊢ V = Vtx ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 eqid ⊢ dom ⁡ iEdg ⁡ G = dom ⁡ iEdg ⁡ G
4 1 2 3 vtxdgfval ⊢ G ∈ W → VtxDeg ⁡ G = u ∈ V ⟼ x ∈ dom ⁡ iEdg ⁡ G | u ∈ iEdg ⁡ G ⁡ x + 𝑒 x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = u
5 eqid ⊢ x ∈ dom ⁡ iEdg ⁡ G | u ∈ iEdg ⁡ G ⁡ x = x ∈ dom ⁡ iEdg ⁡ G | u ∈ iEdg ⁡ G ⁡ x
6 fvex ⊢ iEdg ⁡ G ∈ V
7 dmexg ⊢ iEdg ⁡ G ∈ V → dom ⁡ iEdg ⁡ G ∈ V
8 6 7 mp1i ⊢ G ∈ W ∧ u ∈ V → dom ⁡ iEdg ⁡ G ∈ V
9 5 8 rabexd ⊢ G ∈ W ∧ u ∈ V → x ∈ dom ⁡ iEdg ⁡ G | u ∈ iEdg ⁡ G ⁡ x ∈ V
10 hashxnn0 ⊢ x ∈ dom ⁡ iEdg ⁡ G | u ∈ iEdg ⁡ G ⁡ x ∈ V → x ∈ dom ⁡ iEdg ⁡ G | u ∈ iEdg ⁡ G ⁡ x ∈ ℕ 0 *
11 9 10 syl ⊢ G ∈ W ∧ u ∈ V → x ∈ dom ⁡ iEdg ⁡ G | u ∈ iEdg ⁡ G ⁡ x ∈ ℕ 0 *
12 eqid ⊢ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = u = x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = u
13 12 8 rabexd ⊢ G ∈ W ∧ u ∈ V → x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = u ∈ V
14 hashxnn0 ⊢ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = u ∈ V → x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = u ∈ ℕ 0 *
15 13 14 syl ⊢ G ∈ W ∧ u ∈ V → x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = u ∈ ℕ 0 *
16 xnn0xaddcl ⊢ x ∈ dom ⁡ iEdg ⁡ G | u ∈ iEdg ⁡ G ⁡ x ∈ ℕ 0 * ∧ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = u ∈ ℕ 0 * → x ∈ dom ⁡ iEdg ⁡ G | u ∈ iEdg ⁡ G ⁡ x + 𝑒 x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = u ∈ ℕ 0 *
17 11 15 16 syl2anc ⊢ G ∈ W ∧ u ∈ V → x ∈ dom ⁡ iEdg ⁡ G | u ∈ iEdg ⁡ G ⁡ x + 𝑒 x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = u ∈ ℕ 0 *
18 4 17 fmpt3d ⊢ G ∈ W → VtxDeg ⁡ G : V ⟶ ℕ 0 *