Detailed syntax breakdown of Definition df-omul
Step | Hyp | Ref
| Expression |
1 | | comu 7445 |
. 2
class
·𝑜 |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | vy |
. . 3
setvar 𝑦 |
4 | | con0 5640 |
. . 3
class
On |
5 | 3 | cv 1474 |
. . . 4
class 𝑦 |
6 | | vz |
. . . . . 6
setvar 𝑧 |
7 | | cvv 3173 |
. . . . . 6
class
V |
8 | 6 | cv 1474 |
. . . . . . 7
class 𝑧 |
9 | 2 | cv 1474 |
. . . . . . 7
class 𝑥 |
10 | | coa 7444 |
. . . . . . 7
class
+𝑜 |
11 | 8, 9, 10 | co 6549 |
. . . . . 6
class (𝑧 +𝑜 𝑥) |
12 | 6, 7, 11 | cmpt 4643 |
. . . . 5
class (𝑧 ∈ V ↦ (𝑧 +𝑜 𝑥)) |
13 | | c0 3874 |
. . . . 5
class
∅ |
14 | 12, 13 | crdg 7392 |
. . . 4
class
rec((𝑧 ∈ V
↦ (𝑧
+𝑜 𝑥)),
∅) |
15 | 5, 14 | cfv 5804 |
. . 3
class
(rec((𝑧 ∈ V
↦ (𝑧
+𝑜 𝑥)),
∅)‘𝑦) |
16 | 2, 3, 4, 4, 15 | cmpt2 6551 |
. 2
class (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +𝑜 𝑥)), ∅)‘𝑦)) |
17 | 1, 16 | wceq 1475 |
1
wff
·𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +𝑜 𝑥)), ∅)‘𝑦)) |