Metamath Proof Explorer

Theorem vtxdgfval

Description: The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 9-Dec-2020)

Ref Expression
Hypotheses vtxdgfval.v ⊢ V = Vtx ⁡ G
vtxdgfval.i ⊢ I = iEdg ⁡ G
vtxdgfval.a ⊢ A = dom ⁡ I
Assertion vtxdgfval ⊢ G ∈ W → VtxDeg ⁡ G = u ∈ V ⟼ x ∈ A | u ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = u

Proof

Step Hyp Ref Expression
1 vtxdgfval.v ⊢ V = Vtx ⁡ G
2 vtxdgfval.i ⊢ I = iEdg ⁡ G
3 vtxdgfval.a ⊢ A = dom ⁡ I
4 df-vtxdg ⊢ VtxDeg = g ∈ V ⟼ ⦋ Vtx ⁡ g / v⦌ ⦋ iEdg ⁡ g / e⦌ u ∈ v ⟼ x ∈ dom ⁡ e | u ∈ e ⁡ x + 𝑒 x ∈ dom ⁡ e | e ⁡ x = u
5 fvex ⊢ Vtx ⁡ g ∈ V
6 fvex ⊢ iEdg ⁡ g ∈ V
7 simpl ⊢ v = Vtx ⁡ g ∧ e = iEdg ⁡ g → v = Vtx ⁡ g
8 dmeq ⊢ e = iEdg ⁡ g → dom ⁡ e = dom ⁡ iEdg ⁡ g
9 fveq1 ⊢ e = iEdg ⁡ g → e ⁡ x = iEdg ⁡ g ⁡ x
10 9 eleq2d ⊢ e = iEdg ⁡ g → u ∈ e ⁡ x ↔ u ∈ iEdg ⁡ g ⁡ x
11 8 10 rabeqbidv ⊢ e = iEdg ⁡ g → x ∈ dom ⁡ e | u ∈ e ⁡ x = x ∈ dom ⁡ iEdg ⁡ g | u ∈ iEdg ⁡ g ⁡ x
12 11 fveq2d ⊢ e = iEdg ⁡ g → x ∈ dom ⁡ e | u ∈ e ⁡ x = x ∈ dom ⁡ iEdg ⁡ g | u ∈ iEdg ⁡ g ⁡ x
13 9 eqeq1d ⊢ e = iEdg ⁡ g → e ⁡ x = u ↔ iEdg ⁡ g ⁡ x = u
14 8 13 rabeqbidv ⊢ e = iEdg ⁡ g → x ∈ dom ⁡ e | e ⁡ x = u = x ∈ dom ⁡ iEdg ⁡ g | iEdg ⁡ g ⁡ x = u
15 14 fveq2d ⊢ e = iEdg ⁡ g → x ∈ dom ⁡ e | e ⁡ x = u = x ∈ dom ⁡ iEdg ⁡ g | iEdg ⁡ g ⁡ x = u
16 12 15 oveq12d ⊢ e = iEdg ⁡ g → x ∈ dom ⁡ e | u ∈ e ⁡ x + 𝑒 x ∈ dom ⁡ e | e ⁡ x = u = x ∈ dom ⁡ iEdg ⁡ g | u ∈ iEdg ⁡ g ⁡ x + 𝑒 x ∈ dom ⁡ iEdg ⁡ g | iEdg ⁡ g ⁡ x = u
17 16 adantl ⊢ v = Vtx ⁡ g ∧ e = iEdg ⁡ g → x ∈ dom ⁡ e | u ∈ e ⁡ x + 𝑒 x ∈ dom ⁡ e | e ⁡ x = u = x ∈ dom ⁡ iEdg ⁡ g | u ∈ iEdg ⁡ g ⁡ x + 𝑒 x ∈ dom ⁡ iEdg ⁡ g | iEdg ⁡ g ⁡ x = u
18 7 17 mpteq12dv ⊢ v = Vtx ⁡ g ∧ e = iEdg ⁡ g → u ∈ v ⟼ x ∈ dom ⁡ e | u ∈ e ⁡ x + 𝑒 x ∈ dom ⁡ e | e ⁡ x = u = u ∈ Vtx ⁡ g ⟼ x ∈ dom ⁡ iEdg ⁡ g | u ∈ iEdg ⁡ g ⁡ x + 𝑒 x ∈ dom ⁡ iEdg ⁡ g | iEdg ⁡ g ⁡ x = u
19 5 6 18 csbie2 ⊢ ⦋ Vtx ⁡ g / v⦌ ⦋ iEdg ⁡ g / e⦌ u ∈ v ⟼ x ∈ dom ⁡ e | u ∈ e ⁡ x + 𝑒 x ∈ dom ⁡ e | e ⁡ x = u = u ∈ Vtx ⁡ g ⟼ x ∈ dom ⁡ iEdg ⁡ g | u ∈ iEdg ⁡ g ⁡ x + 𝑒 x ∈ dom ⁡ iEdg ⁡ g | iEdg ⁡ g ⁡ x = u
20 fveq2 ⊢ g = G → Vtx ⁡ g = Vtx ⁡ G
21 20 1 eqtr4di ⊢ g = G → Vtx ⁡ g = V
22 fveq2 ⊢ g = G → iEdg ⁡ g = iEdg ⁡ G
23 22 dmeqd ⊢ g = G → dom ⁡ iEdg ⁡ g = dom ⁡ iEdg ⁡ G
24 2 dmeqi ⊢ dom ⁡ I = dom ⁡ iEdg ⁡ G
25 3 24 eqtri ⊢ A = dom ⁡ iEdg ⁡ G
26 23 25 eqtr4di ⊢ g = G → dom ⁡ iEdg ⁡ g = A
27 22 2 eqtr4di ⊢ g = G → iEdg ⁡ g = I
28 27 fveq1d ⊢ g = G → iEdg ⁡ g ⁡ x = I ⁡ x
29 28 eleq2d ⊢ g = G → u ∈ iEdg ⁡ g ⁡ x ↔ u ∈ I ⁡ x
30 26 29 rabeqbidv ⊢ g = G → x ∈ dom ⁡ iEdg ⁡ g | u ∈ iEdg ⁡ g ⁡ x = x ∈ A | u ∈ I ⁡ x
31 30 fveq2d ⊢ g = G → x ∈ dom ⁡ iEdg ⁡ g | u ∈ iEdg ⁡ g ⁡ x = x ∈ A | u ∈ I ⁡ x
32 28 eqeq1d ⊢ g = G → iEdg ⁡ g ⁡ x = u ↔ I ⁡ x = u
33 26 32 rabeqbidv ⊢ g = G → x ∈ dom ⁡ iEdg ⁡ g | iEdg ⁡ g ⁡ x = u = x ∈ A | I ⁡ x = u
34 33 fveq2d ⊢ g = G → x ∈ dom ⁡ iEdg ⁡ g | iEdg ⁡ g ⁡ x = u = x ∈ A | I ⁡ x = u
35 31 34 oveq12d ⊢ g = G → x ∈ dom ⁡ iEdg ⁡ g | u ∈ iEdg ⁡ g ⁡ x + 𝑒 x ∈ dom ⁡ iEdg ⁡ g | iEdg ⁡ g ⁡ x = u = x ∈ A | u ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = u
36 21 35 mpteq12dv ⊢ g = G → u ∈ Vtx ⁡ g ⟼ x ∈ dom ⁡ iEdg ⁡ g | u ∈ iEdg ⁡ g ⁡ x + 𝑒 x ∈ dom ⁡ iEdg ⁡ g | iEdg ⁡ g ⁡ x = u = u ∈ V ⟼ x ∈ A | u ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = u
37 36 adantl ⊢ G ∈ W ∧ g = G → u ∈ Vtx ⁡ g ⟼ x ∈ dom ⁡ iEdg ⁡ g | u ∈ iEdg ⁡ g ⁡ x + 𝑒 x ∈ dom ⁡ iEdg ⁡ g | iEdg ⁡ g ⁡ x = u = u ∈ V ⟼ x ∈ A | u ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = u
38 19 37 eqtrid ⊢ G ∈ W ∧ g = G → ⦋ Vtx ⁡ g / v⦌ ⦋ iEdg ⁡ g / e⦌ u ∈ v ⟼ x ∈ dom ⁡ e | u ∈ e ⁡ x + 𝑒 x ∈ dom ⁡ e | e ⁡ x = u = u ∈ V ⟼ x ∈ A | u ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = u
39 elex ⊢ G ∈ W → G ∈ V
40 1 fvexi ⊢ V ∈ V
41 mptexg ⊢ V ∈ V → u ∈ V ⟼ x ∈ A | u ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = u ∈ V
42 40 41 mp1i ⊢ G ∈ W → u ∈ V ⟼ x ∈ A | u ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = u ∈ V
43 4 38 39 42 fvmptd2 ⊢ G ∈ W → VtxDeg ⁡ G = u ∈ V ⟼ x ∈ A | u ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = u