Detailed syntax breakdown of Definition df-vtxdg
Step | Hyp | Ref
| Expression |
1 | | cvtxdg 27813 |
. 2
class
VtxDeg |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3430 |
. . 3
class
V |
4 | | vv |
. . . 4
setvar 𝑣 |
5 | 2 | cv 1540 |
. . . . 5
class 𝑔 |
6 | | cvtx 27347 |
. . . . 5
class
Vtx |
7 | 5, 6 | cfv 6430 |
. . . 4
class
(Vtx‘𝑔) |
8 | | ve |
. . . . 5
setvar 𝑒 |
9 | | ciedg 27348 |
. . . . . 6
class
iEdg |
10 | 5, 9 | cfv 6430 |
. . . . 5
class
(iEdg‘𝑔) |
11 | | vu |
. . . . . 6
setvar 𝑢 |
12 | 4 | cv 1540 |
. . . . . 6
class 𝑣 |
13 | 11 | cv 1540 |
. . . . . . . . . 10
class 𝑢 |
14 | | vx |
. . . . . . . . . . . 12
setvar 𝑥 |
15 | 14 | cv 1540 |
. . . . . . . . . . 11
class 𝑥 |
16 | 8 | cv 1540 |
. . . . . . . . . . 11
class 𝑒 |
17 | 15, 16 | cfv 6430 |
. . . . . . . . . 10
class (𝑒‘𝑥) |
18 | 13, 17 | wcel 2109 |
. . . . . . . . 9
wff 𝑢 ∈ (𝑒‘𝑥) |
19 | 16 | cdm 5588 |
. . . . . . . . 9
class dom 𝑒 |
20 | 18, 14, 19 | crab 3069 |
. . . . . . . 8
class {𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)} |
21 | | chash 14025 |
. . . . . . . 8
class
♯ |
22 | 20, 21 | cfv 6430 |
. . . . . . 7
class
(♯‘{𝑥
∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) |
23 | 13 | csn 4566 |
. . . . . . . . . 10
class {𝑢} |
24 | 17, 23 | wceq 1541 |
. . . . . . . . 9
wff (𝑒‘𝑥) = {𝑢} |
25 | 24, 14, 19 | crab 3069 |
. . . . . . . 8
class {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}} |
26 | 25, 21 | cfv 6430 |
. . . . . . 7
class
(♯‘{𝑥
∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}) |
27 | | cxad 12828 |
. . . . . . 7
class
+𝑒 |
28 | 22, 26, 27 | co 7268 |
. . . . . 6
class
((♯‘{𝑥
∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})) |
29 | 11, 12, 28 | cmpt 5161 |
. . . . 5
class (𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))) |
30 | 8, 10, 29 | csb 3836 |
. . . 4
class
⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))) |
31 | 4, 7, 30 | csb 3836 |
. . 3
class
⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))) |
32 | 2, 3, 31 | cmpt 5161 |
. 2
class (𝑔 ∈ V ↦
⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})))) |
33 | 1, 32 | wceq 1541 |
1
wff VtxDeg =
(𝑔 ∈ V ↦
⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})))) |