Detailed syntax breakdown of Definition df-oexp
Step | Hyp | Ref
| Expression |
1 | | coe 7559 |
. 2
class
↑𝑜 |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | con0 5723 |
. . 3
class
On |
5 | 2 | cv 1482 |
. . . . 5
class 𝑥 |
6 | | c0 3915 |
. . . . 5
class
∅ |
7 | 5, 6 | wceq 1483 |
. . . 4
wff 𝑥 = ∅ |
8 | | c1o 7553 |
. . . . 5
class
1𝑜 |
9 | 3 | cv 1482 |
. . . . 5
class 𝑦 |
10 | 8, 9 | cdif 3571 |
. . . 4
class
(1𝑜 ∖ 𝑦) |
11 | | vz |
. . . . . . 7
setvar 𝑧 |
12 | | cvv 3200 |
. . . . . . 7
class
V |
13 | 11 | cv 1482 |
. . . . . . . 8
class 𝑧 |
14 | | comu 7558 |
. . . . . . . 8
class
·𝑜 |
15 | 13, 5, 14 | co 6650 |
. . . . . . 7
class (𝑧 ·𝑜
𝑥) |
16 | 11, 12, 15 | cmpt 4729 |
. . . . . 6
class (𝑧 ∈ V ↦ (𝑧 ·𝑜
𝑥)) |
17 | 16, 8 | crdg 7505 |
. . . . 5
class
rec((𝑧 ∈ V
↦ (𝑧
·𝑜 𝑥)), 1𝑜) |
18 | 9, 17 | cfv 5888 |
. . . 4
class
(rec((𝑧 ∈ V
↦ (𝑧
·𝑜 𝑥)), 1𝑜)‘𝑦) |
19 | 7, 10, 18 | cif 4086 |
. . 3
class if(𝑥 = ∅,
(1𝑜 ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·𝑜 𝑥)),
1𝑜)‘𝑦)) |
20 | 2, 3, 4, 4, 19 | cmpt2 6652 |
. 2
class (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1𝑜 ∖
𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·𝑜
𝑥)),
1𝑜)‘𝑦))) |
21 | 1, 20 | wceq 1483 |
1
wff
↑𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1𝑜 ∖
𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·𝑜
𝑥)),
1𝑜)‘𝑦))) |