Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  bcth Structured version   Unicode version

Theorem bcth 19284
 Description: Baire's Category Theorem. If a nonempty metric space is complete, it is nonmeager in itself. In other words, no open set in the metric space can be the countable union of rare closed subsets (where rare means having an empty interior), so some subset must have a nonempty interior. Theorem 4.7-2 of [Kreyszig] p. 247. (The terminology "meager" and "nonmeager" is used by Kreyszig to replace Baire's "of the first category" and "of the second category." The latter terms are going out of favor to avoid confusion with category theory.) See bcthlem5 19283 for an overview of the proof. (Contributed by NM, 28-Oct-2007.) (Proof shortened by Mario Carneiro, 6-Jan-2014.)
Hypothesis
Ref Expression
bcth.2
Assertion
Ref Expression
bcth
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem bcth
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bcth.2 . . . . . 6
2 simpll 732 . . . . . 6
3 eleq1 2498 . . . . . . . . . . 11
4 eleq1 2498 . . . . . . . . . . 11
53, 4bi2anan9 845 . . . . . . . . . 10
6 simpr 449 . . . . . . . . . . . 12
76breq1d 4224 . . . . . . . . . . 11
8 oveq12 6092 . . . . . . . . . . . . 13
98fveq2d 5734 . . . . . . . . . . . 12
109sseq1d 3377 . . . . . . . . . . 11
117, 10anbi12d 693 . . . . . . . . . 10
125, 11anbi12d 693 . . . . . . . . 9
1312cbvopabv 4279 . . . . . . . 8
14 oveq2 6091 . . . . . . . . . . . 12
1514breq2d 4226 . . . . . . . . . . 11
16 fveq2 5730 . . . . . . . . . . . . 13
1716difeq2d 3467 . . . . . . . . . . . 12
1817sseq2d 3378 . . . . . . . . . . 11
1915, 18anbi12d 693 . . . . . . . . . 10
2019anbi2d 686 . . . . . . . . 9
2120opabbidv 4273 . . . . . . . 8
2213, 21syl5eq 2482 . . . . . . 7
23 fveq2 5730 . . . . . . . . . . . 12
2423difeq1d 3466 . . . . . . . . . . 11
2524sseq2d 3378 . . . . . . . . . 10
2625anbi2d 686 . . . . . . . . 9
2726anbi2d 686 . . . . . . . 8
2827opabbidv 4273 . . . . . . 7
2922, 28cbvmpt2v 6154 . . . . . 6
30 simplr 733 . . . . . 6
31 simpr 449 . . . . . . 7
3216fveq2d 5734 . . . . . . . . 9
3332eqeq1d 2446 . . . . . . . 8
3433cbvralv 2934 . . . . . . 7
3531, 34sylib 190 . . . . . 6
361, 2, 29, 30, 35bcthlem5 19283 . . . . 5
3736ex 425 . . . 4