Detailed syntax breakdown of Definition df-cn
Step | Hyp | Ref
| Expression |
1 | | ccn 12979 |
. 2
class
Cn |
2 | | vj |
. . 3
setvar 𝑗 |
3 | | vk |
. . 3
setvar 𝑘 |
4 | | ctop 12789 |
. . 3
class
Top |
5 | | vf |
. . . . . . . . 9
setvar 𝑓 |
6 | 5 | cv 1347 |
. . . . . . . 8
class 𝑓 |
7 | 6 | ccnv 4610 |
. . . . . . 7
class ◡𝑓 |
8 | | vy |
. . . . . . . 8
setvar 𝑦 |
9 | 8 | cv 1347 |
. . . . . . 7
class 𝑦 |
10 | 7, 9 | cima 4614 |
. . . . . 6
class (◡𝑓 “ 𝑦) |
11 | 2 | cv 1347 |
. . . . . 6
class 𝑗 |
12 | 10, 11 | wcel 2141 |
. . . . 5
wff (◡𝑓 “ 𝑦) ∈ 𝑗 |
13 | 3 | cv 1347 |
. . . . 5
class 𝑘 |
14 | 12, 8, 13 | wral 2448 |
. . . 4
wff
∀𝑦 ∈
𝑘 (◡𝑓 “ 𝑦) ∈ 𝑗 |
15 | 13 | cuni 3796 |
. . . . 5
class ∪ 𝑘 |
16 | 11 | cuni 3796 |
. . . . 5
class ∪ 𝑗 |
17 | | cmap 6626 |
. . . . 5
class
↑𝑚 |
18 | 15, 16, 17 | co 5853 |
. . . 4
class (∪ 𝑘
↑𝑚 ∪ 𝑗) |
19 | 14, 5, 18 | crab 2452 |
. . 3
class {𝑓 ∈ (∪ 𝑘
↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 (◡𝑓 “ 𝑦) ∈ 𝑗} |
20 | 2, 3, 4, 4, 19 | cmpo 5855 |
. 2
class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚
∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 (◡𝑓 “ 𝑦) ∈ 𝑗}) |
21 | 1, 20 | wceq 1348 |
1
wff Cn =
(𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (∪ 𝑘
↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 (◡𝑓 “ 𝑦) ∈ 𝑗}) |