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