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

Theorem bcth 19165
 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 19164 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 731 . . . . . 6
3 eleq1 2461 . . . . . . . . . . 11
4 eleq1 2461 . . . . . . . . . . 11
53, 4bi2anan9 844 . . . . . . . . . 10
6 simpr 448 . . . . . . . . . . . 12
76breq1d 4177 . . . . . . . . . . 11
8 oveq12 6043 . . . . . . . . . . . . 13
98fveq2d 5686 . . . . . . . . . . . 12
109sseq1d 3332 . . . . . . . . . . 11
117, 10anbi12d 692 . . . . . . . . . 10
125, 11anbi12d 692 . . . . . . . . 9
1312cbvopabv 4232 . . . . . . . 8
14 oveq2 6042 . . . . . . . . . . . 12
1514breq2d 4179 . . . . . . . . . . 11
16 fveq2 5682 . . . . . . . . . . . . 13
1716difeq2d 3422 . . . . . . . . . . . 12
1817sseq2d 3333 . . . . . . . . . . 11
1915, 18anbi12d 692 . . . . . . . . . 10
2019anbi2d 685 . . . . . . . . 9
2120opabbidv 4226 . . . . . . . 8
2213, 21syl5eq 2445 . . . . . . 7
23 fveq2 5682 . . . . . . . . . . . 12
2423difeq1d 3421 . . . . . . . . . . 11
2524sseq2d 3333 . . . . . . . . . 10
2625anbi2d 685 . . . . . . . . 9
2726anbi2d 685 . . . . . . . 8
2827opabbidv 4226 . . . . . . 7
2922, 28cbvmpt2v 6105 . . . . . 6
30 simplr 732 . . . . . 6
31 simpr 448 . . . . . . 7
3216fveq2d 5686 . . . . . . . . 9
3332eqeq1d 2409 . . . . . . . 8
3433cbvralv 2889 . . . . . . 7
3531, 34sylib 189 . . . . . 6
361, 2, 29, 30, 35bcthlem5 19164 . . . . 5
3736ex 424 . . . 4