Metamath Proof Explorer

Theorem lebnum

Description: The Lebesgue number lemma, or Lebesgue covering lemma. If X is a compact metric space and U is an open cover of X , then there exists a positive real number d such that every ball of size d (and every subset of a ball of size d , including every subset of diameter less than d ) is a subset of some member of the cover. (Contributed by Mario Carneiro, 14-Feb-2015) (Proof shortened by Mario Carneiro, 5-Sep-2015) (Proof shortened by AV, 30-Sep-2020)

Ref Expression
Hypotheses lebnum.j 
|- J = ( MetOpen ` D )
lebnum.d 
|- ( ph -> D e. ( Met ` X ) )
lebnum.c 
|- ( ph -> J e. Comp )
lebnum.s 
|- ( ph -> U C_ J )
lebnum.u 
|- ( ph -> X = U. U )
Assertion lebnum 
|- ( ph -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )

Proof

Step Hyp Ref Expression
1 lebnum.j 
 |-  J = ( MetOpen ` D )
2 lebnum.d 
 |-  ( ph -> D e. ( Met ` X ) )
3 lebnum.c 
 |-  ( ph -> J e. Comp )
4 lebnum.s 
 |-  ( ph -> U C_ J )
5 lebnum.u 
 |-  ( ph -> X = U. U )
6 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
7 2 6 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
8 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
9 7 8 syl 
 |-  ( ph -> X = U. J )
10 9 5 eqtr3d 
 |-  ( ph -> U. J = U. U )
11 eqid 
 |-  U. J = U. J
12 11 cmpcov 
 |-  ( ( J e. Comp /\ U C_ J /\ U. J = U. U ) -> E. w e. ( ~P U i^i Fin ) U. J = U. w )
13 3 4 10 12 syl3anc 
 |-  ( ph -> E. w e. ( ~P U i^i Fin ) U. J = U. w )
14 1rp 
 |-  1 e. RR+
15 simprl 
 |-  ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) -> w e. ( ~P U i^i Fin ) )
16 15 elin1d 
 |-  ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) -> w e. ~P U )
17 16 elpwid 
 |-  ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) -> w C_ U )
18 17 ad2antrr 
 |-  ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> w C_ U )
19 simplr 
 |-  ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> X e. w )
20 18 19 sseldd 
 |-  ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> X e. U )
21 7 ad3antrrr 
 |-  ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> D e. ( *Met ` X ) )
22 simpr 
 |-  ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> x e. X )
23 rpxr 
 |-  ( 1 e. RR+ -> 1 e. RR* )
24 14 23 mp1i 
 |-  ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> 1 e. RR* )
25 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ 1 e. RR* ) -> ( x ( ball ` D ) 1 ) C_ X )
26 21 22 24 25 syl3anc 
 |-  ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> ( x ( ball ` D ) 1 ) C_ X )
27 sseq2 
 |-  ( u = X -> ( ( x ( ball ` D ) 1 ) C_ u <-> ( x ( ball ` D ) 1 ) C_ X ) )
28 27 rspcev 
 |-  ( ( X e. U /\ ( x ( ball ` D ) 1 ) C_ X ) -> E. u e. U ( x ( ball ` D ) 1 ) C_ u )
29 20 26 28 syl2anc 
 |-  ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> E. u e. U ( x ( ball ` D ) 1 ) C_ u )
30 29 ralrimiva 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) -> A. x e. X E. u e. U ( x ( ball ` D ) 1 ) C_ u )
31 oveq2 
 |-  ( d = 1 -> ( x ( ball ` D ) d ) = ( x ( ball ` D ) 1 ) )
32 31 sseq1d 
 |-  ( d = 1 -> ( ( x ( ball ` D ) d ) C_ u <-> ( x ( ball ` D ) 1 ) C_ u ) )
33 32 rexbidv 
 |-  ( d = 1 -> ( E. u e. U ( x ( ball ` D ) d ) C_ u <-> E. u e. U ( x ( ball ` D ) 1 ) C_ u ) )
34 33 ralbidv 
 |-  ( d = 1 -> ( A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u <-> A. x e. X E. u e. U ( x ( ball ` D ) 1 ) C_ u ) )
35 34 rspcev 
 |-  ( ( 1 e. RR+ /\ A. x e. X E. u e. U ( x ( ball ` D ) 1 ) C_ u ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )
36 14 30 35 sylancr 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )
37 2 ad2antrr 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> D e. ( Met ` X ) )
38 3 ad2antrr 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> J e. Comp )
39 17 adantr 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> w C_ U )
40 4 ad2antrr 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> U C_ J )
41 39 40 sstrd 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> w C_ J )
42 9 ad2antrr 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> X = U. J )
43 simplrr 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> U. J = U. w )
44 42 43 eqtrd 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> X = U. w )
45 15 elin2d 
 |-  ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) -> w e. Fin )
46 45 adantr 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> w e. Fin )
47 simpr 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> -. X e. w )
48 eqid 
 |-  ( y e. X |-> sum_ k e. w inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) = ( y e. X |-> sum_ k e. w inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) )
49 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
50 1 37 38 41 44 46 47 48 49 lebnumlem3 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> E. d e. RR+ A. x e. X E. u e. w ( x ( ball ` D ) d ) C_ u )
51 ssrexv 
 |-  ( w C_ U -> ( E. u e. w ( x ( ball ` D ) d ) C_ u -> E. u e. U ( x ( ball ` D ) d ) C_ u ) )
52 39 51 syl 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> ( E. u e. w ( x ( ball ` D ) d ) C_ u -> E. u e. U ( x ( ball ` D ) d ) C_ u ) )
53 52 ralimdv 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> ( A. x e. X E. u e. w ( x ( ball ` D ) d ) C_ u -> A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) )
54 53 reximdv 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> ( E. d e. RR+ A. x e. X E. u e. w ( x ( ball ` D ) d ) C_ u -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) )
55 50 54 mpd 
 |-  ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )
56 36 55 pm2.61dan 
 |-  ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )
57 13 56 rexlimddv 
 |-  ( ph -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )