Metamath Proof Explorer

Theorem bcth

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 a closure with empty interior), so some subset Mk 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 for an overview of the proof. (Contributed by NM, 28-Oct-2007) (Proof shortened by Mario Carneiro, 6-Jan-2014)

Ref Expression
Hypothesis bcth.2 
|- J = ( MetOpen ` D )
Assertion bcth 
|- ( ( D e. ( CMet ` X ) /\ M : NN --> ( Clsd ` J ) /\ ( ( int ` J ) ` U. ran M ) =/= (/) ) -> E. k e. NN ( ( int ` J ) ` ( M ` k ) ) =/= (/) )

Proof

Step Hyp Ref Expression
1 bcth.2 
 |-  J = ( MetOpen ` D )
2 simpll 
 |-  ( ( ( D e. ( CMet ` X ) /\ M : NN --> ( Clsd ` J ) ) /\ A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) ) -> D e. ( CMet ` X ) )
3 eleq1w 
 |-  ( x = y -> ( x e. X <-> y e. X ) )
4 eleq1w 
 |-  ( r = m -> ( r e. RR+ <-> m e. RR+ ) )
5 3 4 bi2anan9 
 |-  ( ( x = y /\ r = m ) -> ( ( x e. X /\ r e. RR+ ) <-> ( y e. X /\ m e. RR+ ) ) )
6 simpr 
 |-  ( ( x = y /\ r = m ) -> r = m )
7 6 breq1d 
 |-  ( ( x = y /\ r = m ) -> ( r < ( 1 / k ) <-> m < ( 1 / k ) ) )
8 oveq12 
 |-  ( ( x = y /\ r = m ) -> ( x ( ball ` D ) r ) = ( y ( ball ` D ) m ) )
9 8 fveq2d 
 |-  ( ( x = y /\ r = m ) -> ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) = ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) )
10 9 sseq1d 
 |-  ( ( x = y /\ r = m ) -> ( ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) <-> ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) )
11 7 10 anbi12d 
 |-  ( ( x = y /\ r = m ) -> ( ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) <-> ( m < ( 1 / k ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) )
12 5 11 anbi12d 
 |-  ( ( x = y /\ r = m ) -> ( ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) <-> ( ( y e. X /\ m e. RR+ ) /\ ( m < ( 1 / k ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) )
13 12 cbvopabv 
 |-  { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } = { <. y , m >. | ( ( y e. X /\ m e. RR+ ) /\ ( m < ( 1 / k ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) }
14 oveq2 
 |-  ( k = n -> ( 1 / k ) = ( 1 / n ) )
15 14 breq2d 
 |-  ( k = n -> ( m < ( 1 / k ) <-> m < ( 1 / n ) ) )
16 fveq2 
 |-  ( k = n -> ( M ` k ) = ( M ` n ) )
17 16 difeq2d 
 |-  ( k = n -> ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) = ( ( ( ball ` D ) ` z ) \ ( M ` n ) ) )
18 17 sseq2d 
 |-  ( k = n -> ( ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) <-> ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` n ) ) ) )
19 15 18 anbi12d 
 |-  ( k = n -> ( ( m < ( 1 / k ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) <-> ( m < ( 1 / n ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` n ) ) ) ) )
20 19 anbi2d 
 |-  ( k = n -> ( ( ( y e. X /\ m e. RR+ ) /\ ( m < ( 1 / k ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) <-> ( ( y e. X /\ m e. RR+ ) /\ ( m < ( 1 / n ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` n ) ) ) ) ) )
21 20 opabbidv 
 |-  ( k = n -> { <. y , m >. | ( ( y e. X /\ m e. RR+ ) /\ ( m < ( 1 / k ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } = { <. y , m >. | ( ( y e. X /\ m e. RR+ ) /\ ( m < ( 1 / n ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` n ) ) ) ) } )
22 13 21 eqtrid 
 |-  ( k = n -> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } = { <. y , m >. | ( ( y e. X /\ m e. RR+ ) /\ ( m < ( 1 / n ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` n ) ) ) ) } )
23 fveq2 
 |-  ( z = g -> ( ( ball ` D ) ` z ) = ( ( ball ` D ) ` g ) )
24 23 difeq1d 
 |-  ( z = g -> ( ( ( ball ` D ) ` z ) \ ( M ` n ) ) = ( ( ( ball ` D ) ` g ) \ ( M ` n ) ) )
25 24 sseq2d 
 |-  ( z = g -> ( ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` n ) ) <-> ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` g ) \ ( M ` n ) ) ) )
26 25 anbi2d 
 |-  ( z = g -> ( ( m < ( 1 / n ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` n ) ) ) <-> ( m < ( 1 / n ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` g ) \ ( M ` n ) ) ) ) )
27 26 anbi2d 
 |-  ( z = g -> ( ( ( y e. X /\ m e. RR+ ) /\ ( m < ( 1 / n ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` n ) ) ) ) <-> ( ( y e. X /\ m e. RR+ ) /\ ( m < ( 1 / n ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` g ) \ ( M ` n ) ) ) ) ) )
28 27 opabbidv 
 |-  ( z = g -> { <. y , m >. | ( ( y e. X /\ m e. RR+ ) /\ ( m < ( 1 / n ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` n ) ) ) ) } = { <. y , m >. | ( ( y e. X /\ m e. RR+ ) /\ ( m < ( 1 / n ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` g ) \ ( M ` n ) ) ) ) } )
29 22 28 cbvmpov 
 |-  ( k e. NN , z e. ( X X. RR+ ) |-> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } ) = ( n e. NN , g e. ( X X. RR+ ) |-> { <. y , m >. | ( ( y e. X /\ m e. RR+ ) /\ ( m < ( 1 / n ) /\ ( ( cls ` J ) ` ( y ( ball ` D ) m ) ) C_ ( ( ( ball ` D ) ` g ) \ ( M ` n ) ) ) ) } )
30 simplr 
 |-  ( ( ( D e. ( CMet ` X ) /\ M : NN --> ( Clsd ` J ) ) /\ A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) ) -> M : NN --> ( Clsd ` J ) )
31 simpr 
 |-  ( ( ( D e. ( CMet ` X ) /\ M : NN --> ( Clsd ` J ) ) /\ A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) ) -> A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) )
32 16 fveqeq2d 
 |-  ( k = n -> ( ( ( int ` J ) ` ( M ` k ) ) = (/) <-> ( ( int ` J ) ` ( M ` n ) ) = (/) ) )
33 32 cbvralvw 
 |-  ( A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) <-> A. n e. NN ( ( int ` J ) ` ( M ` n ) ) = (/) )
34 31 33 sylib 
 |-  ( ( ( D e. ( CMet ` X ) /\ M : NN --> ( Clsd ` J ) ) /\ A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) ) -> A. n e. NN ( ( int ` J ) ` ( M ` n ) ) = (/) )
35 1 2 29 30 34 bcthlem5 
 |-  ( ( ( D e. ( CMet ` X ) /\ M : NN --> ( Clsd ` J ) ) /\ A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) ) -> ( ( int ` J ) ` U. ran M ) = (/) )
36 35 ex 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> ( Clsd ` J ) ) -> ( A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) -> ( ( int ` J ) ` U. ran M ) = (/) ) )
37 36 necon3ad 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> ( Clsd ` J ) ) -> ( ( ( int ` J ) ` U. ran M ) =/= (/) -> -. A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) ) )
38 37 3impia 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> ( Clsd ` J ) /\ ( ( int ` J ) ` U. ran M ) =/= (/) ) -> -. A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) )
39 df-ne 
 |-  ( ( ( int ` J ) ` ( M ` k ) ) =/= (/) <-> -. ( ( int ` J ) ` ( M ` k ) ) = (/) )
40 39 rexbii 
 |-  ( E. k e. NN ( ( int ` J ) ` ( M ` k ) ) =/= (/) <-> E. k e. NN -. ( ( int ` J ) ` ( M ` k ) ) = (/) )
41 rexnal 
 |-  ( E. k e. NN -. ( ( int ` J ) ` ( M ` k ) ) = (/) <-> -. A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) )
42 40 41 bitri 
 |-  ( E. k e. NN ( ( int ` J ) ` ( M ` k ) ) =/= (/) <-> -. A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) )
43 38 42 sylibr 
 |-  ( ( D e. ( CMet ` X ) /\ M : NN --> ( Clsd ` J ) /\ ( ( int ` J ) ` U. ran M ) =/= (/) ) -> E. k e. NN ( ( int ` J ) ` ( M ` k ) ) =/= (/) )