Detailed syntax breakdown of Definition df-2ndc
Step | Hyp | Ref
| Expression |
1 | | c2ndc 22587 |
. 2
class
2ndω |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1541 |
. . . . . 6
class 𝑥 |
4 | | com 7706 |
. . . . . 6
class
ω |
5 | | cdom 8714 |
. . . . . 6
class
≼ |
6 | 3, 4, 5 | wbr 5079 |
. . . . 5
wff 𝑥 ≼
ω |
7 | | ctg 17146 |
. . . . . . 7
class
topGen |
8 | 3, 7 | cfv 6432 |
. . . . . 6
class
(topGen‘𝑥) |
9 | | vj |
. . . . . . 7
setvar 𝑗 |
10 | 9 | cv 1541 |
. . . . . 6
class 𝑗 |
11 | 8, 10 | wceq 1542 |
. . . . 5
wff
(topGen‘𝑥) =
𝑗 |
12 | 6, 11 | wa 396 |
. . . 4
wff (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝑗) |
13 | | ctb 22093 |
. . . 4
class
TopBases |
14 | 12, 2, 13 | wrex 3067 |
. . 3
wff
∃𝑥 ∈
TopBases (𝑥 ≼ ω
∧ (topGen‘𝑥) =
𝑗) |
15 | 14, 9 | cab 2717 |
. 2
class {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧
(topGen‘𝑥) = 𝑗)} |
16 | 1, 15 | wceq 1542 |
1
wff
2ndω = {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)} |