Metamath Proof Explorer


Theorem 2ndcsep

Description: A second-countable topology is separable, which is to say it contains a countable dense subset. (Contributed by Mario Carneiro, 13-Apr-2015)

Ref Expression
Hypothesis 2ndcsep.1 X = J
Assertion 2ndcsep J 2 nd 𝜔 x 𝒫 X x ω cls J x = X

Proof

Step Hyp Ref Expression
1 2ndcsep.1 X = J
2 is2ndc J 2 nd 𝜔 b TopBases b ω topGen b = J
3 vex b V
4 difss b b
5 ssdomg b V b b b b
6 3 4 5 mp2 b b
7 simpr b TopBases b ω b ω
8 domtr b b b ω b ω
9 6 7 8 sylancr b TopBases b ω b ω
10 eldifsn y b y b y
11 n0 y z z y
12 elunii z y y b z b
13 simpl z y y b z y
14 12 13 jca z y y b z b z y
15 14 expcom y b z y z b z y
16 15 eximdv y b z z y z z b z y
17 16 imp y b z z y z z b z y
18 df-rex z b z y z z b z y
19 17 18 sylibr y b z z y z b z y
20 11 19 sylan2b y b y z b z y
21 10 20 sylbi y b z b z y
22 21 rgen y b z b z y
23 vuniex b V
24 eleq1 z = f y z y f y y
25 23 24 axcc4dom b ω y b z b z y f f : b b y b f y y
26 9 22 25 sylancl b TopBases b ω f f : b b y b f y y
27 frn f : b b ran f b
28 27 ad2antrl b TopBases b ω f : b b y b f y y ran f b
29 vex f V
30 29 rnex ran f V
31 30 elpw ran f 𝒫 b ran f b
32 28 31 sylibr b TopBases b ω f : b b y b f y y ran f 𝒫 b
33 omelon ω On
34 7 adantr b TopBases b ω f : b b y b f y y b ω
35 ondomen ω On b ω b dom card
36 33 34 35 sylancr b TopBases b ω f : b b y b f y y b dom card
37 ssnum b dom card b b b dom card
38 36 4 37 sylancl b TopBases b ω f : b b y b f y y b dom card
39 ffn f : b b f Fn b
40 39 ad2antrl b TopBases b ω f : b b y b f y y f Fn b
41 dffn4 f Fn b f : b onto ran f
42 40 41 sylib b TopBases b ω f : b b y b f y y f : b onto ran f
43 fodomnum b dom card f : b onto ran f ran f b
44 38 42 43 sylc b TopBases b ω f : b b y b f y y ran f b
45 9 adantr b TopBases b ω f : b b y b f y y b ω
46 domtr ran f b b ω ran f ω
47 44 45 46 syl2anc b TopBases b ω f : b b y b f y y ran f ω
48 tgcl b TopBases topGen b Top
49 48 ad2antrr b TopBases b ω f : b b y b f y y topGen b Top
50 unitg b V topGen b = b
51 50 elv topGen b = b
52 51 eqcomi b = topGen b
53 52 clsss3 topGen b Top ran f b cls topGen b ran f b
54 49 28 53 syl2anc b TopBases b ω f : b b y b f y y cls topGen b ran f b
55 ne0i x y y
56 55 anim2i y b x y y b y
57 56 10 sylibr y b x y y b
58 fnfvelrn f Fn b y b f y ran f
59 39 58 sylan f : b b y b f y ran f
60 inelcm f y y f y ran f y ran f
61 60 expcom f y ran f f y y y ran f
62 59 61 syl f : b b y b f y y y ran f
63 62 ex f : b b y b f y y y ran f
64 63 a2d f : b b y b f y y y b y ran f
65 57 64 syl7 f : b b y b f y y y b x y y ran f
66 65 exp4a f : b b y b f y y y b x y y ran f
67 66 ralimdv2 f : b b y b f y y y b x y y ran f
68 67 imp f : b b y b f y y y b x y y ran f
69 68 ad2antlr b TopBases b ω f : b b y b f y y x b y b x y y ran f
70 eqidd b TopBases b ω f : b b y b f y y x b topGen b = topGen b
71 52 a1i b TopBases b ω f : b b y b f y y x b b = topGen b
72 simplll b TopBases b ω f : b b y b f y y x b b TopBases
73 28 adantr b TopBases b ω f : b b y b f y y x b ran f b
74 simpr b TopBases b ω f : b b y b f y y x b x b
75 70 71 72 73 74 elcls3 b TopBases b ω f : b b y b f y y x b x cls topGen b ran f y b x y y ran f
76 69 75 mpbird b TopBases b ω f : b b y b f y y x b x cls topGen b ran f
77 54 76 eqelssd b TopBases b ω f : b b y b f y y cls topGen b ran f = b
78 breq1 x = ran f x ω ran f ω
79 fveqeq2 x = ran f cls topGen b x = b cls topGen b ran f = b
80 78 79 anbi12d x = ran f x ω cls topGen b x = b ran f ω cls topGen b ran f = b
81 80 rspcev ran f 𝒫 b ran f ω cls topGen b ran f = b x 𝒫 b x ω cls topGen b x = b
82 32 47 77 81 syl12anc b TopBases b ω f : b b y b f y y x 𝒫 b x ω cls topGen b x = b
83 26 82 exlimddv b TopBases b ω x 𝒫 b x ω cls topGen b x = b
84 unieq topGen b = J topGen b = J
85 84 52 1 3eqtr4g topGen b = J b = X
86 85 pweqd topGen b = J 𝒫 b = 𝒫 X
87 fveq2 topGen b = J cls topGen b = cls J
88 87 fveq1d topGen b = J cls topGen b x = cls J x
89 88 85 eqeq12d topGen b = J cls topGen b x = b cls J x = X
90 89 anbi2d topGen b = J x ω cls topGen b x = b x ω cls J x = X
91 86 90 rexeqbidv topGen b = J x 𝒫 b x ω cls topGen b x = b x 𝒫 X x ω cls J x = X
92 83 91 syl5ibcom b TopBases b ω topGen b = J x 𝒫 X x ω cls J x = X
93 92 impr b TopBases b ω topGen b = J x 𝒫 X x ω cls J x = X
94 93 rexlimiva b TopBases b ω topGen b = J x 𝒫 X x ω cls J x = X
95 2 94 sylbi J 2 nd 𝜔 x 𝒫 X x ω cls J x = X