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

Theorem bcth 18583
 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 18582 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
StepHypRef Expression
1 bcth.2 . . . . . 6
2 simpll 733 . . . . . 6
3 eleq1 2313 . . . . . . . . . . 11
4 eleq1 2313 . . . . . . . . . . 11
53, 4bi2anan9 848 . . . . . . . . . 10
6 simpr 449 . . . . . . . . . . . 12
76breq1d 3930 . . . . . . . . . . 11
8 oveq12 5719 . . . . . . . . . . . . 13
98fveq2d 5381 . . . . . . . . . . . 12
109sseq1d 3126 . . . . . . . . . . 11
117, 10anbi12d 694 . . . . . . . . . 10
125, 11anbi12d 694 . . . . . . . . 9
1312cbvopabv 3985 . . . . . . . 8
14 oveq2 5718 . . . . . . . . . . . 12
1514breq2d 3932 . . . . . . . . . . 11
16 fveq2 5377 . . . . . . . . . . . . 13
1716difeq2d 3211 . . . . . . . . . . . 12
1817sseq2d 3127 . . . . . . . . . . 11
1915, 18anbi12d 694 . . . . . . . . . 10
2019anbi2d 687 . . . . . . . . 9
2120opabbidv 3979 . . . . . . . 8
2213, 21syl5eq 2297 . . . . . . 7
23 fveq2 5377 . . . . . . . . . . . 12
2423difeq1d 3210 . . . . . . . . . . 11
2524sseq2d 3127 . . . . . . . . . 10
2625anbi2d 687 . . . . . . . . 9
2726anbi2d 687 . . . . . . . 8
2827opabbidv 3979 . . . . . . 7
2922, 28cbvmpt2v 5778 . . . . . 6
30 simplr 734 . . . . . 6
31 simpr 449 . . . . . . 7
3216fveq2d 5381 . . . . . . . . 9
3332eqeq1d 2261 . . . . . . . 8
3433cbvralv 2708 . . . . . . 7
3531, 34sylib 190 . . . . . 6
361, 2, 29, 30, 35bcthlem5 18582 . . . . 5
3736ex 425 . . . 4