Step |
Hyp |
Ref |
Expression |
1 |
|
2ndctop |
⊢ ( 𝐽 ∈ 2ndω → 𝐽 ∈ Top ) |
2 |
|
is2ndc |
⊢ ( 𝐽 ∈ 2ndω ↔ ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) ) |
3 |
|
ssrab2 |
⊢ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ⊆ 𝑏 |
4 |
|
bastg |
⊢ ( 𝑏 ∈ TopBases → 𝑏 ⊆ ( topGen ‘ 𝑏 ) ) |
5 |
4
|
3ad2ant1 |
⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) ) → 𝑏 ⊆ ( topGen ‘ 𝑏 ) ) |
6 |
3 5
|
sstrid |
⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) ) → { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ⊆ ( topGen ‘ 𝑏 ) ) |
7 |
|
fvex |
⊢ ( topGen ‘ 𝑏 ) ∈ V |
8 |
7
|
elpw2 |
⊢ ( { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ∈ 𝒫 ( topGen ‘ 𝑏 ) ↔ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ⊆ ( topGen ‘ 𝑏 ) ) |
9 |
6 8
|
sylibr |
⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) ) → { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ∈ 𝒫 ( topGen ‘ 𝑏 ) ) |
10 |
|
vex |
⊢ 𝑏 ∈ V |
11 |
|
ssdomg |
⊢ ( 𝑏 ∈ V → ( { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ⊆ 𝑏 → { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ≼ 𝑏 ) ) |
12 |
10 3 11
|
mp2 |
⊢ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ≼ 𝑏 |
13 |
|
simp2 |
⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) ) → 𝑏 ≼ ω ) |
14 |
|
domtr |
⊢ ( ( { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ≼ 𝑏 ∧ 𝑏 ≼ ω ) → { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ≼ ω ) |
15 |
12 13 14
|
sylancr |
⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) ) → { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ≼ ω ) |
16 |
|
eltg2b |
⊢ ( 𝑏 ∈ TopBases → ( 𝑜 ∈ ( topGen ‘ 𝑏 ) ↔ ∀ 𝑦 ∈ 𝑜 ∃ 𝑡 ∈ 𝑏 ( 𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) ) ) |
17 |
16
|
3ad2ant1 |
⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) ) → ( 𝑜 ∈ ( topGen ‘ 𝑏 ) ↔ ∀ 𝑦 ∈ 𝑜 ∃ 𝑡 ∈ 𝑏 ( 𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) ) ) |
18 |
|
elequ1 |
⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝑡 ↔ 𝑥 ∈ 𝑡 ) ) |
19 |
18
|
anbi1d |
⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) ↔ ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) ) ) |
20 |
19
|
rexbidv |
⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑡 ∈ 𝑏 ( 𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) ↔ ∃ 𝑡 ∈ 𝑏 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) ) ) |
21 |
20
|
rspccv |
⊢ ( ∀ 𝑦 ∈ 𝑜 ∃ 𝑡 ∈ 𝑏 ( 𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) → ( 𝑥 ∈ 𝑜 → ∃ 𝑡 ∈ 𝑏 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) ) ) |
22 |
|
id |
⊢ ( ( 𝑡 ∈ 𝑏 ∧ 𝑥 ∈ 𝑡 ) → ( 𝑡 ∈ 𝑏 ∧ 𝑥 ∈ 𝑡 ) ) |
23 |
22
|
adantrr |
⊢ ( ( 𝑡 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) ) → ( 𝑡 ∈ 𝑏 ∧ 𝑥 ∈ 𝑡 ) ) |
24 |
|
elequ2 |
⊢ ( 𝑞 = 𝑡 → ( 𝑥 ∈ 𝑞 ↔ 𝑥 ∈ 𝑡 ) ) |
25 |
24
|
elrab |
⊢ ( 𝑡 ∈ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ↔ ( 𝑡 ∈ 𝑏 ∧ 𝑥 ∈ 𝑡 ) ) |
26 |
23 25
|
sylibr |
⊢ ( ( 𝑡 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) ) → 𝑡 ∈ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ) |
27 |
|
simprr |
⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) ) ∧ ( 𝑡 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) ) ) → ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) ) |
28 |
|
elequ2 |
⊢ ( 𝑝 = 𝑡 → ( 𝑥 ∈ 𝑝 ↔ 𝑥 ∈ 𝑡 ) ) |
29 |
|
sseq1 |
⊢ ( 𝑝 = 𝑡 → ( 𝑝 ⊆ 𝑜 ↔ 𝑡 ⊆ 𝑜 ) ) |
30 |
28 29
|
anbi12d |
⊢ ( 𝑝 = 𝑡 → ( ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ↔ ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) ) ) |
31 |
30
|
rspcev |
⊢ ( ( 𝑡 ∈ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ∧ ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) ) → ∃ 𝑝 ∈ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) |
32 |
26 27 31
|
syl2an2 |
⊢ ( ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) ) ∧ ( 𝑡 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) ) ) → ∃ 𝑝 ∈ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) |
33 |
32
|
rexlimdvaa |
⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) ) → ( ∃ 𝑡 ∈ 𝑏 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) → ∃ 𝑝 ∈ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) |
34 |
21 33
|
syl9r |
⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) ) → ( ∀ 𝑦 ∈ 𝑜 ∃ 𝑡 ∈ 𝑏 ( 𝑦 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑜 ) → ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) |
35 |
17 34
|
sylbid |
⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) ) → ( 𝑜 ∈ ( topGen ‘ 𝑏 ) → ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) |
36 |
35
|
ralrimiv |
⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) ) → ∀ 𝑜 ∈ ( topGen ‘ 𝑏 ) ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) |
37 |
|
breq1 |
⊢ ( 𝑠 = { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } → ( 𝑠 ≼ ω ↔ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ≼ ω ) ) |
38 |
|
rexeq |
⊢ ( 𝑠 = { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } → ( ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ↔ ∃ 𝑝 ∈ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) |
39 |
38
|
imbi2d |
⊢ ( 𝑠 = { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } → ( ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ↔ ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) |
40 |
39
|
ralbidv |
⊢ ( 𝑠 = { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } → ( ∀ 𝑜 ∈ ( topGen ‘ 𝑏 ) ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ↔ ∀ 𝑜 ∈ ( topGen ‘ 𝑏 ) ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) |
41 |
37 40
|
anbi12d |
⊢ ( 𝑠 = { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } → ( ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ ( topGen ‘ 𝑏 ) ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ↔ ( { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ≼ ω ∧ ∀ 𝑜 ∈ ( topGen ‘ 𝑏 ) ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) ) |
42 |
41
|
rspcev |
⊢ ( ( { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ∈ 𝒫 ( topGen ‘ 𝑏 ) ∧ ( { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ≼ ω ∧ ∀ 𝑜 ∈ ( topGen ‘ 𝑏 ) ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ { 𝑞 ∈ 𝑏 ∣ 𝑥 ∈ 𝑞 } ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) → ∃ 𝑠 ∈ 𝒫 ( topGen ‘ 𝑏 ) ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ ( topGen ‘ 𝑏 ) ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) |
43 |
9 15 36 42
|
syl12anc |
⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ∧ 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) ) → ∃ 𝑠 ∈ 𝒫 ( topGen ‘ 𝑏 ) ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ ( topGen ‘ 𝑏 ) ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) |
44 |
43
|
3expia |
⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) → ( 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) → ∃ 𝑠 ∈ 𝒫 ( topGen ‘ 𝑏 ) ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ ( topGen ‘ 𝑏 ) ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) ) |
45 |
|
unieq |
⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ∪ ( topGen ‘ 𝑏 ) = ∪ 𝐽 ) |
46 |
45
|
eleq2d |
⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ( 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) ↔ 𝑥 ∈ ∪ 𝐽 ) ) |
47 |
|
pweq |
⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → 𝒫 ( topGen ‘ 𝑏 ) = 𝒫 𝐽 ) |
48 |
|
raleq |
⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ∀ 𝑜 ∈ ( topGen ‘ 𝑏 ) ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) |
49 |
48
|
anbi2d |
⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ ( topGen ‘ 𝑏 ) ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ↔ ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) ) |
50 |
47 49
|
rexeqbidv |
⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ∃ 𝑠 ∈ 𝒫 ( topGen ‘ 𝑏 ) ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ ( topGen ‘ 𝑏 ) ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ↔ ∃ 𝑠 ∈ 𝒫 𝐽 ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) ) |
51 |
46 50
|
imbi12d |
⊢ ( ( topGen ‘ 𝑏 ) = 𝐽 → ( ( 𝑥 ∈ ∪ ( topGen ‘ 𝑏 ) → ∃ 𝑠 ∈ 𝒫 ( topGen ‘ 𝑏 ) ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ ( topGen ‘ 𝑏 ) ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) ↔ ( 𝑥 ∈ ∪ 𝐽 → ∃ 𝑠 ∈ 𝒫 𝐽 ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) ) ) |
52 |
44 51
|
syl5ibcom |
⊢ ( ( 𝑏 ∈ TopBases ∧ 𝑏 ≼ ω ) → ( ( topGen ‘ 𝑏 ) = 𝐽 → ( 𝑥 ∈ ∪ 𝐽 → ∃ 𝑠 ∈ 𝒫 𝐽 ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) ) ) |
53 |
52
|
expimpd |
⊢ ( 𝑏 ∈ TopBases → ( ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) → ( 𝑥 ∈ ∪ 𝐽 → ∃ 𝑠 ∈ 𝒫 𝐽 ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) ) ) |
54 |
53
|
rexlimiv |
⊢ ( ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝐽 ) → ( 𝑥 ∈ ∪ 𝐽 → ∃ 𝑠 ∈ 𝒫 𝐽 ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) ) |
55 |
2 54
|
sylbi |
⊢ ( 𝐽 ∈ 2ndω → ( 𝑥 ∈ ∪ 𝐽 → ∃ 𝑠 ∈ 𝒫 𝐽 ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) ) |
56 |
55
|
ralrimiv |
⊢ ( 𝐽 ∈ 2ndω → ∀ 𝑥 ∈ ∪ 𝐽 ∃ 𝑠 ∈ 𝒫 𝐽 ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) |
57 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
58 |
57
|
is1stc2 |
⊢ ( 𝐽 ∈ 1stω ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ ∪ 𝐽 ∃ 𝑠 ∈ 𝒫 𝐽 ( 𝑠 ≼ ω ∧ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → ∃ 𝑝 ∈ 𝑠 ( 𝑥 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑜 ) ) ) ) ) |
59 |
1 56 58
|
sylanbrc |
⊢ ( 𝐽 ∈ 2ndω → 𝐽 ∈ 1stω ) |