This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2ndc1stc

Description: A second-countable space is first-countable. (Contributed by Jeff Hankins, 17-Jan-2010)

Ref Expression
Assertion 2ndc1stc ( 𝐽 ∈ 2ndω → 𝐽 ∈ 1stω )

Proof

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ω )