Step |
Hyp |
Ref |
Expression |
1 |
|
snex |
⊢ { 𝑥 } ∈ V |
2 |
|
distop |
⊢ ( { 𝑥 } ∈ V → 𝒫 { 𝑥 } ∈ Top ) |
3 |
1 2
|
ax-mp |
⊢ 𝒫 { 𝑥 } ∈ Top |
4 |
|
tgtop |
⊢ ( 𝒫 { 𝑥 } ∈ Top → ( topGen ‘ 𝒫 { 𝑥 } ) = 𝒫 { 𝑥 } ) |
5 |
3 4
|
ax-mp |
⊢ ( topGen ‘ 𝒫 { 𝑥 } ) = 𝒫 { 𝑥 } |
6 |
|
topbas |
⊢ ( 𝒫 { 𝑥 } ∈ Top → 𝒫 { 𝑥 } ∈ TopBases ) |
7 |
3 6
|
ax-mp |
⊢ 𝒫 { 𝑥 } ∈ TopBases |
8 |
|
snfi |
⊢ { 𝑥 } ∈ Fin |
9 |
|
pwfi |
⊢ ( { 𝑥 } ∈ Fin ↔ 𝒫 { 𝑥 } ∈ Fin ) |
10 |
8 9
|
mpbi |
⊢ 𝒫 { 𝑥 } ∈ Fin |
11 |
|
isfinite |
⊢ ( 𝒫 { 𝑥 } ∈ Fin ↔ 𝒫 { 𝑥 } ≺ ω ) |
12 |
10 11
|
mpbi |
⊢ 𝒫 { 𝑥 } ≺ ω |
13 |
|
sdomdom |
⊢ ( 𝒫 { 𝑥 } ≺ ω → 𝒫 { 𝑥 } ≼ ω ) |
14 |
12 13
|
ax-mp |
⊢ 𝒫 { 𝑥 } ≼ ω |
15 |
|
2ndci |
⊢ ( ( 𝒫 { 𝑥 } ∈ TopBases ∧ 𝒫 { 𝑥 } ≼ ω ) → ( topGen ‘ 𝒫 { 𝑥 } ) ∈ 2ndω ) |
16 |
7 14 15
|
mp2an |
⊢ ( topGen ‘ 𝒫 { 𝑥 } ) ∈ 2ndω |
17 |
5 16
|
eqeltrri |
⊢ 𝒫 { 𝑥 } ∈ 2ndω |
18 |
|
2ndc1stc |
⊢ ( 𝒫 { 𝑥 } ∈ 2ndω → 𝒫 { 𝑥 } ∈ 1stω ) |
19 |
17 18
|
ax-mp |
⊢ 𝒫 { 𝑥 } ∈ 1stω |
20 |
19
|
rgenw |
⊢ ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ 1stω |
21 |
|
dislly |
⊢ ( 𝑋 ∈ 𝑉 → ( 𝒫 𝑋 ∈ Locally 1stω ↔ ∀ 𝑥 ∈ 𝑋 𝒫 { 𝑥 } ∈ 1stω ) ) |
22 |
20 21
|
mpbiri |
⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Locally 1stω ) |
23 |
|
lly1stc |
⊢ Locally 1stω = 1stω |
24 |
22 23
|
eleqtrdi |
⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ 1stω ) |