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

Theorem bcth 18745
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  M `
 k 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 18744 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  |-  J  =  ( MetOpen `  D )
Assertion
Ref Expression
bcth  |-  ( ( D  e.  ( CMet `  X )  /\  M : NN --> ( Clsd `  J
)  /\  ( ( int `  J ) `  U. ran  M )  =/=  (/) )  ->  E. k  e.  NN  ( ( int `  J ) `  ( M `  k )
)  =/=  (/) )
Distinct variable groups:    D, k    k, J    k, M    k, X
Dummy variables  n  r  x  z  g  m  y are mutually distinct and distinct from all other variables.

Proof of Theorem bcth
StepHypRef Expression
1 bcth.2 . . . . . 6  |-  J  =  ( MetOpen `  D )
2 simpll 732 . . . . . 6  |-  ( ( ( D  e.  (
CMet `  X )  /\  M : NN --> ( Clsd `  J ) )  /\  A. k  e.  NN  (
( int `  J
) `  ( M `  k ) )  =  (/) )  ->  D  e.  ( CMet `  X
) )
3 eleq1 2344 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
x  e.  X  <->  y  e.  X ) )
4 eleq1 2344 . . . . . . . . . . 11  |-  ( r  =  m  ->  (
r  e.  RR+  <->  m  e.  RR+ ) )
53, 4bi2anan9 845 . . . . . . . . . 10  |-  ( ( x  =  y  /\  r  =  m )  ->  ( ( x  e.  X  /\  r  e.  RR+ )  <->  ( y  e.  X  /\  m  e.  RR+ ) ) )
6 simpr 449 . . . . . . . . . . . 12  |-  ( ( x  =  y  /\  r  =  m )  ->  r  =  m )
76breq1d 4034 . . . . . . . . . . 11  |-  ( ( x  =  y  /\  r  =  m )  ->  ( r  <  (
1  /  k )  <-> 
m  <  ( 1  /  k ) ) )
8 oveq12 5828 . . . . . . . . . . . . 13  |-  ( ( x  =  y  /\  r  =  m )  ->  ( x ( ball `  D ) r )  =  ( y (
ball `  D )
m ) )
98fveq2d 5489 . . . . . . . . . . . 12  |-  ( ( x  =  y  /\  r  =  m )  ->  ( ( cls `  J
) `  ( x
( ball `  D )
r ) )  =  ( ( cls `  J
) `  ( y
( ball `  D )
m ) ) )
109sseq1d 3206 . . . . . . . . . . 11  |-  ( ( 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 )
) ) )
117, 10anbi12d 693 . . . . . . . . . 10  |-  ( ( 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 )
) ) ) )
125, 11anbi12d 693 . . . . . . . . 9  |-  ( ( 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 ) ) ) ) ) )
1312cbvopabv 4089 . . . . . . . 8  |-  { <. 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 5827 . . . . . . . . . . . 12  |-  ( k  =  n  ->  (
1  /  k )  =  ( 1  /  n ) )
1514breq2d 4036 . . . . . . . . . . 11  |-  ( k  =  n  ->  (
m  <  ( 1  /  k )  <->  m  <  ( 1  /  n ) ) )
16 fveq2 5485 . . . . . . . . . . . . 13  |-  ( k  =  n  ->  ( M `  k )  =  ( M `  n ) )
1716difeq2d 3295 . . . . . . . . . . . 12  |-  ( k  =  n  ->  (
( ( ball `  D
) `  z )  \  ( M `  k ) )  =  ( ( ( ball `  D ) `  z
)  \  ( M `  n ) ) )
1817sseq2d 3207 . . . . . . . . . . 11  |-  ( 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 )
) ) )
1915, 18anbi12d 693 . . . . . . . . . 10  |-  ( 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 )
) ) ) )
2019anbi2d 686 . . . . . . . . 9  |-  ( 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 ) ) ) ) ) )
2120opabbidv 4083 . . . . . . . 8  |-  ( 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 )
) ) ) } )
2213, 21syl5eq 2328 . . . . . . 7  |-  ( 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 5485 . . . . . . . . . . . 12  |-  ( z  =  g  ->  (
( ball `  D ) `  z )  =  ( ( ball `  D
) `  g )
)
2423difeq1d 3294 . . . . . . . . . . 11  |-  ( z  =  g  ->  (
( ( ball `  D
) `  z )  \  ( M `  n ) )  =  ( ( ( ball `  D ) `  g
)  \  ( M `  n ) ) )
2524sseq2d 3207 . . . . . . . . . 10  |-  ( 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 )
) ) )
2625anbi2d 686 . . . . . . . . 9  |-  ( 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 )
) ) ) )
2726anbi2d 686 . . . . . . . 8  |-  ( 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 ) ) ) ) ) )
2827opabbidv 4083 . . . . . . 7  |-  ( 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 )
) ) ) } )
2922, 28cbvmpt2v 5887 . . . . . 6  |-  ( 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 733 . . . . . 6  |-  ( ( ( D  e.  (
CMet `  X )  /\  M : NN --> ( Clsd `  J ) )  /\  A. k  e.  NN  (
( int `  J
) `  ( M `  k ) )  =  (/) )  ->  M : NN
--> ( Clsd `  J
) )
31 simpr 449 . . . . . . 7  |-  ( ( ( D  e.  (
CMet `  X )  /\  M : NN --> ( Clsd `  J ) )  /\  A. k  e.  NN  (
( int `  J
) `  ( M `  k ) )  =  (/) )  ->  A. k  e.  NN  ( ( int `  J ) `  ( M `  k )
)  =  (/) )
3216fveq2d 5489 . . . . . . . . 9  |-  ( k  =  n  ->  (
( int `  J
) `  ( M `  k ) )  =  ( ( int `  J
) `  ( M `  n ) ) )
3332eqeq1d 2292 . . . . . . . 8  |-  ( k  =  n  ->  (
( ( int `  J
) `  ( M `  k ) )  =  (/) 
<->  ( ( int `  J
) `  ( M `  n ) )  =  (/) ) )
3433cbvralv 2765 . . . . . . 7  |-  ( A. k  e.  NN  (
( int `  J
) `  ( M `  k ) )  =  (/) 
<-> 
A. n  e.  NN  ( ( int `  J
) `  ( M `  n ) )  =  (/) )
3531, 34sylib 190 . . . . . 6  |-  ( ( ( D  e.  (
CMet `  X )  /\  M : NN --> ( Clsd `  J ) )  /\  A. k  e.  NN  (
( int `  J
) `  ( M `  k ) )  =  (/) )  ->  A. n  e.  NN  ( ( int `  J ) `  ( M `  n )
)  =  (/) )
361, 2, 29, 30, 35bcthlem5 18744 . . . . 5  |-  ( ( ( D  e.  (
CMet `  X )  /\  M : NN --> ( Clsd `  J ) )  /\  A. k  e.  NN  (
( int `  J
) `  ( M `  k ) )  =  (/) )  ->  ( ( int `  J ) `
 U. ran  M
)  =  (/) )
3736ex 425 . . . 4  |-  ( ( D  e.  ( CMet `  X )  /\  M : NN --> ( Clsd `  J
) )  ->  ( A. k  e.  NN  ( ( int `  J
) `  ( M `  k ) )  =  (/)  ->  ( ( int `  J ) `  U. ran  M )  =  (/) ) )
3837necon3ad 2483 . . 3  |-  ( ( D  e.  ( CMet `  X )  /\  M : NN --> ( Clsd `  J
) )  ->  (
( ( int `  J
) `  U. ran  M
)  =/=  (/)  ->  -.  A. k  e.  NN  (
( int `  J
) `  ( M `  k ) )  =  (/) ) )
39383impia 1150 . 2  |-  ( ( D  e.  ( CMet `  X )  /\  M : NN --> ( Clsd `  J
)  /\  ( ( int `  J ) `  U. ran  M )  =/=  (/) )  ->  -.  A. k  e.  NN  (
( int `  J
) `  ( M `  k ) )  =  (/) )
40 df-ne 2449 . . . 4  |-  ( ( ( int `  J
) `  ( M `  k ) )  =/=  (/) 
<->  -.  ( ( int `  J ) `  ( M `  k )
)  =  (/) )
4140rexbii 2569 . . 3  |-  ( E. k  e.  NN  (
( int `  J
) `  ( M `  k ) )  =/=  (/) 
<->  E. k  e.  NN  -.  ( ( int `  J
) `  ( M `  k ) )  =  (/) )
42 rexnal 2555 . . 3  |-  ( E. k  e.  NN  -.  ( ( int `  J
) `  ( M `  k ) )  =  (/) 
<->  -.  A. k  e.  NN  ( ( int `  J ) `  ( M `  k )
)  =  (/) )
4341, 42bitri 242 . 2  |-  ( E. k  e.  NN  (
( int `  J
) `  ( M `  k ) )  =/=  (/) 
<->  -.  A. k  e.  NN  ( ( int `  J ) `  ( M `  k )
)  =  (/) )
4439, 43sylibr 205 1  |-  ( ( D  e.  ( CMet `  X )  /\  M : NN --> ( Clsd `  J
)  /\  ( ( int `  J ) `  U. ran  M )  =/=  (/) )  ->  E. k  e.  NN  ( ( int `  J ) `  ( M `  k )
)  =/=  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    /\ wa 360    /\ w3a 936    = wceq 1624    e. wcel 1685    =/= wne 2447   A.wral 2544   E.wrex 2545    \ cdif 3150    C_ wss 3153   (/)c0 3456   U.cuni 3828   class class class wbr 4024   {copab 4077    X. cxp 4686   ran crn 4689   -->wf 5217   ` cfv 5221  (class class class)co 5819    e. cmpt2 5821   1c1 8733    < clt 8862    / cdiv 9418   NNcn 9741   RR+crp 10349   ballcbl 16365   MetOpencmopn 16366   Clsdccld 16747   intcnt 16748   clsccl 16749   CMetcms 18674
This theorem is referenced by:  bcth2  18746  bcth3  18747
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-rep 4132  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511  ax-inf2 7337  ax-dc 8067  ax-cnex 8788  ax-resscn 8789  ax-1cn 8790  ax-icn 8791  ax-addcl 8792  ax-addrcl 8793  ax-mulcl 8794  ax-mulrcl 8795  ax-mulcom 8796  ax-addass 8797  ax-mulass 8798  ax-distr 8799  ax-i2m1 8800  ax-1ne0 8801  ax-1rid 8802  ax-rnegex 8803  ax-rrecex 8804  ax-cnre 8805  ax-pre-lttri 8806  ax-pre-lttrn 8807  ax-pre-ltadd 8808  ax-pre-mulgt0 8809  ax-pre-sup 8810
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-nel 2450  df-ral 2549  df-rex 2550  df-reu 2551  df-rmo 2552  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pss 3169  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-tp 3649  df-op 3650  df-uni 3829  df-int 3864  df-iun 3908  df-iin 3909  df-br 4025  df-opab 4079  df-mpt 4080  df-tr 4115  df-eprel 4304  df-id 4308  df-po 4313  df-so 4314  df-fr 4351  df-we 4353  df-ord 4394  df-on 4395  df-lim 4396  df-suc 4397  df-om 4656  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-fv 5229  df-ov 5822  df-oprab 5823  df-mpt2 5824  df-1st 6083  df-2nd 6084  df-iota 6252  df-riota 6299  df-recs 6383  df-rdg 6418  df-1o 6474  df-er 6655  df-map 6769  df-pm 6770  df-en 6859  df-dom 6860  df-sdom 6861  df-sup 7189  df-pnf 8864  df-mnf 8865  df-xr 8866  df-ltxr 8867  df-le 8868  df-sub 9034  df-neg 9035  df-div 9419  df-nn 9742  df-2 9799  df-n0 9961  df-z 10020  df-uz 10226  df-q 10312  df-rp 10350  df-xneg 10447  df-xadd 10448  df-xmul 10449  df-ico 10656  df-rest 13321  df-topgen 13338  df-xmet 16367  df-met 16368  df-bl 16369  df-mopn 16370  df-top 16630  df-bases 16632  df-topon 16633  df-cld 16750  df-ntr 16751  df-cls 16752  df-nei 16829  df-lm 16953  df-fbas 17514  df-fg 17515  df-fil 17535  df-fm 17627  df-flim 17628  df-flf 17629  df-cfil 18675  df-cau 18676  df-cmet 18677
  Copyright terms: Public domain W3C validator