Detailed syntax breakdown of Definition df-kgen
Step | Hyp | Ref
| Expression |
1 | | ckgen 22682 |
. 2
class
𝑘Gen |
2 | | vj |
. . 3
setvar 𝑗 |
3 | | ctop 22040 |
. . 3
class
Top |
4 | 2 | cv 1541 |
. . . . . . . 8
class 𝑗 |
5 | | vk |
. . . . . . . . 9
setvar 𝑘 |
6 | 5 | cv 1541 |
. . . . . . . 8
class 𝑘 |
7 | | crest 17129 |
. . . . . . . 8
class
↾t |
8 | 4, 6, 7 | co 7271 |
. . . . . . 7
class (𝑗 ↾t 𝑘) |
9 | | ccmp 22535 |
. . . . . . 7
class
Comp |
10 | 8, 9 | wcel 2110 |
. . . . . 6
wff (𝑗 ↾t 𝑘) ∈ Comp |
11 | | vx |
. . . . . . . . 9
setvar 𝑥 |
12 | 11 | cv 1541 |
. . . . . . . 8
class 𝑥 |
13 | 12, 6 | cin 3891 |
. . . . . . 7
class (𝑥 ∩ 𝑘) |
14 | 13, 8 | wcel 2110 |
. . . . . 6
wff (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘) |
15 | 10, 14 | wi 4 |
. . . . 5
wff ((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘)) |
16 | 4 | cuni 4845 |
. . . . . 6
class ∪ 𝑗 |
17 | 16 | cpw 4539 |
. . . . 5
class 𝒫
∪ 𝑗 |
18 | 15, 5, 17 | wral 3066 |
. . . 4
wff
∀𝑘 ∈
𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘)) |
19 | 18, 11, 17 | crab 3070 |
. . 3
class {𝑥 ∈ 𝒫 ∪ 𝑗
∣ ∀𝑘 ∈
𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))} |
20 | 2, 3, 19 | cmpt 5162 |
. 2
class (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗
∣ ∀𝑘 ∈
𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))}) |
21 | 1, 20 | wceq 1542 |
1
wff
𝑘Gen = (𝑗
∈ Top ↦ {𝑥
∈ 𝒫 ∪ 𝑗 ∣ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))}) |