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