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

Theorem lebnumlem1 22037
Description: Lemma for lebnum 22043. The function  F measures the sum of all of the distances to escape the sets of the cover. Since by assumption it is a cover, there is at least one set which covers a given point, and since it is open, the point is a positive distance from the edge of the set. Thus, the sum is a strictly positive number. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by AV, 30-Sep-2020.)
Hypotheses
Ref Expression
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
)
lebnumlem1.u  |-  ( ph  ->  U  e.  Fin )
lebnumlem1.n  |-  ( ph  ->  -.  X  e.  U
)
lebnumlem1.f  |-  F  =  ( y  e.  X  |-> 
sum_ k  e.  U inf ( ran  ( z  e.  ( X  \  k
)  |->  ( y D z ) ) , 
RR* ,  <  ) )
Assertion
Ref Expression
lebnumlem1  |-  ( ph  ->  F : X --> RR+ )
Distinct variable groups:    y, k,
z, D    k, J, y, z    U, k, y, z    ph, k, y, z   
k, X, y, z
Allowed substitution hints:    F( y, z, k)

Proof of Theorem lebnumlem1
Dummy variables  m  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lebnumlem1.u . . . . 5  |-  ( ph  ->  U  e.  Fin )
21adantr 471 . . . 4  |-  ( (
ph  /\  y  e.  X )  ->  U  e.  Fin )
3 lebnum.d . . . . . . . 8  |-  ( ph  ->  D  e.  ( Met `  X ) )
43ad2antrr 737 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  D  e.  ( Met `  X
) )
5 difssd 3572 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  ( X  \  k )  C_  X )
6 lebnum.s . . . . . . . . . . . 12  |-  ( ph  ->  U  C_  J )
76adantr 471 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  X )  ->  U  C_  J )
87sselda 3443 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  k  e.  J )
9 elssuni 4240 . . . . . . . . . 10  |-  ( k  e.  J  ->  k  C_ 
U. J )
108, 9syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  k  C_ 
U. J )
11 metxmet 21397 . . . . . . . . . . . 12  |-  ( D  e.  ( Met `  X
)  ->  D  e.  ( *Met `  X
) )
123, 11syl 17 . . . . . . . . . . 11  |-  ( ph  ->  D  e.  ( *Met `  X ) )
13 lebnum.j . . . . . . . . . . . 12  |-  J  =  ( MetOpen `  D )
1413mopnuni 21504 . . . . . . . . . . 11  |-  ( D  e.  ( *Met `  X )  ->  X  =  U. J )
1512, 14syl 17 . . . . . . . . . 10  |-  ( ph  ->  X  =  U. J
)
1615ad2antrr 737 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  X  =  U. J )
1710, 16sseqtr4d 3480 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  k  C_  X )
18 lebnumlem1.n . . . . . . . . . . . 12  |-  ( ph  ->  -.  X  e.  U
)
19 eleq1 2527 . . . . . . . . . . . . 13  |-  ( k  =  X  ->  (
k  e.  U  <->  X  e.  U ) )
2019notbid 300 . . . . . . . . . . . 12  |-  ( k  =  X  ->  ( -.  k  e.  U  <->  -.  X  e.  U ) )
2118, 20syl5ibrcom 230 . . . . . . . . . . 11  |-  ( ph  ->  ( k  =  X  ->  -.  k  e.  U ) )
2221necon2ad 2650 . . . . . . . . . 10  |-  ( ph  ->  ( k  e.  U  ->  k  =/=  X ) )
2322adantr 471 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  X )  ->  (
k  e.  U  -> 
k  =/=  X ) )
2423imp 435 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  k  =/=  X )
25 pssdifn0 3838 . . . . . . . 8  |-  ( ( k  C_  X  /\  k  =/=  X )  -> 
( X  \  k
)  =/=  (/) )
2617, 24, 25syl2anc 671 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  ( X  \  k )  =/=  (/) )
27 eqid 2461 . . . . . . . 8  |-  ( y  e.  X  |-> inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  ) )  =  ( y  e.  X  |-> inf ( ran  ( z  e.  ( X  \ 
k )  |->  ( y D z ) ) ,  RR* ,  <  )
)
2827metdsre 21918 . . . . . . 7  |-  ( ( D  e.  ( Met `  X )  /\  ( X  \  k )  C_  X  /\  ( X  \ 
k )  =/=  (/) )  -> 
( y  e.  X  |-> inf ( ran  ( z  e.  ( X  \ 
k )  |->  ( y D z ) ) ,  RR* ,  <  )
) : X --> RR )
294, 5, 26, 28syl3anc 1276 . . . . . 6  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  (
y  e.  X  |-> inf ( ran  ( z  e.  ( X  \  k
)  |->  ( y D z ) ) , 
RR* ,  <  ) ) : X --> RR )
3027fmpt 6065 . . . . . 6  |-  ( A. y  e.  X inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  )  e.  RR  <->  ( y  e.  X  |-> inf ( ran  ( z  e.  ( X  \  k
)  |->  ( y D z ) ) , 
RR* ,  <  ) ) : X --> RR )
3129, 30sylibr 217 . . . . 5  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  A. y  e.  X inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  )  e.  RR )
32 simplr 767 . . . . 5  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  y  e.  X )
33 rsp 2765 . . . . 5  |-  ( A. y  e.  X inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  )  e.  RR  ->  ( y  e.  X  -> inf ( ran  ( z  e.  ( X  \ 
k )  |->  ( y D z ) ) ,  RR* ,  <  )  e.  RR ) )
3431, 32, 33sylc 62 . . . 4  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  -> inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  )  e.  RR )
352, 34fsumrecl 13848 . . 3  |-  ( (
ph  /\  y  e.  X )  ->  sum_ k  e.  U inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  )  e.  RR )
36 lebnum.u . . . . . . 7  |-  ( ph  ->  X  =  U. U
)
3736eleq2d 2524 . . . . . 6  |-  ( ph  ->  ( y  e.  X  <->  y  e.  U. U ) )
3837biimpa 491 . . . . 5  |-  ( (
ph  /\  y  e.  X )  ->  y  e.  U. U )
39 eluni2 4215 . . . . 5  |-  ( y  e.  U. U  <->  E. m  e.  U  y  e.  m )
4038, 39sylib 201 . . . 4  |-  ( (
ph  /\  y  e.  X )  ->  E. m  e.  U  y  e.  m )
41 0red 9669 . . . . 5  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  0  e.  RR )
42 simplr 767 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  y  e.  X )
43 eqid 2461 . . . . . . . 8  |-  ( w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m ) 
|->  ( w D z ) ) ,  RR* ,  <  ) )  =  ( w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m )  |->  ( w D z ) ) ,  RR* ,  <  )
)
4443metdsval 21912 . . . . . . 7  |-  ( y  e.  X  ->  (
( w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m )  |->  ( w D z ) ) ,  RR* ,  <  )
) `  y )  = inf ( ran  ( z  e.  ( X  \  m )  |->  ( y D z ) ) ,  RR* ,  <  )
)
4542, 44syl 17 . . . . . 6  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( (
w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m
)  |->  ( w D z ) ) , 
RR* ,  <  ) ) `
 y )  = inf ( ran  ( z  e.  ( X  \  m )  |->  ( y D z ) ) ,  RR* ,  <  )
)
463ad2antrr 737 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  D  e.  ( Met `  X ) )
47 difssd 3572 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( X  \  m )  C_  X
)
486ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  U  C_  J
)
49 simprl 769 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  m  e.  U )
5048, 49sseldd 3444 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  m  e.  J )
51 elssuni 4240 . . . . . . . . . . 11  |-  ( m  e.  J  ->  m  C_ 
U. J )
5250, 51syl 17 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  m  C_  U. J
)
5346, 11, 143syl 18 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  X  =  U. J )
5452, 53sseqtr4d 3480 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  m  C_  X
)
55 eleq1 2527 . . . . . . . . . . . . . 14  |-  ( m  =  X  ->  (
m  e.  U  <->  X  e.  U ) )
5655notbid 300 . . . . . . . . . . . . 13  |-  ( m  =  X  ->  ( -.  m  e.  U  <->  -.  X  e.  U ) )
5718, 56syl5ibrcom 230 . . . . . . . . . . . 12  |-  ( ph  ->  ( m  =  X  ->  -.  m  e.  U ) )
5857necon2ad 2650 . . . . . . . . . . 11  |-  ( ph  ->  ( m  e.  U  ->  m  =/=  X ) )
5958ad2antrr 737 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( m  e.  U  ->  m  =/= 
X ) )
6049, 59mpd 15 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  m  =/=  X )
61 pssdifn0 3838 . . . . . . . . 9  |-  ( ( m  C_  X  /\  m  =/=  X )  -> 
( X  \  m
)  =/=  (/) )
6254, 60, 61syl2anc 671 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( X  \  m )  =/=  (/) )
6343metdsre 21918 . . . . . . . 8  |-  ( ( D  e.  ( Met `  X )  /\  ( X  \  m )  C_  X  /\  ( X  \  m )  =/=  (/) )  -> 
( w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m )  |->  ( w D z ) ) ,  RR* ,  <  )
) : X --> RR )
6446, 47, 62, 63syl3anc 1276 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m ) 
|->  ( w D z ) ) ,  RR* ,  <  ) ) : X --> RR )
6564, 42ffvelrnd 6045 . . . . . 6  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( (
w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m
)  |->  ( w D z ) ) , 
RR* ,  <  ) ) `
 y )  e.  RR )
6645, 65eqeltrrd 2540 . . . . 5  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  -> inf ( ran  ( z  e.  ( X  \  m ) 
|->  ( y D z ) ) ,  RR* ,  <  )  e.  RR )
6735adantr 471 . . . . 5  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  sum_ k  e.  U inf ( ran  (
z  e.  ( X 
\  k )  |->  ( y D z ) ) ,  RR* ,  <  )  e.  RR )
6812ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  D  e.  ( *Met `  X
) )
6943metdsf 21913 . . . . . . . . . . 11  |-  ( ( D  e.  ( *Met `  X )  /\  ( X  \  m )  C_  X
)  ->  ( w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m ) 
|->  ( w D z ) ) ,  RR* ,  <  ) ) : X --> ( 0 [,] +oo ) )
7068, 47, 69syl2anc 671 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m ) 
|->  ( w D z ) ) ,  RR* ,  <  ) ) : X --> ( 0 [,] +oo ) )
7170, 42ffvelrnd 6045 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( (
w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m
)  |->  ( w D z ) ) , 
RR* ,  <  ) ) `
 y )  e.  ( 0 [,] +oo ) )
72 elxrge0 11769 . . . . . . . . 9  |-  ( ( ( w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m )  |->  ( w D z ) ) ,  RR* ,  <  )
) `  y )  e.  ( 0 [,] +oo ) 
<->  ( ( ( w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m ) 
|->  ( w D z ) ) ,  RR* ,  <  ) ) `  y )  e.  RR*  /\  0  <_  ( (
w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m
)  |->  ( w D z ) ) , 
RR* ,  <  ) ) `
 y ) ) )
7371, 72sylib 201 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( (
( w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m )  |->  ( w D z ) ) ,  RR* ,  <  )
) `  y )  e.  RR*  /\  0  <_ 
( ( w  e.  X  |-> inf ( ran  (
z  e.  ( X 
\  m )  |->  ( w D z ) ) ,  RR* ,  <  ) ) `  y ) ) )
7473simprd 469 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  0  <_  ( ( w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m )  |->  ( w D z ) ) ,  RR* ,  <  )
) `  y )
)
75 elndif 3568 . . . . . . . . . 10  |-  ( y  e.  m  ->  -.  y  e.  ( X  \  m ) )
7675ad2antll 740 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  -.  y  e.  ( X  \  m
) )
7753difeq1d 3561 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( X  \  m )  =  ( U. J  \  m
) )
7813mopntop 21503 . . . . . . . . . . . . 13  |-  ( D  e.  ( *Met `  X )  ->  J  e.  Top )
7968, 78syl 17 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  J  e.  Top )
80 eqid 2461 . . . . . . . . . . . . 13  |-  U. J  =  U. J
8180opncld 20096 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  m  e.  J )  ->  ( U. J  \  m )  e.  (
Clsd `  J )
)
8279, 50, 81syl2anc 671 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( U. J  \  m )  e.  ( Clsd `  J
) )
8377, 82eqeltrd 2539 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( X  \  m )  e.  (
Clsd `  J )
)
84 cldcls 20105 . . . . . . . . . 10  |-  ( ( X  \  m )  e.  ( Clsd `  J
)  ->  ( ( cls `  J ) `  ( X  \  m
) )  =  ( X  \  m ) )
8583, 84syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( ( cls `  J ) `  ( X  \  m
) )  =  ( X  \  m ) )
8676, 85neleqtrrd 2561 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  -.  y  e.  ( ( cls `  J
) `  ( X  \  m ) ) )
8743, 13metdseq0 21919 . . . . . . . . . 10  |-  ( ( D  e.  ( *Met `  X )  /\  ( X  \  m )  C_  X  /\  y  e.  X
)  ->  ( (
( w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m )  |->  ( w D z ) ) ,  RR* ,  <  )
) `  y )  =  0  <->  y  e.  ( ( cls `  J
) `  ( X  \  m ) ) ) )
8868, 47, 42, 87syl3anc 1276 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( (
( w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m )  |->  ( w D z ) ) ,  RR* ,  <  )
) `  y )  =  0  <->  y  e.  ( ( cls `  J
) `  ( X  \  m ) ) ) )
8988necon3abid 2671 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( (
( w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m )  |->  ( w D z ) ) ,  RR* ,  <  )
) `  y )  =/=  0  <->  -.  y  e.  ( ( cls `  J
) `  ( X  \  m ) ) ) )
9086, 89mpbird 240 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  ( (
w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m
)  |->  ( w D z ) ) , 
RR* ,  <  ) ) `
 y )  =/=  0 )
9165, 74, 90ne0gt0d 9797 . . . . . 6  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  0  <  ( ( w  e.  X  |-> inf ( ran  ( z  e.  ( X  \  m )  |->  ( w D z ) ) ,  RR* ,  <  )
) `  y )
)
9291, 45breqtrd 4440 . . . . 5  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  0  < inf ( ran  ( z  e.  ( X  \  m
)  |->  ( y D z ) ) , 
RR* ,  <  ) )
931ad2antrr 737 . . . . . 6  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  U  e.  Fin )
9434adantlr 726 . . . . . 6  |-  ( ( ( ( ph  /\  y  e.  X )  /\  ( m  e.  U  /\  y  e.  m
) )  /\  k  e.  U )  -> inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  )  e.  RR )
9512ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  D  e.  ( *Met `  X ) )
9627metdsf 21913 . . . . . . . . . . . 12  |-  ( ( D  e.  ( *Met `  X )  /\  ( X  \ 
k )  C_  X
)  ->  ( y  e.  X  |-> inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  ) ) : X --> ( 0 [,] +oo ) )
9795, 5, 96syl2anc 671 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  (
y  e.  X  |-> inf ( ran  ( z  e.  ( X  \  k
)  |->  ( y D z ) ) , 
RR* ,  <  ) ) : X --> ( 0 [,] +oo ) )
9827fmpt 6065 . . . . . . . . . . 11  |-  ( A. y  e.  X inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  )  e.  ( 0 [,] +oo )  <->  ( y  e.  X  |-> inf ( ran  ( z  e.  ( X  \  k
)  |->  ( y D z ) ) , 
RR* ,  <  ) ) : X --> ( 0 [,] +oo ) )
9997, 98sylibr 217 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  A. y  e.  X inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  )  e.  ( 0 [,] +oo )
)
100 rsp 2765 . . . . . . . . . 10  |-  ( A. y  e.  X inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  )  e.  ( 0 [,] +oo )  ->  ( y  e.  X  -> inf ( ran  ( z  e.  ( X  \ 
k )  |->  ( y D z ) ) ,  RR* ,  <  )  e.  ( 0 [,] +oo ) ) )
10199, 32, 100sylc 62 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  -> inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  )  e.  ( 0 [,] +oo )
)
102 elxrge0 11769 . . . . . . . . 9  |-  (inf ( ran  ( z  e.  ( X  \  k
)  |->  ( y D z ) ) , 
RR* ,  <  )  e.  ( 0 [,] +oo ) 
<->  (inf ( ran  (
z  e.  ( X 
\  k )  |->  ( y D z ) ) ,  RR* ,  <  )  e.  RR*  /\  0  <_ inf ( ran  ( z  e.  ( X  \ 
k )  |->  ( y D z ) ) ,  RR* ,  <  )
) )
103101, 102sylib 201 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  (inf ( ran  ( z  e.  ( X  \  k
)  |->  ( y D z ) ) , 
RR* ,  <  )  e. 
RR*  /\  0  <_ inf ( ran  ( z  e.  ( X  \  k
)  |->  ( y D z ) ) , 
RR* ,  <  ) ) )
104103simprd 469 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  U )  ->  0  <_ inf ( ran  ( z  e.  ( X  \ 
k )  |->  ( y D z ) ) ,  RR* ,  <  )
)
105104adantlr 726 . . . . . 6  |-  ( ( ( ( ph  /\  y  e.  X )  /\  ( m  e.  U  /\  y  e.  m
) )  /\  k  e.  U )  ->  0  <_ inf ( ran  ( z  e.  ( X  \ 
k )  |->  ( y D z ) ) ,  RR* ,  <  )
)
106 difeq2 3556 . . . . . . . . 9  |-  ( k  =  m  ->  ( X  \  k )  =  ( X  \  m
) )
107106mpteq1d 4497 . . . . . . . 8  |-  ( k  =  m  ->  (
z  e.  ( X 
\  k )  |->  ( y D z ) )  =  ( z  e.  ( X  \  m )  |->  ( y D z ) ) )
108107rneqd 5080 . . . . . . 7  |-  ( k  =  m  ->  ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) )  =  ran  ( z  e.  ( X  \  m ) 
|->  ( y D z ) ) )
109108infeq1d 8018 . . . . . 6  |-  ( k  =  m  -> inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  )  = inf ( ran  ( z  e.  ( X  \  m ) 
|->  ( y D z ) ) ,  RR* ,  <  ) )
11093, 94, 105, 109, 49fsumge1 13905 . . . . 5  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  -> inf ( ran  ( z  e.  ( X  \  m ) 
|->  ( y D z ) ) ,  RR* ,  <  )  <_  sum_ k  e.  U inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  ) )
11141, 66, 67, 92, 110ltletrd 9820 . . . 4  |-  ( ( ( ph  /\  y  e.  X )  /\  (
m  e.  U  /\  y  e.  m )
)  ->  0  <  sum_ k  e.  U inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  ) )
11240, 111rexlimddv 2894 . . 3  |-  ( (
ph  /\  y  e.  X )  ->  0  <  sum_ k  e.  U inf ( ran  ( z  e.  ( X  \  k
)  |->  ( y D z ) ) , 
RR* ,  <  ) )
11335, 112elrpd 11366 . 2  |-  ( (
ph  /\  y  e.  X )  ->  sum_ k  e.  U inf ( ran  ( z  e.  ( X  \  k ) 
|->  ( y D z ) ) ,  RR* ,  <  )  e.  RR+ )
114 lebnumlem1.f . 2  |-  F  =  ( y  e.  X  |-> 
sum_ k  e.  U inf ( ran  ( z  e.  ( X  \  k
)  |->  ( y D z ) ) , 
RR* ,  <  ) )
115113, 114fmptd 6068 1  |-  ( ph  ->  F : X --> RR+ )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1454    e. wcel 1897    =/= wne 2632   A.wral 2748   E.wrex 2749    \ cdif 3412    C_ wss 3415   (/)c0 3742   U.cuni 4211   class class class wbr 4415    |-> cmpt 4474   ran crn 4853   -->wf 5596   ` cfv 5600  (class class class)co 6314   Fincfn 7594  infcinf 7980   RRcr 9563   0cc0 9564   +oocpnf 9697   RR*cxr 9699    < clt 9700    <_ cle 9701   RR+crp 11330   [,]cicc 11666   sum_csu 13800   *Metcxmt 19003   Metcme 19004   MetOpencmopn 19008   Topctop 19965   Clsdccld 20079   clsccl 20081   Compccmp 20449
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-inf2 8171  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641  ax-pre-sup 9642
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-fal 1460  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-int 4248  df-iun 4293  df-iin 4294  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-se 4812  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-isom 5609  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-1st 6819  df-2nd 6820  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-1o 7207  df-oadd 7211  df-er 7388  df-ec 7390  df-map 7499  df-en 7595  df-dom 7596  df-sdom 7597  df-fin 7598  df-sup 7981  df-inf 7982  df-oi 8050  df-card 8398  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-div 10297  df-nn 10637  df-2 10695  df-3 10696  df-n0 10898  df-z 10966  df-uz 11188  df-q 11293  df-rp 11331  df-xneg 11437  df-xadd 11438  df-xmul 11439  df-ico 11669  df-icc 11670  df-fz 11813  df-fzo 11946  df-seq 12245  df-exp 12304  df-hash 12547  df-cj 13210  df-re 13211  df-im 13212  df-sqrt 13346  df-abs 13347  df-clim 13600  df-sum 13801  df-topgen 15390  df-psmet 19010  df-xmet 19011  df-met 19012  df-bl 19013  df-mopn 19014  df-top 19969  df-bases 19970  df-topon 19971  df-cld 20082  df-ntr 20083  df-cls 20084
This theorem is referenced by:  lebnumlem2  22038  lebnumlem3  22039
  Copyright terms: Public domain W3C validator