Detailed syntax breakdown of Definition df-hash
Step | Hyp | Ref
| Expression |
1 | | chash 13861 |
. 2
class
♯ |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | | cvv 3398 |
. . . . . . 7
class
V |
4 | 2 | cv 1542 |
. . . . . . . 8
class 𝑥 |
5 | | c1 10695 |
. . . . . . . 8
class
1 |
6 | | caddc 10697 |
. . . . . . . 8
class
+ |
7 | 4, 5, 6 | co 7191 |
. . . . . . 7
class (𝑥 + 1) |
8 | 2, 3, 7 | cmpt 5120 |
. . . . . 6
class (𝑥 ∈ V ↦ (𝑥 + 1)) |
9 | | cc0 10694 |
. . . . . 6
class
0 |
10 | 8, 9 | crdg 8123 |
. . . . 5
class
rec((𝑥 ∈ V
↦ (𝑥 + 1)),
0) |
11 | | com 7622 |
. . . . 5
class
ω |
12 | 10, 11 | cres 5538 |
. . . 4
class
(rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) |
13 | | ccrd 9516 |
. . . 4
class
card |
14 | 12, 13 | ccom 5540 |
. . 3
class
((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card) |
15 | | cfn 8604 |
. . . . 5
class
Fin |
16 | 3, 15 | cdif 3850 |
. . . 4
class (V
∖ Fin) |
17 | | cpnf 10829 |
. . . . 5
class
+∞ |
18 | 17 | csn 4527 |
. . . 4
class
{+∞} |
19 | 16, 18 | cxp 5534 |
. . 3
class ((V
∖ Fin) × {+∞}) |
20 | 14, 19 | cun 3851 |
. 2
class
(((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card) ∪ ((V ∖ Fin) ×
{+∞})) |
21 | 1, 20 | wceq 1543 |
1
wff ♯ =
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω) ∘ card) ∪ ((V ∖ Fin) ×
{+∞})) |