Step | Hyp | Ref
| Expression |
1 | | df-vtxdg 40682 |
. . 3
⊢ VtxDeg =
(𝑔 ∈ V ↦
⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})))) |
2 | 1 | a1i 11 |
. 2
⊢ (𝐺 ∈ 𝑊 → VtxDeg = (𝑔 ∈ V ↦
⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))))) |
3 | | fvex 6113 |
. . . 4
⊢
(Vtx‘𝑔) ∈
V |
4 | | fvex 6113 |
. . . 4
⊢
(iEdg‘𝑔)
∈ V |
5 | | simpl 472 |
. . . . 5
⊢ ((𝑣 = (Vtx‘𝑔) ∧ 𝑒 = (iEdg‘𝑔)) → 𝑣 = (Vtx‘𝑔)) |
6 | | dmeq 5246 |
. . . . . . . . 9
⊢ (𝑒 = (iEdg‘𝑔) → dom 𝑒 = dom (iEdg‘𝑔)) |
7 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑒 = (iEdg‘𝑔) → (𝑒‘𝑥) = ((iEdg‘𝑔)‘𝑥)) |
8 | 7 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝑒 = (iEdg‘𝑔) → (𝑢 ∈ (𝑒‘𝑥) ↔ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥))) |
9 | 6, 8 | rabeqbidv 3168 |
. . . . . . . 8
⊢ (𝑒 = (iEdg‘𝑔) → {𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)} = {𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) |
10 | 9 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑒 = (iEdg‘𝑔) → (#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) = (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)})) |
11 | 7 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑒 = (iEdg‘𝑔) → ((𝑒‘𝑥) = {𝑢} ↔ ((iEdg‘𝑔)‘𝑥) = {𝑢})) |
12 | 6, 11 | rabeqbidv 3168 |
. . . . . . . 8
⊢ (𝑒 = (iEdg‘𝑔) → {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}} = {𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}}) |
13 | 12 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑒 = (iEdg‘𝑔) → (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}) = (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}})) |
14 | 10, 13 | oveq12d 6567 |
. . . . . 6
⊢ (𝑒 = (iEdg‘𝑔) → ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})) = ((#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}}))) |
15 | 14 | adantl 481 |
. . . . 5
⊢ ((𝑣 = (Vtx‘𝑔) ∧ 𝑒 = (iEdg‘𝑔)) → ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})) = ((#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}}))) |
16 | 5, 15 | mpteq12dv 4663 |
. . . 4
⊢ ((𝑣 = (Vtx‘𝑔) ∧ 𝑒 = (iEdg‘𝑔)) → (𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))) = (𝑢 ∈ (Vtx‘𝑔) ↦ ((#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}})))) |
17 | 3, 4, 16 | csbie2 3529 |
. . 3
⊢
⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))) = (𝑢 ∈ (Vtx‘𝑔) ↦ ((#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}}))) |
18 | | fveq2 6103 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺)) |
19 | | vtxdgfval.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
20 | 18, 19 | syl6eqr 2662 |
. . . . 5
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = 𝑉) |
21 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺)) |
22 | 21 | dmeqd 5248 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → dom (iEdg‘𝑔) = dom (iEdg‘𝐺)) |
23 | | vtxdgfval.a |
. . . . . . . . . 10
⊢ 𝐴 = dom 𝐼 |
24 | | vtxdgfval.i |
. . . . . . . . . . 11
⊢ 𝐼 = (iEdg‘𝐺) |
25 | 24 | dmeqi 5247 |
. . . . . . . . . 10
⊢ dom 𝐼 = dom (iEdg‘𝐺) |
26 | 23, 25 | eqtri 2632 |
. . . . . . . . 9
⊢ 𝐴 = dom (iEdg‘𝐺) |
27 | 22, 26 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → dom (iEdg‘𝑔) = 𝐴) |
28 | 21, 24 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = 𝐼) |
29 | 28 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((iEdg‘𝑔)‘𝑥) = (𝐼‘𝑥)) |
30 | 29 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (𝑢 ∈ ((iEdg‘𝑔)‘𝑥) ↔ 𝑢 ∈ (𝐼‘𝑥))) |
31 | 27, 30 | rabeqbidv 3168 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → {𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) |
32 | 31 | fveq2d 6107 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) = (#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)})) |
33 | 29 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (((iEdg‘𝑔)‘𝑥) = {𝑢} ↔ (𝐼‘𝑥) = {𝑢})) |
34 | 27, 33 | rabeqbidv 3168 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → {𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}} = {𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}}) |
35 | 34 | fveq2d 6107 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}}) = (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}})) |
36 | 32, 35 | oveq12d 6567 |
. . . . 5
⊢ (𝑔 = 𝐺 → ((#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}})) = ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}}))) |
37 | 20, 36 | mpteq12dv 4663 |
. . . 4
⊢ (𝑔 = 𝐺 → (𝑢 ∈ (Vtx‘𝑔) ↦ ((#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}}))) = (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}})))) |
38 | 37 | adantl 481 |
. . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑔 = 𝐺) → (𝑢 ∈ (Vtx‘𝑔) ↦ ((#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}}))) = (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}})))) |
39 | 17, 38 | syl5eq 2656 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑔 = 𝐺) → ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))) = (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}})))) |
40 | | elex 3185 |
. 2
⊢ (𝐺 ∈ 𝑊 → 𝐺 ∈ V) |
41 | | fvex 6113 |
. . . 4
⊢
(Vtx‘𝐺) ∈
V |
42 | 19, 41 | eqeltri 2684 |
. . 3
⊢ 𝑉 ∈ V |
43 | | mptexg 6389 |
. . 3
⊢ (𝑉 ∈ V → (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}}))) ∈ V) |
44 | 42, 43 | mp1i 13 |
. 2
⊢ (𝐺 ∈ 𝑊 → (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}}))) ∈ V) |
45 | 2, 39, 40, 44 | fvmptd 6197 |
1
⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺) = (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}})))) |