Metamath Proof Explorer

Theorem vtxdgfival

Description: The degree of a vertex for graphs of finite size. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 21-Jan-2018) (Revised by AV, 8-Dec-2020) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypotheses vtxdgval.v ⊢ V = Vtx ⁡ G
vtxdgval.i ⊢ I = iEdg ⁡ G
vtxdgval.a ⊢ A = dom ⁡ I
Assertion vtxdgfival ⊢ A ∈ Fin ∧ U ∈ V → VtxDeg ⁡ G ⁡ U = x ∈ A | U ∈ I ⁡ x + x ∈ A | I ⁡ x = U

Proof

Step Hyp Ref Expression
1 vtxdgval.v ⊢ V = Vtx ⁡ G
2 vtxdgval.i ⊢ I = iEdg ⁡ G
3 vtxdgval.a ⊢ A = dom ⁡ I
4 1 2 3 vtxdgval ⊢ U ∈ V → VtxDeg ⁡ G ⁡ U = x ∈ A | U ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = U
5 4 adantl ⊢ A ∈ Fin ∧ U ∈ V → VtxDeg ⁡ G ⁡ U = x ∈ A | U ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = U
6 rabfi ⊢ A ∈ Fin → x ∈ A | U ∈ I ⁡ x ∈ Fin
7 hashcl ⊢ x ∈ A | U ∈ I ⁡ x ∈ Fin → x ∈ A | U ∈ I ⁡ x ∈ ℕ 0
8 6 7 syl ⊢ A ∈ Fin → x ∈ A | U ∈ I ⁡ x ∈ ℕ 0
9 8 nn0red ⊢ A ∈ Fin → x ∈ A | U ∈ I ⁡ x ∈ ℝ
10 rabfi ⊢ A ∈ Fin → x ∈ A | I ⁡ x = U ∈ Fin
11 hashcl ⊢ x ∈ A | I ⁡ x = U ∈ Fin → x ∈ A | I ⁡ x = U ∈ ℕ 0
12 10 11 syl ⊢ A ∈ Fin → x ∈ A | I ⁡ x = U ∈ ℕ 0
13 12 nn0red ⊢ A ∈ Fin → x ∈ A | I ⁡ x = U ∈ ℝ
14 9 13 jca ⊢ A ∈ Fin → x ∈ A | U ∈ I ⁡ x ∈ ℝ ∧ x ∈ A | I ⁡ x = U ∈ ℝ
15 14 adantr ⊢ A ∈ Fin ∧ U ∈ V → x ∈ A | U ∈ I ⁡ x ∈ ℝ ∧ x ∈ A | I ⁡ x = U ∈ ℝ
16 rexadd ⊢ x ∈ A | U ∈ I ⁡ x ∈ ℝ ∧ x ∈ A | I ⁡ x = U ∈ ℝ → x ∈ A | U ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = U = x ∈ A | U ∈ I ⁡ x + x ∈ A | I ⁡ x = U
17 15 16 syl ⊢ A ∈ Fin ∧ U ∈ V → x ∈ A | U ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = U = x ∈ A | U ∈ I ⁡ x + x ∈ A | I ⁡ x = U
18 5 17 eqtrd ⊢ A ∈ Fin ∧ U ∈ V → VtxDeg ⁡ G ⁡ U = x ∈ A | U ∈ I ⁡ x + x ∈ A | I ⁡ x = U