Detailed syntax breakdown of Definition df-1stc
Step | Hyp | Ref
| Expression |
1 | | c1stc 22569 |
. 2
class
1stω |
2 | | vy |
. . . . . . . 8
setvar 𝑦 |
3 | 2 | cv 1540 |
. . . . . . 7
class 𝑦 |
4 | | com 7700 |
. . . . . . 7
class
ω |
5 | | cdom 8705 |
. . . . . . 7
class
≼ |
6 | 3, 4, 5 | wbr 5078 |
. . . . . 6
wff 𝑦 ≼
ω |
7 | | vx |
. . . . . . . . 9
setvar 𝑥 |
8 | | vz |
. . . . . . . . 9
setvar 𝑧 |
9 | 7, 8 | wel 2110 |
. . . . . . . 8
wff 𝑥 ∈ 𝑧 |
10 | 7 | cv 1540 |
. . . . . . . . 9
class 𝑥 |
11 | 8 | cv 1540 |
. . . . . . . . . . . 12
class 𝑧 |
12 | 11 | cpw 4538 |
. . . . . . . . . . 11
class 𝒫
𝑧 |
13 | 3, 12 | cin 3890 |
. . . . . . . . . 10
class (𝑦 ∩ 𝒫 𝑧) |
14 | 13 | cuni 4844 |
. . . . . . . . 9
class ∪ (𝑦
∩ 𝒫 𝑧) |
15 | 10, 14 | wcel 2109 |
. . . . . . . 8
wff 𝑥 ∈ ∪ (𝑦
∩ 𝒫 𝑧) |
16 | 9, 15 | wi 4 |
. . . . . . 7
wff (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)) |
17 | | vj |
. . . . . . . 8
setvar 𝑗 |
18 | 17 | cv 1540 |
. . . . . . 7
class 𝑗 |
19 | 16, 8, 18 | wral 3065 |
. . . . . 6
wff
∀𝑧 ∈
𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)) |
20 | 6, 19 | wa 395 |
. . . . 5
wff (𝑦 ≼ ω ∧
∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧))) |
21 | 18 | cpw 4538 |
. . . . 5
class 𝒫
𝑗 |
22 | 20, 2, 21 | wrex 3066 |
. . . 4
wff
∃𝑦 ∈
𝒫 𝑗(𝑦 ≼ ω ∧
∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧))) |
23 | 18 | cuni 4844 |
. . . 4
class ∪ 𝑗 |
24 | 22, 7, 23 | wral 3065 |
. . 3
wff
∀𝑥 ∈
∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧))) |
25 | | ctop 22023 |
. . 3
class
Top |
26 | 24, 17, 25 | crab 3069 |
. 2
class {𝑗 ∈ Top ∣
∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))} |
27 | 1, 26 | wceq 1541 |
1
wff
1stω = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))} |