Detailed syntax breakdown of Definition df-hash
| Step | Hyp | Ref
| Expression |
| 1 | | chash 14369 |
. 2
class
♯ |
| 2 | | vx |
. . . . . . 7
setvar 𝑥 |
| 3 | | cvv 3480 |
. . . . . . 7
class
V |
| 4 | 2 | cv 1539 |
. . . . . . . 8
class 𝑥 |
| 5 | | c1 11156 |
. . . . . . . 8
class
1 |
| 6 | | caddc 11158 |
. . . . . . . 8
class
+ |
| 7 | 4, 5, 6 | co 7431 |
. . . . . . 7
class (𝑥 + 1) |
| 8 | 2, 3, 7 | cmpt 5225 |
. . . . . 6
class (𝑥 ∈ V ↦ (𝑥 + 1)) |
| 9 | | cc0 11155 |
. . . . . 6
class
0 |
| 10 | 8, 9 | crdg 8449 |
. . . . 5
class
rec((𝑥 ∈ V
↦ (𝑥 + 1)),
0) |
| 11 | | com 7887 |
. . . . 5
class
ω |
| 12 | 10, 11 | cres 5687 |
. . . 4
class
(rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) |
| 13 | | ccrd 9975 |
. . . 4
class
card |
| 14 | 12, 13 | ccom 5689 |
. . 3
class
((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card) |
| 15 | | cfn 8985 |
. . . . 5
class
Fin |
| 16 | 3, 15 | cdif 3948 |
. . . 4
class (V
∖ Fin) |
| 17 | | cpnf 11292 |
. . . . 5
class
+∞ |
| 18 | 17 | csn 4626 |
. . . 4
class
{+∞} |
| 19 | 16, 18 | cxp 5683 |
. . 3
class ((V
∖ Fin) × {+∞}) |
| 20 | 14, 19 | cun 3949 |
. 2
class
(((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card) ∪ ((V ∖ Fin) ×
{+∞})) |
| 21 | 1, 20 | wceq 1540 |
1
wff ♯ =
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω) ∘ card) ∪ ((V ∖ Fin) ×
{+∞})) |