Detailed syntax breakdown of Definition df-xko
Step | Hyp | Ref
| Expression |
1 | | cxko 22458 |
. 2
class
↑ko |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | vr |
. . 3
setvar 𝑟 |
4 | | ctop 21790 |
. . 3
class
Top |
5 | | vk |
. . . . . . 7
setvar 𝑘 |
6 | | vv |
. . . . . . 7
setvar 𝑣 |
7 | 3 | cv 1542 |
. . . . . . . . . 10
class 𝑟 |
8 | | vx |
. . . . . . . . . . 11
setvar 𝑥 |
9 | 8 | cv 1542 |
. . . . . . . . . 10
class 𝑥 |
10 | | crest 16925 |
. . . . . . . . . 10
class
↾t |
11 | 7, 9, 10 | co 7213 |
. . . . . . . . 9
class (𝑟 ↾t 𝑥) |
12 | | ccmp 22283 |
. . . . . . . . 9
class
Comp |
13 | 11, 12 | wcel 2110 |
. . . . . . . 8
wff (𝑟 ↾t 𝑥) ∈ Comp |
14 | 7 | cuni 4819 |
. . . . . . . . 9
class ∪ 𝑟 |
15 | 14 | cpw 4513 |
. . . . . . . 8
class 𝒫
∪ 𝑟 |
16 | 13, 8, 15 | crab 3065 |
. . . . . . 7
class {𝑥 ∈ 𝒫 ∪ 𝑟
∣ (𝑟
↾t 𝑥)
∈ Comp} |
17 | 2 | cv 1542 |
. . . . . . 7
class 𝑠 |
18 | | vf |
. . . . . . . . . . 11
setvar 𝑓 |
19 | 18 | cv 1542 |
. . . . . . . . . 10
class 𝑓 |
20 | 5 | cv 1542 |
. . . . . . . . . 10
class 𝑘 |
21 | 19, 20 | cima 5554 |
. . . . . . . . 9
class (𝑓 “ 𝑘) |
22 | 6 | cv 1542 |
. . . . . . . . 9
class 𝑣 |
23 | 21, 22 | wss 3866 |
. . . . . . . 8
wff (𝑓 “ 𝑘) ⊆ 𝑣 |
24 | | ccn 22121 |
. . . . . . . . 9
class
Cn |
25 | 7, 17, 24 | co 7213 |
. . . . . . . 8
class (𝑟 Cn 𝑠) |
26 | 23, 18, 25 | crab 3065 |
. . . . . . 7
class {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} |
27 | 5, 6, 16, 17, 26 | cmpo 7215 |
. . . . . 6
class (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟
∣ (𝑟
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
28 | 27 | crn 5552 |
. . . . 5
class ran
(𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟
∣ (𝑟
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
29 | | cfi 9026 |
. . . . 5
class
fi |
30 | 28, 29 | cfv 6380 |
. . . 4
class
(fi‘ran (𝑘
∈ {𝑥 ∈ 𝒫
∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) |
31 | | ctg 16942 |
. . . 4
class
topGen |
32 | 30, 31 | cfv 6380 |
. . 3
class
(topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟
∣ (𝑟
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) |
33 | 2, 3, 4, 4, 32 | cmpo 7215 |
. 2
class (𝑠 ∈ Top, 𝑟 ∈ Top ↦
(topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟
∣ (𝑟
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})))) |
34 | 1, 33 | wceq 1543 |
1
wff
↑ko = (𝑠
∈ Top, 𝑟 ∈ Top
↦ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟
∣ (𝑟
↾t 𝑥)
∈ Comp}, 𝑣 ∈
𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})))) |