Detailed syntax breakdown of Definition df-hash
Step | Hyp | Ref
| Expression |
1 | | chash 12979 |
. 2
class
# |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | | cvv 3173 |
. . . . . . 7
class
V |
4 | 2 | cv 1474 |
. . . . . . . 8
class 𝑥 |
5 | | c1 9816 |
. . . . . . . 8
class
1 |
6 | | caddc 9818 |
. . . . . . . 8
class
+ |
7 | 4, 5, 6 | co 6549 |
. . . . . . 7
class (𝑥 + 1) |
8 | 2, 3, 7 | cmpt 4643 |
. . . . . 6
class (𝑥 ∈ V ↦ (𝑥 + 1)) |
9 | | cc0 9815 |
. . . . . 6
class
0 |
10 | 8, 9 | crdg 7392 |
. . . . 5
class
rec((𝑥 ∈ V
↦ (𝑥 + 1)),
0) |
11 | | com 6957 |
. . . . 5
class
ω |
12 | 10, 11 | cres 5040 |
. . . 4
class
(rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) |
13 | | ccrd 8644 |
. . . 4
class
card |
14 | 12, 13 | ccom 5042 |
. . 3
class
((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card) |
15 | | cfn 7841 |
. . . . 5
class
Fin |
16 | 3, 15 | cdif 3537 |
. . . 4
class (V
∖ Fin) |
17 | | cpnf 9950 |
. . . . 5
class
+∞ |
18 | 17 | csn 4125 |
. . . 4
class
{+∞} |
19 | 16, 18 | cxp 5036 |
. . 3
class ((V
∖ Fin) × {+∞}) |
20 | 14, 19 | cun 3538 |
. 2
class
(((rec((𝑥 ∈ V
↦ (𝑥 + 1)), 0)
↾ ω) ∘ card) ∪ ((V ∖ Fin) ×
{+∞})) |
21 | 1, 20 | wceq 1475 |
1
wff # =
(((rec((𝑥 ∈ V ↦
(𝑥 + 1)), 0) ↾
ω) ∘ card) ∪ ((V ∖ Fin) ×
{+∞})) |