Detailed syntax breakdown of Definition df-oadd
Step | Hyp | Ref
| Expression |
1 | | coa 5937 |
. 2
class
+𝑜 |
2 | | vx |
. . 3
setvar x |
3 | | vy |
. . 3
setvar y |
4 | | con0 4066 |
. . 3
class On |
5 | 3 | cv 1241 |
. . . 4
class y |
6 | | vz |
. . . . . 6
setvar z |
7 | | cvv 2551 |
. . . . . 6
class V |
8 | 6 | cv 1241 |
. . . . . . 7
class z |
9 | 8 | csuc 4068 |
. . . . . 6
class suc z |
10 | 6, 7, 9 | cmpt 3809 |
. . . . 5
class (z ∈ V ↦ suc
z) |
11 | 2 | cv 1241 |
. . . . 5
class x |
12 | 10, 11 | crdg 5896 |
. . . 4
class rec((z ∈ V ↦ suc
z), x) |
13 | 5, 12 | cfv 4845 |
. . 3
class (rec((z ∈ V ↦ suc
z), x)‘y) |
14 | 2, 3, 4, 4, 13 | cmpt2 5457 |
. 2
class (x ∈ On, y ∈ On ↦
(rec((z ∈
V ↦ suc z), x)‘y)) |
15 | 1, 14 | wceq 1242 |
1
wff +𝑜 =
(x ∈ On,
y ∈ On
↦ (rec((z ∈ V ↦ suc z), x)‘y)) |