Detailed syntax breakdown of Definition df-made
Step | Hyp | Ref
| Expression |
1 | | cmade 33667 |
. 2
class
M |
2 | | vf |
. . . 4
setvar 𝑓 |
3 | | cvv 3398 |
. . . 4
class
V |
4 | | cscut 33618 |
. . . . 5
class
|s |
5 | 2 | cv 1541 |
. . . . . . . . 9
class 𝑓 |
6 | 5 | crn 5526 |
. . . . . . . 8
class ran 𝑓 |
7 | 6 | cuni 4796 |
. . . . . . 7
class ∪ ran 𝑓 |
8 | 7 | cpw 4488 |
. . . . . 6
class 𝒫
∪ ran 𝑓 |
9 | 8, 8 | cxp 5523 |
. . . . 5
class
(𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓) |
10 | 4, 9 | cima 5528 |
. . . 4
class ( |s
“ (𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓)) |
11 | 2, 3, 10 | cmpt 5110 |
. . 3
class (𝑓 ∈ V ↦ ( |s “
(𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓))) |
12 | 11 | crecs 8036 |
. 2
class
recs((𝑓 ∈ V
↦ ( |s “ (𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓)))) |
13 | 1, 12 | wceq 1542 |
1
wff M =
recs((𝑓 ∈ V ↦ (
|s “ (𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓)))) |