Metamath Proof Explorer


Theorem 2ndcctbss

Description: If a topology is second-countable, every base has a countable subset which is a base. Exercise 16B2 in Willard. (Contributed by Jeff Hankins, 28-Jan-2010) (Proof shortened by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypotheses 2ndcctbss.1 J = topGen B
2ndcctbss.2 S = u v | u c v c w B u w w v
Assertion 2ndcctbss B TopBases J 2 nd 𝜔 b TopBases b ω b B J = topGen b

Proof

Step Hyp Ref Expression
1 2ndcctbss.1 J = topGen B
2 2ndcctbss.2 S = u v | u c v c w B u w w v
3 simpr B TopBases J 2 nd 𝜔 J 2 nd 𝜔
4 is2ndc J 2 nd 𝜔 c TopBases c ω topGen c = J
5 3 4 sylib B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J
6 vex c V
7 6 6 xpex c × c V
8 3simpa u c v c w B u w w v u c v c
9 8 ssopab2i u v | u c v c w B u w w v u v | u c v c
10 df-xp c × c = u v | u c v c
11 9 2 10 3sstr4i S c × c
12 ssdomg c × c V S c × c S c × c
13 7 11 12 mp2 S c × c
14 6 xpdom1 c ω c × c ω × c
15 omex ω V
16 15 xpdom2 c ω ω × c ω × ω
17 domtr c × c ω × c ω × c ω × ω c × c ω × ω
18 14 16 17 syl2anc c ω c × c ω × ω
19 xpomen ω × ω ω
20 domentr c × c ω × ω ω × ω ω c × c ω
21 18 19 20 sylancl c ω c × c ω
22 21 adantr c ω topGen c = J c × c ω
23 22 ad2antll B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J c × c ω
24 domtr S c × c c × c ω S ω
25 13 23 24 sylancr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J S ω
26 2 relopabiv Rel S
27 simpr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J x S x S
28 1st2nd Rel S x S x = 1 st x 2 nd x
29 26 27 28 sylancr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J x S x = 1 st x 2 nd x
30 29 27 eqeltrrd B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J x S 1 st x 2 nd x S
31 df-br 1 st x S 2 nd x 1 st x 2 nd x S
32 fvex 1 st x V
33 fvex 2 nd x V
34 simpl u = 1 st x v = 2 nd x u = 1 st x
35 34 eleq1d u = 1 st x v = 2 nd x u c 1 st x c
36 simpr u = 1 st x v = 2 nd x v = 2 nd x
37 36 eleq1d u = 1 st x v = 2 nd x v c 2 nd x c
38 sseq1 u = 1 st x u w 1 st x w
39 sseq2 v = 2 nd x w v w 2 nd x
40 38 39 bi2anan9 u = 1 st x v = 2 nd x u w w v 1 st x w w 2 nd x
41 40 rexbidv u = 1 st x v = 2 nd x w B u w w v w B 1 st x w w 2 nd x
42 35 37 41 3anbi123d u = 1 st x v = 2 nd x u c v c w B u w w v 1 st x c 2 nd x c w B 1 st x w w 2 nd x
43 32 33 42 2 braba 1 st x S 2 nd x 1 st x c 2 nd x c w B 1 st x w w 2 nd x
44 31 43 bitr3i 1 st x 2 nd x S 1 st x c 2 nd x c w B 1 st x w w 2 nd x
45 44 simp3bi 1 st x 2 nd x S w B 1 st x w w 2 nd x
46 30 45 syl B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J x S w B 1 st x w w 2 nd x
47 fvi B TopBases I B = B
48 47 ad3antrrr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J x S I B = B
49 48 rexeqdv B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J x S w I B 1 st x w w 2 nd x w B 1 st x w w 2 nd x
50 46 49 mpbird B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J x S w I B 1 st x w w 2 nd x
51 50 ralrimiva B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J x S w I B 1 st x w w 2 nd x
52 fvex I B V
53 sseq2 w = f x 1 st x w 1 st x f x
54 sseq1 w = f x w 2 nd x f x 2 nd x
55 53 54 anbi12d w = f x 1 st x w w 2 nd x 1 st x f x f x 2 nd x
56 52 55 axcc4dom S ω x S w I B 1 st x w w 2 nd x f f : S I B x S 1 st x f x f x 2 nd x
57 25 51 56 syl2anc B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f f : S I B x S 1 st x f x f x 2 nd x
58 47 ad2antrr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J I B = B
59 58 feq3d B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S I B f : S B
60 59 anbi1d B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S I B x S 1 st x f x f x 2 nd x f : S B x S 1 st x f x f x 2 nd x
61 2ndctop J 2 nd 𝜔 J Top
62 61 adantl B TopBases J 2 nd 𝜔 J Top
63 62 ad2antrr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x J Top
64 frn f : S B ran f B
65 64 ad2antrl B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x ran f B
66 bastg B TopBases B topGen B
67 66 ad3antrrr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x B topGen B
68 67 1 sseqtrrdi B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x B J
69 65 68 sstrd B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x ran f J
70 simprrl B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o o J
71 simprr c TopBases c ω topGen c = J topGen c = J
72 71 ad2antlr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o topGen c = J
73 70 72 eleqtrrd B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o o topGen c
74 simprrr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o t o
75 tg2 o topGen c t o d c t d d o
76 73 74 75 syl2anc B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o
77 bastg c TopBases c topGen c
78 77 ad2antrl B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J c topGen c
79 78 ad2antrr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o c topGen c
80 1 eqeq2i topGen c = J topGen c = topGen B
81 80 biimpi topGen c = J topGen c = topGen B
82 81 adantl c ω topGen c = J topGen c = topGen B
83 82 ad2antll B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J topGen c = topGen B
84 83 ad2antrr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o topGen c = topGen B
85 79 84 sseqtrd B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o c topGen B
86 simprl B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o d c
87 85 86 sseldd B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o d topGen B
88 simprrl B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o t d
89 tg2 d topGen B t d m B t m m d
90 87 88 89 syl2anc B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d
91 66 ad3antrrr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o B topGen B
92 91 ad2antrr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d B topGen B
93 72 ad2antrr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d topGen c = J
94 93 1 eqtr2di B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d topGen B = topGen c
95 92 94 sseqtrd B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d B topGen c
96 simprl B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d m B
97 95 96 sseldd B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d m topGen c
98 simprrl B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d t m
99 tg2 m topGen c t m n c t n n m
100 97 98 99 syl2anc B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d n c t n n m
101 ffn f : S B f Fn S
102 101 ad2antrr f : S B x S 1 st x f x f x 2 nd x o J t o f Fn S
103 102 ad2antlr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o f Fn S
104 103 ad2antrr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d n c t n n m f Fn S
105 simprl B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d n c t n n m n c
106 86 ad2antrr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d n c t n n m d c
107 simplrl B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d n c t n n m m B
108 simprrr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d n c t n n m n m
109 simprr m B t m m d m d
110 109 ad2antlr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d n c t n n m m d
111 sseq2 w = m n w n m
112 sseq1 w = m w d m d
113 111 112 anbi12d w = m n w w d n m m d
114 113 rspcev m B n m m d w B n w w d
115 107 108 110 114 syl12anc B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d n c t n n m w B n w w d
116 df-br n S d n d S
117 vex n V
118 vex d V
119 simpl u = n v = d u = n
120 119 eleq1d u = n v = d u c n c
121 simpr u = n v = d v = d
122 121 eleq1d u = n v = d v c d c
123 sseq1 u = n u w n w
124 sseq2 v = d w v w d
125 123 124 bi2anan9 u = n v = d u w w v n w w d
126 125 rexbidv u = n v = d w B u w w v w B n w w d
127 120 122 126 3anbi123d u = n v = d u c v c w B u w w v n c d c w B n w w d
128 117 118 127 2 braba n S d n c d c w B n w w d
129 116 128 bitr3i n d S n c d c w B n w w d
130 105 106 115 129 syl3anbrc B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d n c t n n m n d S
131 fnfvelrn f Fn S n d S f n d ran f
132 104 130 131 syl2anc B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d n c t n n m f n d ran f
133 simprl d c t d d o m B t m m d n c t n n m n c
134 simplll d c t d d o m B t m m d n c t n n m d c
135 simplrl d c t d d o m B t m m d n c t n n m m B
136 simprrr d c t d d o m B t m m d n c t n n m n m
137 109 ad2antlr d c t d d o m B t m m d n c t n n m m d
138 135 136 137 114 syl12anc d c t d d o m B t m m d n c t n n m w B n w w d
139 133 134 138 129 syl3anbrc d c t d d o m B t m m d n c t n n m n d S
140 fveq2 x = n d 1 st x = 1 st n d
141 fveq2 x = n d f x = f n d
142 140 141 sseq12d x = n d 1 st x f x 1 st n d f n d
143 fveq2 x = n d 2 nd x = 2 nd n d
144 141 143 sseq12d x = n d f x 2 nd x f n d 2 nd n d
145 142 144 anbi12d x = n d 1 st x f x f x 2 nd x 1 st n d f n d f n d 2 nd n d
146 145 rspcv n d S x S 1 st x f x f x 2 nd x 1 st n d f n d f n d 2 nd n d
147 139 146 syl d c t d d o m B t m m d n c t n n m x S 1 st x f x f x 2 nd x 1 st n d f n d f n d 2 nd n d
148 117 118 op1st 1 st n d = n
149 148 sseq1i 1 st n d f n d n f n d
150 117 118 op2nd 2 nd n d = d
151 150 sseq2i f n d 2 nd n d f n d d
152 149 151 anbi12i 1 st n d f n d f n d 2 nd n d n f n d f n d d
153 simprl d c t d d o m B t m m d n c t n n m n f n d f n d d n f n d
154 simprl n c t n n m t n
155 154 ad2antlr d c t d d o m B t m m d n c t n n m n f n d f n d d t n
156 153 155 sseldd d c t d d o m B t m m d n c t n n m n f n d f n d d t f n d
157 simprr d c t d d o m B t m m d n c t n n m n f n d f n d d f n d d
158 simplrr d c t d d o m B t m m d d o
159 158 ad2antrr d c t d d o m B t m m d n c t n n m n f n d f n d d d o
160 157 159 sstrd d c t d d o m B t m m d n c t n n m n f n d f n d d f n d o
161 156 160 jca d c t d d o m B t m m d n c t n n m n f n d f n d d t f n d f n d o
162 161 ex d c t d d o m B t m m d n c t n n m n f n d f n d d t f n d f n d o
163 152 162 syl5bi d c t d d o m B t m m d n c t n n m 1 st n d f n d f n d 2 nd n d t f n d f n d o
164 147 163 syldc x S 1 st x f x f x 2 nd x d c t d d o m B t m m d n c t n n m t f n d f n d o
165 164 exp4c x S 1 st x f x f x 2 nd x d c t d d o m B t m m d n c t n n m t f n d f n d o
166 165 ad2antlr f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d n c t n n m t f n d f n d o
167 166 adantl B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d n c t n n m t f n d f n d o
168 167 imp41 B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d n c t n n m t f n d f n d o
169 eleq2 b = f n d t b t f n d
170 sseq1 b = f n d b o f n d o
171 169 170 anbi12d b = f n d t b b o t f n d f n d o
172 171 rspcev f n d ran f t f n d f n d o b ran f t b b o
173 132 168 172 syl2anc B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d n c t n n m b ran f t b b o
174 100 173 rexlimddv B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o m B t m m d b ran f t b b o
175 90 174 rexlimddv B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o d c t d d o b ran f t b b o
176 76 175 rexlimddv B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o b ran f t b b o
177 176 expr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o b ran f t b b o
178 177 ralrimivv B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x o J t o b ran f t b b o
179 basgen2 J Top ran f J o J t o b ran f t b b o topGen ran f = J
180 63 69 178 179 syl3anc B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x topGen ran f = J
181 180 63 eqeltrd B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x topGen ran f Top
182 tgclb ran f TopBases topGen ran f Top
183 181 182 sylibr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x ran f TopBases
184 omelon ω On
185 25 adantr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x S ω
186 ondomen ω On S ω S dom card
187 184 185 186 sylancr B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x S dom card
188 101 ad2antrl B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x f Fn S
189 dffn4 f Fn S f : S onto ran f
190 188 189 sylib B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x f : S onto ran f
191 fodomnum S dom card f : S onto ran f ran f S
192 187 190 191 sylc B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x ran f S
193 domtr ran f S S ω ran f ω
194 192 185 193 syl2anc B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x ran f ω
195 180 eqcomd B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x J = topGen ran f
196 breq1 b = ran f b ω ran f ω
197 sseq1 b = ran f b B ran f B
198 fveq2 b = ran f topGen b = topGen ran f
199 198 eqeq2d b = ran f J = topGen b J = topGen ran f
200 196 197 199 3anbi123d b = ran f b ω b B J = topGen b ran f ω ran f B J = topGen ran f
201 200 rspcev ran f TopBases ran f ω ran f B J = topGen ran f b TopBases b ω b B J = topGen b
202 183 194 65 195 201 syl13anc B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x b TopBases b ω b B J = topGen b
203 202 ex B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S B x S 1 st x f x f x 2 nd x b TopBases b ω b B J = topGen b
204 60 203 sylbid B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f : S I B x S 1 st x f x f x 2 nd x b TopBases b ω b B J = topGen b
205 204 exlimdv B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J f f : S I B x S 1 st x f x f x 2 nd x b TopBases b ω b B J = topGen b
206 57 205 mpd B TopBases J 2 nd 𝜔 c TopBases c ω topGen c = J b TopBases b ω b B J = topGen b
207 5 206 rexlimddv B TopBases J 2 nd 𝜔 b TopBases b ω b B J = topGen b