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 |
|
lebnumlem1.u |
|- ( ph -> U e. Fin ) |
7 |
|
lebnumlem1.n |
|- ( ph -> -. X e. U ) |
8 |
|
lebnumlem1.f |
|- F = ( y e. X |-> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) |
9 |
6
|
adantr |
|- ( ( ph /\ y e. X ) -> U e. Fin ) |
10 |
2
|
ad2antrr |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> D e. ( Met ` X ) ) |
11 |
|
difssd |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> ( X \ k ) C_ X ) |
12 |
4
|
adantr |
|- ( ( ph /\ y e. X ) -> U C_ J ) |
13 |
12
|
sselda |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> k e. J ) |
14 |
|
elssuni |
|- ( k e. J -> k C_ U. J ) |
15 |
13 14
|
syl |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> k C_ U. J ) |
16 |
|
metxmet |
|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) ) |
17 |
2 16
|
syl |
|- ( ph -> D e. ( *Met ` X ) ) |
18 |
1
|
mopnuni |
|- ( D e. ( *Met ` X ) -> X = U. J ) |
19 |
17 18
|
syl |
|- ( ph -> X = U. J ) |
20 |
19
|
ad2antrr |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> X = U. J ) |
21 |
15 20
|
sseqtrrd |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> k C_ X ) |
22 |
|
eleq1 |
|- ( k = X -> ( k e. U <-> X e. U ) ) |
23 |
22
|
notbid |
|- ( k = X -> ( -. k e. U <-> -. X e. U ) ) |
24 |
7 23
|
syl5ibrcom |
|- ( ph -> ( k = X -> -. k e. U ) ) |
25 |
24
|
necon2ad |
|- ( ph -> ( k e. U -> k =/= X ) ) |
26 |
25
|
adantr |
|- ( ( ph /\ y e. X ) -> ( k e. U -> k =/= X ) ) |
27 |
26
|
imp |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> k =/= X ) |
28 |
|
pssdifn0 |
|- ( ( k C_ X /\ k =/= X ) -> ( X \ k ) =/= (/) ) |
29 |
21 27 28
|
syl2anc |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> ( X \ k ) =/= (/) ) |
30 |
|
eqid |
|- ( 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* , < ) ) |
31 |
30
|
metdsre |
|- ( ( 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 ) |
32 |
10 11 29 31
|
syl3anc |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) : X --> RR ) |
33 |
30
|
fmpt |
|- ( 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 ) |
34 |
32 33
|
sylibr |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> A. y e. X inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. RR ) |
35 |
|
simplr |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> y e. X ) |
36 |
|
rsp |
|- ( 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 ) ) |
37 |
34 35 36
|
sylc |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. RR ) |
38 |
9 37
|
fsumrecl |
|- ( ( ph /\ y e. X ) -> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. RR ) |
39 |
5
|
eleq2d |
|- ( ph -> ( y e. X <-> y e. U. U ) ) |
40 |
39
|
biimpa |
|- ( ( ph /\ y e. X ) -> y e. U. U ) |
41 |
|
eluni2 |
|- ( y e. U. U <-> E. m e. U y e. m ) |
42 |
40 41
|
sylib |
|- ( ( ph /\ y e. X ) -> E. m e. U y e. m ) |
43 |
|
0red |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> 0 e. RR ) |
44 |
|
simplr |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> y e. X ) |
45 |
|
eqid |
|- ( 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* , < ) ) |
46 |
45
|
metdsval |
|- ( 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* , < ) ) |
47 |
44 46
|
syl |
|- ( ( ( 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* , < ) ) |
48 |
2
|
ad2antrr |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> D e. ( Met ` X ) ) |
49 |
|
difssd |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( X \ m ) C_ X ) |
50 |
4
|
ad2antrr |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> U C_ J ) |
51 |
|
simprl |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> m e. U ) |
52 |
50 51
|
sseldd |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> m e. J ) |
53 |
|
elssuni |
|- ( m e. J -> m C_ U. J ) |
54 |
52 53
|
syl |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> m C_ U. J ) |
55 |
48 16 18
|
3syl |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> X = U. J ) |
56 |
54 55
|
sseqtrrd |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> m C_ X ) |
57 |
|
eleq1 |
|- ( m = X -> ( m e. U <-> X e. U ) ) |
58 |
57
|
notbid |
|- ( m = X -> ( -. m e. U <-> -. X e. U ) ) |
59 |
7 58
|
syl5ibrcom |
|- ( ph -> ( m = X -> -. m e. U ) ) |
60 |
59
|
necon2ad |
|- ( ph -> ( m e. U -> m =/= X ) ) |
61 |
60
|
ad2antrr |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( m e. U -> m =/= X ) ) |
62 |
51 61
|
mpd |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> m =/= X ) |
63 |
|
pssdifn0 |
|- ( ( m C_ X /\ m =/= X ) -> ( X \ m ) =/= (/) ) |
64 |
56 62 63
|
syl2anc |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( X \ m ) =/= (/) ) |
65 |
45
|
metdsre |
|- ( ( 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 ) |
66 |
48 49 64 65
|
syl3anc |
|- ( ( ( 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 ) |
67 |
66 44
|
ffvelrnd |
|- ( ( ( 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 ) |
68 |
47 67
|
eqeltrrd |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> inf ( ran ( z e. ( X \ m ) |-> ( y D z ) ) , RR* , < ) e. RR ) |
69 |
38
|
adantr |
|- ( ( ( 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 ) |
70 |
17
|
ad2antrr |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> D e. ( *Met ` X ) ) |
71 |
45
|
metdsf |
|- ( ( D e. ( *Met ` X ) /\ ( X \ m ) C_ X ) -> ( w e. X |-> inf ( ran ( z e. ( X \ m ) |-> ( w D z ) ) , RR* , < ) ) : X --> ( 0 [,] +oo ) ) |
72 |
70 49 71
|
syl2anc |
|- ( ( ( 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 ) ) |
73 |
72 44
|
ffvelrnd |
|- ( ( ( 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 ) ) |
74 |
|
elxrge0 |
|- ( ( ( 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 ) ) ) |
75 |
73 74
|
sylib |
|- ( ( ( 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 ) ) ) |
76 |
75
|
simprd |
|- ( ( ( 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 ) ) |
77 |
|
elndif |
|- ( y e. m -> -. y e. ( X \ m ) ) |
78 |
77
|
ad2antll |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> -. y e. ( X \ m ) ) |
79 |
55
|
difeq1d |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( X \ m ) = ( U. J \ m ) ) |
80 |
1
|
mopntop |
|- ( D e. ( *Met ` X ) -> J e. Top ) |
81 |
70 80
|
syl |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> J e. Top ) |
82 |
|
eqid |
|- U. J = U. J |
83 |
82
|
opncld |
|- ( ( J e. Top /\ m e. J ) -> ( U. J \ m ) e. ( Clsd ` J ) ) |
84 |
81 52 83
|
syl2anc |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( U. J \ m ) e. ( Clsd ` J ) ) |
85 |
79 84
|
eqeltrd |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( X \ m ) e. ( Clsd ` J ) ) |
86 |
|
cldcls |
|- ( ( X \ m ) e. ( Clsd ` J ) -> ( ( cls ` J ) ` ( X \ m ) ) = ( X \ m ) ) |
87 |
85 86
|
syl |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> ( ( cls ` J ) ` ( X \ m ) ) = ( X \ m ) ) |
88 |
78 87
|
neleqtrrd |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> -. y e. ( ( cls ` J ) ` ( X \ m ) ) ) |
89 |
45 1
|
metdseq0 |
|- ( ( 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 ) ) ) ) |
90 |
70 49 44 89
|
syl3anc |
|- ( ( ( 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 ) ) ) ) |
91 |
90
|
necon3abid |
|- ( ( ( 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 ) ) ) ) |
92 |
88 91
|
mpbird |
|- ( ( ( 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 ) |
93 |
67 76 92
|
ne0gt0d |
|- ( ( ( 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 ) ) |
94 |
93 47
|
breqtrd |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> 0 < inf ( ran ( z e. ( X \ m ) |-> ( y D z ) ) , RR* , < ) ) |
95 |
6
|
ad2antrr |
|- ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) -> U e. Fin ) |
96 |
37
|
adantlr |
|- ( ( ( ( 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 ) |
97 |
17
|
ad2antrr |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> D e. ( *Met ` X ) ) |
98 |
30
|
metdsf |
|- ( ( D e. ( *Met ` X ) /\ ( X \ k ) C_ X ) -> ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) : X --> ( 0 [,] +oo ) ) |
99 |
97 11 98
|
syl2anc |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> ( y e. X |-> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) : X --> ( 0 [,] +oo ) ) |
100 |
30
|
fmpt |
|- ( 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 ) ) |
101 |
99 100
|
sylibr |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> A. y e. X inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. ( 0 [,] +oo ) ) |
102 |
|
rsp |
|- ( 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 ) ) ) |
103 |
101 35 102
|
sylc |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. ( 0 [,] +oo ) ) |
104 |
|
elxrge0 |
|- ( 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* , < ) ) ) |
105 |
103 104
|
sylib |
|- ( ( ( 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* , < ) ) ) |
106 |
105
|
simprd |
|- ( ( ( ph /\ y e. X ) /\ k e. U ) -> 0 <_ inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) |
107 |
106
|
adantlr |
|- ( ( ( ( ph /\ y e. X ) /\ ( m e. U /\ y e. m ) ) /\ k e. U ) -> 0 <_ inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) |
108 |
|
difeq2 |
|- ( k = m -> ( X \ k ) = ( X \ m ) ) |
109 |
108
|
mpteq1d |
|- ( k = m -> ( z e. ( X \ k ) |-> ( y D z ) ) = ( z e. ( X \ m ) |-> ( y D z ) ) ) |
110 |
109
|
rneqd |
|- ( k = m -> ran ( z e. ( X \ k ) |-> ( y D z ) ) = ran ( z e. ( X \ m ) |-> ( y D z ) ) ) |
111 |
110
|
infeq1d |
|- ( k = m -> inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) = inf ( ran ( z e. ( X \ m ) |-> ( y D z ) ) , RR* , < ) ) |
112 |
95 96 107 111 51
|
fsumge1 |
|- ( ( ( 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* , < ) ) |
113 |
43 68 69 94 112
|
ltletrd |
|- ( ( ( 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* , < ) ) |
114 |
42 113
|
rexlimddv |
|- ( ( ph /\ y e. X ) -> 0 < sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) |
115 |
38 114
|
elrpd |
|- ( ( ph /\ y e. X ) -> sum_ k e. U inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) e. RR+ ) |
116 |
115 8
|
fmptd |
|- ( ph -> F : X --> RR+ ) |