Metamath Proof Explorer

Theorem vtxdgfisnn0

Description: The degree of a vertex in a graph of finite size is a nonnegative integer. (Contributed by Alexander van der Vekens, 10-Mar-2018) (Revised by AV, 11-Dec-2020) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypotheses vtxdgf.v ⊢ V = Vtx ⁡ G
vtxdg0e.i ⊢ I = iEdg ⁡ G
vtxdgfisnn0.a ⊢ A = dom ⁡ I
Assertion vtxdgfisnn0 ⊢ A ∈ Fin ∧ U ∈ V → VtxDeg ⁡ G ⁡ U ∈ ℕ 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 2 3 vtxdgfival ⊢ A ∈ Fin ∧ U ∈ V → VtxDeg ⁡ G ⁡ U = x ∈ A | U ∈ I ⁡ x + x ∈ A | I ⁡ x = U
5 rabfi ⊢ A ∈ Fin → x ∈ A | U ∈ I ⁡ x ∈ Fin
6 hashcl ⊢ x ∈ A | U ∈ I ⁡ x ∈ Fin → x ∈ A | U ∈ I ⁡ x ∈ ℕ 0
7 5 6 syl ⊢ A ∈ Fin → x ∈ A | U ∈ I ⁡ x ∈ ℕ 0
8 rabfi ⊢ A ∈ Fin → x ∈ A | I ⁡ x = U ∈ Fin
9 hashcl ⊢ x ∈ A | I ⁡ x = U ∈ Fin → x ∈ A | I ⁡ x = U ∈ ℕ 0
10 8 9 syl ⊢ A ∈ Fin → x ∈ A | I ⁡ x = U ∈ ℕ 0
11 7 10 nn0addcld ⊢ A ∈ Fin → x ∈ A | U ∈ I ⁡ x + x ∈ A | I ⁡ x = U ∈ ℕ 0
12 11 adantr ⊢ A ∈ Fin ∧ U ∈ V → x ∈ A | U ∈ I ⁡ x + x ∈ A | I ⁡ x = U ∈ ℕ 0
13 4 12 eqeltrd ⊢ A ∈ Fin ∧ U ∈ V → VtxDeg ⁡ G ⁡ U ∈ ℕ 0