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