Step |
Hyp |
Ref |
Expression |
1 |
|
heibor.1 |
|- J = ( MetOpen ` D ) |
2 |
|
heibor.3 |
|- K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v } |
3 |
|
heibor.4 |
|- G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) } |
4 |
|
heibor.5 |
|- B = ( z e. X , m e. NN0 |-> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) ) |
5 |
|
heibor.6 |
|- ( ph -> D e. ( CMet ` X ) ) |
6 |
|
heibor.7 |
|- ( ph -> F : NN0 --> ( ~P X i^i Fin ) ) |
7 |
|
heibor.8 |
|- ( ph -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) ) |
8 |
|
heibor.9 |
|- ( ph -> A. x e. G ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) ) |
9 |
|
heibor.10 |
|- ( ph -> C G 0 ) |
10 |
|
heibor.11 |
|- S = seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) ) |
11 |
|
heibor.12 |
|- M = ( n e. NN |-> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. ) |
12 |
|
heibor.13 |
|- ( ph -> U C_ J ) |
13 |
|
heibor.14 |
|- Y e. _V |
14 |
|
heibor.15 |
|- ( ph -> Y e. Z ) |
15 |
|
heibor.16 |
|- ( ph -> Z e. U ) |
16 |
|
heibor.17 |
|- ( ph -> ( 1st o. M ) ( ~~>t ` J ) Y ) |
17 |
|
cmetmet |
|- ( D e. ( CMet ` X ) -> D e. ( Met ` X ) ) |
18 |
|
metxmet |
|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) ) |
19 |
5 17 18
|
3syl |
|- ( ph -> D e. ( *Met ` X ) ) |
20 |
12 15
|
sseldd |
|- ( ph -> Z e. J ) |
21 |
1
|
mopni2 |
|- ( ( D e. ( *Met ` X ) /\ Z e. J /\ Y e. Z ) -> E. x e. RR+ ( Y ( ball ` D ) x ) C_ Z ) |
22 |
19 20 14 21
|
syl3anc |
|- ( ph -> E. x e. RR+ ( Y ( ball ` D ) x ) C_ Z ) |
23 |
|
rphalfcl |
|- ( x e. RR+ -> ( x / 2 ) e. RR+ ) |
24 |
|
breq2 |
|- ( r = ( x / 2 ) -> ( ( 2nd ` ( M ` k ) ) < r <-> ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) |
25 |
24
|
rexbidv |
|- ( r = ( x / 2 ) -> ( E. k e. NN ( 2nd ` ( M ` k ) ) < r <-> E. k e. NN ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) |
26 |
1 2 3 4 5 6 7 8 9 10 11
|
heiborlem7 |
|- A. r e. RR+ E. k e. NN ( 2nd ` ( M ` k ) ) < r |
27 |
25 26
|
vtoclri |
|- ( ( x / 2 ) e. RR+ -> E. k e. NN ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) |
28 |
23 27
|
syl |
|- ( x e. RR+ -> E. k e. NN ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) |
29 |
28
|
adantl |
|- ( ( ph /\ x e. RR+ ) -> E. k e. NN ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) |
30 |
|
nnnn0 |
|- ( k e. NN -> k e. NN0 ) |
31 |
1 2 3 4 5 6 7 8 9 10
|
heiborlem4 |
|- ( ( ph /\ k e. NN0 ) -> ( S ` k ) G k ) |
32 |
|
fvex |
|- ( S ` k ) e. _V |
33 |
|
vex |
|- k e. _V |
34 |
1 2 3 32 33
|
heiborlem2 |
|- ( ( S ` k ) G k <-> ( k e. NN0 /\ ( S ` k ) e. ( F ` k ) /\ ( ( S ` k ) B k ) e. K ) ) |
35 |
34
|
simp3bi |
|- ( ( S ` k ) G k -> ( ( S ` k ) B k ) e. K ) |
36 |
31 35
|
syl |
|- ( ( ph /\ k e. NN0 ) -> ( ( S ` k ) B k ) e. K ) |
37 |
30 36
|
sylan2 |
|- ( ( ph /\ k e. NN ) -> ( ( S ` k ) B k ) e. K ) |
38 |
37
|
ad2ant2r |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( S ` k ) B k ) e. K ) |
39 |
19
|
ad2antrr |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> D e. ( *Met ` X ) ) |
40 |
1 2 3 4 5 6 7 8 9 10 11
|
heiborlem5 |
|- ( ph -> M : NN --> ( X X. RR+ ) ) |
41 |
40
|
ffvelrnda |
|- ( ( ph /\ k e. NN ) -> ( M ` k ) e. ( X X. RR+ ) ) |
42 |
41
|
ad2ant2r |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( M ` k ) e. ( X X. RR+ ) ) |
43 |
|
xp1st |
|- ( ( M ` k ) e. ( X X. RR+ ) -> ( 1st ` ( M ` k ) ) e. X ) |
44 |
42 43
|
syl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( 1st ` ( M ` k ) ) e. X ) |
45 |
|
2nn |
|- 2 e. NN |
46 |
|
nnexpcl |
|- ( ( 2 e. NN /\ k e. NN0 ) -> ( 2 ^ k ) e. NN ) |
47 |
45 30 46
|
sylancr |
|- ( k e. NN -> ( 2 ^ k ) e. NN ) |
48 |
47
|
nnrpd |
|- ( k e. NN -> ( 2 ^ k ) e. RR+ ) |
49 |
48
|
rpreccld |
|- ( k e. NN -> ( 1 / ( 2 ^ k ) ) e. RR+ ) |
50 |
49
|
ad2antrl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( 1 / ( 2 ^ k ) ) e. RR+ ) |
51 |
50
|
rpxrd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( 1 / ( 2 ^ k ) ) e. RR* ) |
52 |
|
xp2nd |
|- ( ( M ` k ) e. ( X X. RR+ ) -> ( 2nd ` ( M ` k ) ) e. RR+ ) |
53 |
42 52
|
syl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( 2nd ` ( M ` k ) ) e. RR+ ) |
54 |
53
|
rpxrd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( 2nd ` ( M ` k ) ) e. RR* ) |
55 |
|
1le3 |
|- 1 <_ 3 |
56 |
|
elrp |
|- ( ( 2 ^ k ) e. RR+ <-> ( ( 2 ^ k ) e. RR /\ 0 < ( 2 ^ k ) ) ) |
57 |
|
1re |
|- 1 e. RR |
58 |
|
3re |
|- 3 e. RR |
59 |
|
lediv1 |
|- ( ( 1 e. RR /\ 3 e. RR /\ ( ( 2 ^ k ) e. RR /\ 0 < ( 2 ^ k ) ) ) -> ( 1 <_ 3 <-> ( 1 / ( 2 ^ k ) ) <_ ( 3 / ( 2 ^ k ) ) ) ) |
60 |
57 58 59
|
mp3an12 |
|- ( ( ( 2 ^ k ) e. RR /\ 0 < ( 2 ^ k ) ) -> ( 1 <_ 3 <-> ( 1 / ( 2 ^ k ) ) <_ ( 3 / ( 2 ^ k ) ) ) ) |
61 |
56 60
|
sylbi |
|- ( ( 2 ^ k ) e. RR+ -> ( 1 <_ 3 <-> ( 1 / ( 2 ^ k ) ) <_ ( 3 / ( 2 ^ k ) ) ) ) |
62 |
55 61
|
mpbii |
|- ( ( 2 ^ k ) e. RR+ -> ( 1 / ( 2 ^ k ) ) <_ ( 3 / ( 2 ^ k ) ) ) |
63 |
48 62
|
syl |
|- ( k e. NN -> ( 1 / ( 2 ^ k ) ) <_ ( 3 / ( 2 ^ k ) ) ) |
64 |
63
|
ad2antrl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( 1 / ( 2 ^ k ) ) <_ ( 3 / ( 2 ^ k ) ) ) |
65 |
|
fveq2 |
|- ( n = k -> ( S ` n ) = ( S ` k ) ) |
66 |
|
oveq2 |
|- ( n = k -> ( 2 ^ n ) = ( 2 ^ k ) ) |
67 |
66
|
oveq2d |
|- ( n = k -> ( 3 / ( 2 ^ n ) ) = ( 3 / ( 2 ^ k ) ) ) |
68 |
65 67
|
opeq12d |
|- ( n = k -> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. = <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. ) |
69 |
|
opex |
|- <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. e. _V |
70 |
68 11 69
|
fvmpt |
|- ( k e. NN -> ( M ` k ) = <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. ) |
71 |
70
|
fveq2d |
|- ( k e. NN -> ( 2nd ` ( M ` k ) ) = ( 2nd ` <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. ) ) |
72 |
|
ovex |
|- ( 3 / ( 2 ^ k ) ) e. _V |
73 |
32 72
|
op2nd |
|- ( 2nd ` <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. ) = ( 3 / ( 2 ^ k ) ) |
74 |
71 73
|
eqtrdi |
|- ( k e. NN -> ( 2nd ` ( M ` k ) ) = ( 3 / ( 2 ^ k ) ) ) |
75 |
74
|
ad2antrl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( 2nd ` ( M ` k ) ) = ( 3 / ( 2 ^ k ) ) ) |
76 |
64 75
|
breqtrrd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( 1 / ( 2 ^ k ) ) <_ ( 2nd ` ( M ` k ) ) ) |
77 |
|
ssbl |
|- ( ( ( D e. ( *Met ` X ) /\ ( 1st ` ( M ` k ) ) e. X ) /\ ( ( 1 / ( 2 ^ k ) ) e. RR* /\ ( 2nd ` ( M ` k ) ) e. RR* ) /\ ( 1 / ( 2 ^ k ) ) <_ ( 2nd ` ( M ` k ) ) ) -> ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 1 / ( 2 ^ k ) ) ) C_ ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 2nd ` ( M ` k ) ) ) ) |
78 |
39 44 51 54 76 77
|
syl221anc |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 1 / ( 2 ^ k ) ) ) C_ ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 2nd ` ( M ` k ) ) ) ) |
79 |
30
|
ad2antrl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> k e. NN0 ) |
80 |
|
oveq1 |
|- ( z = ( 1st ` ( M ` k ) ) -> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) = ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) ) |
81 |
|
oveq2 |
|- ( m = k -> ( 2 ^ m ) = ( 2 ^ k ) ) |
82 |
81
|
oveq2d |
|- ( m = k -> ( 1 / ( 2 ^ m ) ) = ( 1 / ( 2 ^ k ) ) ) |
83 |
82
|
oveq2d |
|- ( m = k -> ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) = ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 1 / ( 2 ^ k ) ) ) ) |
84 |
|
ovex |
|- ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 1 / ( 2 ^ k ) ) ) e. _V |
85 |
80 83 4 84
|
ovmpo |
|- ( ( ( 1st ` ( M ` k ) ) e. X /\ k e. NN0 ) -> ( ( 1st ` ( M ` k ) ) B k ) = ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 1 / ( 2 ^ k ) ) ) ) |
86 |
44 79 85
|
syl2anc |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( 1st ` ( M ` k ) ) B k ) = ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 1 / ( 2 ^ k ) ) ) ) |
87 |
70
|
fveq2d |
|- ( k e. NN -> ( 1st ` ( M ` k ) ) = ( 1st ` <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. ) ) |
88 |
32 72
|
op1st |
|- ( 1st ` <. ( S ` k ) , ( 3 / ( 2 ^ k ) ) >. ) = ( S ` k ) |
89 |
87 88
|
eqtrdi |
|- ( k e. NN -> ( 1st ` ( M ` k ) ) = ( S ` k ) ) |
90 |
89
|
ad2antrl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( 1st ` ( M ` k ) ) = ( S ` k ) ) |
91 |
90
|
oveq1d |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( 1st ` ( M ` k ) ) B k ) = ( ( S ` k ) B k ) ) |
92 |
86 91
|
eqtr3d |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 1 / ( 2 ^ k ) ) ) = ( ( S ` k ) B k ) ) |
93 |
|
df-ov |
|- ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 2nd ` ( M ` k ) ) ) = ( ( ball ` D ) ` <. ( 1st ` ( M ` k ) ) , ( 2nd ` ( M ` k ) ) >. ) |
94 |
|
1st2nd2 |
|- ( ( M ` k ) e. ( X X. RR+ ) -> ( M ` k ) = <. ( 1st ` ( M ` k ) ) , ( 2nd ` ( M ` k ) ) >. ) |
95 |
42 94
|
syl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( M ` k ) = <. ( 1st ` ( M ` k ) ) , ( 2nd ` ( M ` k ) ) >. ) |
96 |
95
|
fveq2d |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( ball ` D ) ` ( M ` k ) ) = ( ( ball ` D ) ` <. ( 1st ` ( M ` k ) ) , ( 2nd ` ( M ` k ) ) >. ) ) |
97 |
93 96
|
eqtr4id |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 2nd ` ( M ` k ) ) ) = ( ( ball ` D ) ` ( M ` k ) ) ) |
98 |
78 92 97
|
3sstr3d |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( S ` k ) B k ) C_ ( ( ball ` D ) ` ( M ` k ) ) ) |
99 |
1
|
mopntop |
|- ( D e. ( *Met ` X ) -> J e. Top ) |
100 |
39 99
|
syl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> J e. Top ) |
101 |
|
blssm |
|- ( ( D e. ( *Met ` X ) /\ ( 1st ` ( M ` k ) ) e. X /\ ( 2nd ` ( M ` k ) ) e. RR* ) -> ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 2nd ` ( M ` k ) ) ) C_ X ) |
102 |
39 44 54 101
|
syl3anc |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 2nd ` ( M ` k ) ) ) C_ X ) |
103 |
1
|
mopnuni |
|- ( D e. ( *Met ` X ) -> X = U. J ) |
104 |
39 103
|
syl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> X = U. J ) |
105 |
102 97 104
|
3sstr3d |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( ball ` D ) ` ( M ` k ) ) C_ U. J ) |
106 |
|
eqid |
|- U. J = U. J |
107 |
106
|
sscls |
|- ( ( J e. Top /\ ( ( ball ` D ) ` ( M ` k ) ) C_ U. J ) -> ( ( ball ` D ) ` ( M ` k ) ) C_ ( ( cls ` J ) ` ( ( ball ` D ) ` ( M ` k ) ) ) ) |
108 |
100 105 107
|
syl2anc |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( ball ` D ) ` ( M ` k ) ) C_ ( ( cls ` J ) ` ( ( ball ` D ) ` ( M ` k ) ) ) ) |
109 |
97
|
fveq2d |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( cls ` J ) ` ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 2nd ` ( M ` k ) ) ) ) = ( ( cls ` J ) ` ( ( ball ` D ) ` ( M ` k ) ) ) ) |
110 |
23
|
ad2antlr |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( x / 2 ) e. RR+ ) |
111 |
110
|
rpxrd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( x / 2 ) e. RR* ) |
112 |
|
simprr |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) |
113 |
1
|
blsscls |
|- ( ( ( D e. ( *Met ` X ) /\ ( 1st ` ( M ` k ) ) e. X ) /\ ( ( 2nd ` ( M ` k ) ) e. RR* /\ ( x / 2 ) e. RR* /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( cls ` J ) ` ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 2nd ` ( M ` k ) ) ) ) C_ ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( x / 2 ) ) ) |
114 |
39 44 54 111 112 113
|
syl23anc |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( cls ` J ) ` ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( 2nd ` ( M ` k ) ) ) ) C_ ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( x / 2 ) ) ) |
115 |
109 114
|
eqsstrrd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( cls ` J ) ` ( ( ball ` D ) ` ( M ` k ) ) ) C_ ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( x / 2 ) ) ) |
116 |
|
rpre |
|- ( x e. RR+ -> x e. RR ) |
117 |
116
|
ad2antlr |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> x e. RR ) |
118 |
1 2 3 4 5 6 7 8 9 10 11
|
heiborlem6 |
|- ( ph -> A. t e. NN ( ( ball ` D ) ` ( M ` ( t + 1 ) ) ) C_ ( ( ball ` D ) ` ( M ` t ) ) ) |
119 |
19 40 118 1
|
caublcls |
|- ( ( ph /\ ( 1st o. M ) ( ~~>t ` J ) Y /\ k e. NN ) -> Y e. ( ( cls ` J ) ` ( ( ball ` D ) ` ( M ` k ) ) ) ) |
120 |
119
|
3expia |
|- ( ( ph /\ ( 1st o. M ) ( ~~>t ` J ) Y ) -> ( k e. NN -> Y e. ( ( cls ` J ) ` ( ( ball ` D ) ` ( M ` k ) ) ) ) ) |
121 |
16 120
|
mpdan |
|- ( ph -> ( k e. NN -> Y e. ( ( cls ` J ) ` ( ( ball ` D ) ` ( M ` k ) ) ) ) ) |
122 |
121
|
imp |
|- ( ( ph /\ k e. NN ) -> Y e. ( ( cls ` J ) ` ( ( ball ` D ) ` ( M ` k ) ) ) ) |
123 |
122
|
ad2ant2r |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> Y e. ( ( cls ` J ) ` ( ( ball ` D ) ` ( M ` k ) ) ) ) |
124 |
115 123
|
sseldd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> Y e. ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( x / 2 ) ) ) |
125 |
|
blhalf |
|- ( ( ( D e. ( *Met ` X ) /\ ( 1st ` ( M ` k ) ) e. X ) /\ ( x e. RR /\ Y e. ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( x / 2 ) ) ) ) -> ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( x / 2 ) ) C_ ( Y ( ball ` D ) x ) ) |
126 |
39 44 117 124 125
|
syl22anc |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( 1st ` ( M ` k ) ) ( ball ` D ) ( x / 2 ) ) C_ ( Y ( ball ` D ) x ) ) |
127 |
115 126
|
sstrd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( cls ` J ) ` ( ( ball ` D ) ` ( M ` k ) ) ) C_ ( Y ( ball ` D ) x ) ) |
128 |
108 127
|
sstrd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( ball ` D ) ` ( M ` k ) ) C_ ( Y ( ball ` D ) x ) ) |
129 |
98 128
|
sstrd |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( S ` k ) B k ) C_ ( Y ( ball ` D ) x ) ) |
130 |
|
sstr2 |
|- ( ( ( S ` k ) B k ) C_ ( Y ( ball ` D ) x ) -> ( ( Y ( ball ` D ) x ) C_ Z -> ( ( S ` k ) B k ) C_ Z ) ) |
131 |
129 130
|
syl |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( Y ( ball ` D ) x ) C_ Z -> ( ( S ` k ) B k ) C_ Z ) ) |
132 |
|
unisng |
|- ( Z e. U -> U. { Z } = Z ) |
133 |
15 132
|
syl |
|- ( ph -> U. { Z } = Z ) |
134 |
133
|
sseq2d |
|- ( ph -> ( ( ( S ` k ) B k ) C_ U. { Z } <-> ( ( S ` k ) B k ) C_ Z ) ) |
135 |
134
|
biimpar |
|- ( ( ph /\ ( ( S ` k ) B k ) C_ Z ) -> ( ( S ` k ) B k ) C_ U. { Z } ) |
136 |
15
|
snssd |
|- ( ph -> { Z } C_ U ) |
137 |
|
snex |
|- { Z } e. _V |
138 |
137
|
elpw |
|- ( { Z } e. ~P U <-> { Z } C_ U ) |
139 |
136 138
|
sylibr |
|- ( ph -> { Z } e. ~P U ) |
140 |
|
snfi |
|- { Z } e. Fin |
141 |
140
|
a1i |
|- ( ph -> { Z } e. Fin ) |
142 |
139 141
|
elind |
|- ( ph -> { Z } e. ( ~P U i^i Fin ) ) |
143 |
|
unieq |
|- ( v = { Z } -> U. v = U. { Z } ) |
144 |
143
|
sseq2d |
|- ( v = { Z } -> ( ( ( S ` k ) B k ) C_ U. v <-> ( ( S ` k ) B k ) C_ U. { Z } ) ) |
145 |
144
|
rspcev |
|- ( ( { Z } e. ( ~P U i^i Fin ) /\ ( ( S ` k ) B k ) C_ U. { Z } ) -> E. v e. ( ~P U i^i Fin ) ( ( S ` k ) B k ) C_ U. v ) |
146 |
142 145
|
sylan |
|- ( ( ph /\ ( ( S ` k ) B k ) C_ U. { Z } ) -> E. v e. ( ~P U i^i Fin ) ( ( S ` k ) B k ) C_ U. v ) |
147 |
135 146
|
syldan |
|- ( ( ph /\ ( ( S ` k ) B k ) C_ Z ) -> E. v e. ( ~P U i^i Fin ) ( ( S ` k ) B k ) C_ U. v ) |
148 |
|
ovex |
|- ( ( S ` k ) B k ) e. _V |
149 |
|
sseq1 |
|- ( u = ( ( S ` k ) B k ) -> ( u C_ U. v <-> ( ( S ` k ) B k ) C_ U. v ) ) |
150 |
149
|
rexbidv |
|- ( u = ( ( S ` k ) B k ) -> ( E. v e. ( ~P U i^i Fin ) u C_ U. v <-> E. v e. ( ~P U i^i Fin ) ( ( S ` k ) B k ) C_ U. v ) ) |
151 |
150
|
notbid |
|- ( u = ( ( S ` k ) B k ) -> ( -. E. v e. ( ~P U i^i Fin ) u C_ U. v <-> -. E. v e. ( ~P U i^i Fin ) ( ( S ` k ) B k ) C_ U. v ) ) |
152 |
148 151 2
|
elab2 |
|- ( ( ( S ` k ) B k ) e. K <-> -. E. v e. ( ~P U i^i Fin ) ( ( S ` k ) B k ) C_ U. v ) |
153 |
152
|
con2bii |
|- ( E. v e. ( ~P U i^i Fin ) ( ( S ` k ) B k ) C_ U. v <-> -. ( ( S ` k ) B k ) e. K ) |
154 |
147 153
|
sylib |
|- ( ( ph /\ ( ( S ` k ) B k ) C_ Z ) -> -. ( ( S ` k ) B k ) e. K ) |
155 |
154
|
ex |
|- ( ph -> ( ( ( S ` k ) B k ) C_ Z -> -. ( ( S ` k ) B k ) e. K ) ) |
156 |
155
|
ad2antrr |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( ( S ` k ) B k ) C_ Z -> -. ( ( S ` k ) B k ) e. K ) ) |
157 |
131 156
|
syld |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> ( ( Y ( ball ` D ) x ) C_ Z -> -. ( ( S ` k ) B k ) e. K ) ) |
158 |
38 157
|
mt2d |
|- ( ( ( ph /\ x e. RR+ ) /\ ( k e. NN /\ ( 2nd ` ( M ` k ) ) < ( x / 2 ) ) ) -> -. ( Y ( ball ` D ) x ) C_ Z ) |
159 |
29 158
|
rexlimddv |
|- ( ( ph /\ x e. RR+ ) -> -. ( Y ( ball ` D ) x ) C_ Z ) |
160 |
159
|
nrexdv |
|- ( ph -> -. E. x e. RR+ ( Y ( ball ` D ) x ) C_ Z ) |
161 |
22 160
|
pm2.21dd |
|- ( ph -> ps ) |