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 )