Metamath Proof Explorer

Theorem heiborlem8

Description: Lemma for heibor . The previous lemmas establish that the sequence M is Cauchy, so using completeness we now consider the convergent point Y . By assumption, U is an open cover, so Y is an element of some Z e. U , and some ball centered at Y is contained in Z . But the sequence contains arbitrarily small balls close to Y , so some element ball ( Mn ) of the sequence is contained in Z . And finally we arrive at a contradiction, because { Z } is a finite subcover of U that covers ball ( Mn ) , yet ball ( Mn ) e. K . For convenience, we write this contradiction as ph -> ps where ph is all the accumulated hypotheses and ps is anything at all. (Contributed by Jeff Madsen, 22-Jan-2014)

Ref Expression
Hypotheses heibor.1 
|- J = ( MetOpen ` D )
heibor.3 
|- K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }
heibor.4 
|- G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }
heibor.5 
|- B = ( z e. X , m e. NN0 |-> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )
heibor.6 
|- ( ph -> D e. ( CMet ` X ) )
heibor.7 
|- ( ph -> F : NN0 --> ( ~P X i^i Fin ) )
heibor.8 
|- ( ph -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) )
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 ) )
heibor.10 
|- ( ph -> C G 0 )
heibor.11 
|- S = seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) )
heibor.12 
|- M = ( n e. NN |-> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. )
heibor.13 
|- ( ph -> U C_ J )
heibor.14 
|- Y e. _V
heibor.15 
|- ( ph -> Y e. Z )
heibor.16 
|- ( ph -> Z e. U )
heibor.17 
|- ( ph -> ( 1st o. M ) ( ~~>t ` J ) Y )
Assertion heiborlem8 
|- ( ph -> ps )

Proof

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 ffvelcdmda 
 |-  ( ( 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 )