Metamath Proof Explorer

Theorem 2ndc1stc

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

Ref Expression
Assertion 2ndc1stc ⊢J∈2nd𝜔→J∈1st𝜔

Proof

Step Hyp Ref Expression
1 2ndctop ⊢J∈2nd𝜔→J∈Top
2 is2ndc ⊢J∈2nd𝜔↔∃b∈TopBasesb≼ω∧topGen⁡b=J
3 ssrab2 ⊢q∈b|x∈q⊆b
4 bastg ⊢b∈TopBases→b⊆topGen⁡b
5 4 3ad2ant1 ⊢b∈TopBases∧b≼ω∧x∈⋃topGen⁡b→b⊆topGen⁡b
6 3 5 sstrid ⊢b∈TopBases∧b≼ω∧x∈⋃topGen⁡b→q∈b|x∈q⊆topGen⁡b
7 fvex ⊢topGen⁡b∈V
8 7 elpw2 ⊢q∈b|x∈q∈𝒫topGen⁡b↔q∈b|x∈q⊆topGen⁡b
9 6 8 sylibr ⊢b∈TopBases∧b≼ω∧x∈⋃topGen⁡b→q∈b|x∈q∈𝒫topGen⁡b
10 vex ⊢b∈V
11 ssdomg ⊢b∈V→q∈b|x∈q⊆b→q∈b|x∈q≼b
12 10 3 11 mp2 ⊢q∈b|x∈q≼b
13 simp2 ⊢b∈TopBases∧b≼ω∧x∈⋃topGen⁡b→b≼ω
14 domtr ⊢q∈b|x∈q≼b∧b≼ω→q∈b|x∈q≼ω
15 12 13 14 sylancr ⊢b∈TopBases∧b≼ω∧x∈⋃topGen⁡b→q∈b|x∈q≼ω
16 eltg2b ⊢b∈TopBases→o∈topGen⁡b↔∀y∈o∃t∈by∈t∧t⊆o
17 16 3ad2ant1 ⊢b∈TopBases∧b≼ω∧x∈⋃topGen⁡b→o∈topGen⁡b↔∀y∈o∃t∈by∈t∧t⊆o
18 elequ1 ⊢y=x→y∈t↔x∈t
19 18 anbi1d ⊢y=x→y∈t∧t⊆o↔x∈t∧t⊆o
20 19 rexbidv ⊢y=x→∃t∈by∈t∧t⊆o↔∃t∈bx∈t∧t⊆o
21 20 rspccv ⊢∀y∈o∃t∈by∈t∧t⊆o→x∈o→∃t∈bx∈t∧t⊆o
22 id ⊢t∈b∧x∈t→t∈b∧x∈t
23 22 adantrr ⊢t∈b∧x∈t∧t⊆o→t∈b∧x∈t
24 elequ2 ⊢q=t→x∈q↔x∈t
25 24 elrab ⊢t∈q∈b|x∈q↔t∈b∧x∈t
26 23 25 sylibr ⊢t∈b∧x∈t∧t⊆o→t∈q∈b|x∈q
27 simprr ⊢b∈TopBases∧b≼ω∧x∈⋃topGen⁡b∧t∈b∧x∈t∧t⊆o→x∈t∧t⊆o
28 elequ2 ⊢p=t→x∈p↔x∈t
29 sseq1 ⊢p=t→p⊆o↔t⊆o
30 28 29 anbi12d ⊢p=t→x∈p∧p⊆o↔x∈t∧t⊆o
31 30 rspcev ⊢t∈q∈b|x∈q∧x∈t∧t⊆o→∃p∈q∈b|x∈qx∈p∧p⊆o
32 26 27 31 syl2an2 ⊢b∈TopBases∧b≼ω∧x∈⋃topGen⁡b∧t∈b∧x∈t∧t⊆o→∃p∈q∈b|x∈qx∈p∧p⊆o
33 32 rexlimdvaa ⊢b∈TopBases∧b≼ω∧x∈⋃topGen⁡b→∃t∈bx∈t∧t⊆o→∃p∈q∈b|x∈qx∈p∧p⊆o
34 21 33 syl9r ⊢b∈TopBases∧b≼ω∧x∈⋃topGen⁡b→∀y∈o∃t∈by∈t∧t⊆o→x∈o→∃p∈q∈b|x∈qx∈p∧p⊆o
35 17 34 sylbid ⊢b∈TopBases∧b≼ω∧x∈⋃topGen⁡b→o∈topGen⁡b→x∈o→∃p∈q∈b|x∈qx∈p∧p⊆o
36 35 ralrimiv ⊢b∈TopBases∧b≼ω∧x∈⋃topGen⁡b→∀o∈topGen⁡bx∈o→∃p∈q∈b|x∈qx∈p∧p⊆o
37 breq1 ⊢s=q∈b|x∈q→s≼ω↔q∈b|x∈q≼ω
38 rexeq ⊢s=q∈b|x∈q→∃p∈sx∈p∧p⊆o↔∃p∈q∈b|x∈qx∈p∧p⊆o
39 38 imbi2d ⊢s=q∈b|x∈q→x∈o→∃p∈sx∈p∧p⊆o↔x∈o→∃p∈q∈b|x∈qx∈p∧p⊆o
40 39 ralbidv ⊢s=q∈b|x∈q→∀o∈topGen⁡bx∈o→∃p∈sx∈p∧p⊆o↔∀o∈topGen⁡bx∈o→∃p∈q∈b|x∈qx∈p∧p⊆o
41 37 40 anbi12d ⊢s=q∈b|x∈q→s≼ω∧∀o∈topGen⁡bx∈o→∃p∈sx∈p∧p⊆o↔q∈b|x∈q≼ω∧∀o∈topGen⁡bx∈o→∃p∈q∈b|x∈qx∈p∧p⊆o
42 41 rspcev ⊢q∈b|x∈q∈𝒫topGen⁡b∧q∈b|x∈q≼ω∧∀o∈topGen⁡bx∈o→∃p∈q∈b|x∈qx∈p∧p⊆o→∃s∈𝒫topGen⁡bs≼ω∧∀o∈topGen⁡bx∈o→∃p∈sx∈p∧p⊆o
43 9 15 36 42 syl12anc ⊢b∈TopBases∧b≼ω∧x∈⋃topGen⁡b→∃s∈𝒫topGen⁡bs≼ω∧∀o∈topGen⁡bx∈o→∃p∈sx∈p∧p⊆o
44 43 3expia ⊢b∈TopBases∧b≼ω→x∈⋃topGen⁡b→∃s∈𝒫topGen⁡bs≼ω∧∀o∈topGen⁡bx∈o→∃p∈sx∈p∧p⊆o
45 unieq ⊢topGen⁡b=J→⋃topGen⁡b=⋃J
46 45 eleq2d ⊢topGen⁡b=J→x∈⋃topGen⁡b↔x∈⋃J
47 pweq ⊢topGen⁡b=J→𝒫topGen⁡b=𝒫J
48 raleq ⊢topGen⁡b=J→∀o∈topGen⁡bx∈o→∃p∈sx∈p∧p⊆o↔∀o∈Jx∈o→∃p∈sx∈p∧p⊆o
49 48 anbi2d ⊢topGen⁡b=J→s≼ω∧∀o∈topGen⁡bx∈o→∃p∈sx∈p∧p⊆o↔s≼ω∧∀o∈Jx∈o→∃p∈sx∈p∧p⊆o
50 47 49 rexeqbidv ⊢topGen⁡b=J→∃s∈𝒫topGen⁡bs≼ω∧∀o∈topGen⁡bx∈o→∃p∈sx∈p∧p⊆o↔∃s∈𝒫Js≼ω∧∀o∈Jx∈o→∃p∈sx∈p∧p⊆o
51 46 50 imbi12d ⊢topGen⁡b=J→x∈⋃topGen⁡b→∃s∈𝒫topGen⁡bs≼ω∧∀o∈topGen⁡bx∈o→∃p∈sx∈p∧p⊆o↔x∈⋃J→∃s∈𝒫Js≼ω∧∀o∈Jx∈o→∃p∈sx∈p∧p⊆o
52 44 51 syl5ibcom ⊢b∈TopBases∧b≼ω→topGen⁡b=J→x∈⋃J→∃s∈𝒫Js≼ω∧∀o∈Jx∈o→∃p∈sx∈p∧p⊆o
53 52 expimpd ⊢b∈TopBases→b≼ω∧topGen⁡b=J→x∈⋃J→∃s∈𝒫Js≼ω∧∀o∈Jx∈o→∃p∈sx∈p∧p⊆o
54 53 rexlimiv ⊢∃b∈TopBasesb≼ω∧topGen⁡b=J→x∈⋃J→∃s∈𝒫Js≼ω∧∀o∈Jx∈o→∃p∈sx∈p∧p⊆o
55 2 54 sylbi ⊢J∈2nd𝜔→x∈⋃J→∃s∈𝒫Js≼ω∧∀o∈Jx∈o→∃p∈sx∈p∧p⊆o
56 55 ralrimiv ⊢J∈2nd𝜔→∀x∈⋃J∃s∈𝒫Js≼ω∧∀o∈Jx∈o→∃p∈sx∈p∧p⊆o
57 eqid ⊢⋃J=⋃J
58 57 is1stc2 ⊢J∈1st𝜔↔J∈Top∧∀x∈⋃J∃s∈𝒫Js≼ω∧∀o∈Jx∈o→∃p∈sx∈p∧p⊆o
59 1 56 58 sylanbrc ⊢J∈2nd𝜔→J∈1st𝜔