Description: Lemma for bcth . The proof makes essential use of the Axiom of Dependent Choice axdc4uz , which in the form used here accepts a "selection" function F from each element of K to a nonempty subset of K , and the result function g maps g ( n + 1 ) to an element of F ( n , g ( n ) ) . The trick here is thus in the choice of F and K : we let K be the set of all tagged nonempty open sets (tagged here meaning that we have a point and an open set, in an ordered pair), and F ( k , <. x , z >. ) gives the set of all balls of size less than 1 / k , tagged by their centers, whose closures fit within the given open set z and miss M ( k ) .
Since M ( k ) is closed, z \ M ( k ) is open and also nonempty, since z is nonempty and M ( k ) has empty interior. Then there is some ball contained in it, and hence our function F is valid (it never maps to the empty set). Now starting at a point in the interior of U. ran M , DC gives us the function g all whose elements are constrained by F acting on the previous value. (This is all proven in this lemma.) Now g is a sequence of tagged open balls, forming an inclusion chain (see bcthlem2 ) and whose sizes tend to zero, since they are bounded above by 1 / k . Thus, the centers of these balls form a Cauchy sequence, and converge to a point x (see bcthlem4 ). Since the inclusion chain also ensures the closure of each ball is in the previous ball, the point x must be in all these balls (see bcthlem3 ) and hence misses each M ( k ) , contradicting the fact that x is in the interior of U. ran M (which was the starting point). (Contributed by Mario Carneiro, 6-Jan-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | bcth.2 | |- J = ( MetOpen ` D ) |
|
| bcthlem.4 | |- ( ph -> D e. ( CMet ` X ) ) |
||
| bcthlem.5 | |- F = ( k e. NN , z e. ( X X. RR+ ) |-> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } ) |
||
| bcthlem.6 | |- ( ph -> M : NN --> ( Clsd ` J ) ) |
||
| bcthlem5.7 | |- ( ph -> A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) ) |
||
| Assertion | bcthlem5 | |- ( ph -> ( ( int ` J ) ` U. ran M ) = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bcth.2 | |- J = ( MetOpen ` D ) |
|
| 2 | bcthlem.4 | |- ( ph -> D e. ( CMet ` X ) ) |
|
| 3 | bcthlem.5 | |- F = ( k e. NN , z e. ( X X. RR+ ) |-> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } ) |
|
| 4 | bcthlem.6 | |- ( ph -> M : NN --> ( Clsd ` J ) ) |
|
| 5 | bcthlem5.7 | |- ( ph -> A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) ) |
|
| 6 | cmetmet | |- ( D e. ( CMet ` X ) -> D e. ( Met ` X ) ) |
|
| 7 | metxmet | |- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) ) |
|
| 8 | 2 6 7 | 3syl | |- ( ph -> D e. ( *Met ` X ) ) |
| 9 | 1 | mopntop | |- ( D e. ( *Met ` X ) -> J e. Top ) |
| 10 | 8 9 | syl | |- ( ph -> J e. Top ) |
| 11 | 4 | frnd | |- ( ph -> ran M C_ ( Clsd ` J ) ) |
| 12 | eqid | |- U. J = U. J |
|
| 13 | 12 | cldss2 | |- ( Clsd ` J ) C_ ~P U. J |
| 14 | 11 13 | sstrdi | |- ( ph -> ran M C_ ~P U. J ) |
| 15 | sspwuni | |- ( ran M C_ ~P U. J <-> U. ran M C_ U. J ) |
|
| 16 | 14 15 | sylib | |- ( ph -> U. ran M C_ U. J ) |
| 17 | 12 | ntropn | |- ( ( J e. Top /\ U. ran M C_ U. J ) -> ( ( int ` J ) ` U. ran M ) e. J ) |
| 18 | 10 16 17 | syl2anc | |- ( ph -> ( ( int ` J ) ` U. ran M ) e. J ) |
| 19 | 8 18 | jca | |- ( ph -> ( D e. ( *Met ` X ) /\ ( ( int ` J ) ` U. ran M ) e. J ) ) |
| 20 | 1 | mopni2 | |- ( ( D e. ( *Met ` X ) /\ ( ( int ` J ) ` U. ran M ) e. J /\ n e. ( ( int ` J ) ` U. ran M ) ) -> E. m e. RR+ ( n ( ball ` D ) m ) C_ ( ( int ` J ) ` U. ran M ) ) |
| 21 | 20 | 3expa | |- ( ( ( D e. ( *Met ` X ) /\ ( ( int ` J ) ` U. ran M ) e. J ) /\ n e. ( ( int ` J ) ` U. ran M ) ) -> E. m e. RR+ ( n ( ball ` D ) m ) C_ ( ( int ` J ) ` U. ran M ) ) |
| 22 | 19 21 | sylan | |- ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) ) -> E. m e. RR+ ( n ( ball ` D ) m ) C_ ( ( int ` J ) ` U. ran M ) ) |
| 23 | 1 | mopnuni | |- ( D e. ( *Met ` X ) -> X = U. J ) |
| 24 | 8 23 | syl | |- ( ph -> X = U. J ) |
| 25 | 12 | topopn | |- ( J e. Top -> U. J e. J ) |
| 26 | 10 25 | syl | |- ( ph -> U. J e. J ) |
| 27 | 24 26 | eqeltrd | |- ( ph -> X e. J ) |
| 28 | reex | |- RR e. _V |
|
| 29 | rpssre | |- RR+ C_ RR |
|
| 30 | 28 29 | ssexi | |- RR+ e. _V |
| 31 | xpexg | |- ( ( X e. J /\ RR+ e. _V ) -> ( X X. RR+ ) e. _V ) |
|
| 32 | 27 30 31 | sylancl | |- ( ph -> ( X X. RR+ ) e. _V ) |
| 33 | 32 | 3ad2ant1 | |- ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) -> ( X X. RR+ ) e. _V ) |
| 34 | 12 | ntrss3 | |- ( ( J e. Top /\ U. ran M C_ U. J ) -> ( ( int ` J ) ` U. ran M ) C_ U. J ) |
| 35 | 10 16 34 | syl2anc | |- ( ph -> ( ( int ` J ) ` U. ran M ) C_ U. J ) |
| 36 | 35 24 | sseqtrrd | |- ( ph -> ( ( int ` J ) ` U. ran M ) C_ X ) |
| 37 | 36 | 3ad2ant1 | |- ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) -> ( ( int ` J ) ` U. ran M ) C_ X ) |
| 38 | simp2 | |- ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) -> n e. ( ( int ` J ) ` U. ran M ) ) |
|
| 39 | 37 38 | sseldd | |- ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) -> n e. X ) |
| 40 | simp3 | |- ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) -> m e. RR+ ) |
|
| 41 | 39 40 | opelxpd | |- ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) -> <. n , m >. e. ( X X. RR+ ) ) |
| 42 | opabssxp | |- { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } C_ ( X X. RR+ ) |
|
| 43 | elpw2g | |- ( ( X X. RR+ ) e. _V -> ( { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } e. ~P ( X X. RR+ ) <-> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } C_ ( X X. RR+ ) ) ) |
|
| 44 | 32 43 | syl | |- ( ph -> ( { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } e. ~P ( X X. RR+ ) <-> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } C_ ( X X. RR+ ) ) ) |
| 45 | 44 | adantr | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } e. ~P ( X X. RR+ ) <-> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } C_ ( X X. RR+ ) ) ) |
| 46 | 42 45 | mpbiri | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } e. ~P ( X X. RR+ ) ) |
| 47 | simpl | |- ( ( k e. NN /\ z e. ( X X. RR+ ) ) -> k e. NN ) |
|
| 48 | rspa | |- ( ( A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) /\ k e. NN ) -> ( ( int ` J ) ` ( M ` k ) ) = (/) ) |
|
| 49 | 5 47 48 | syl2an | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( int ` J ) ` ( M ` k ) ) = (/) ) |
| 50 | ssdif0 | |- ( ( ( ball ` D ) ` z ) C_ ( M ` k ) <-> ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) = (/) ) |
|
| 51 | 1st2nd2 | |- ( z e. ( X X. RR+ ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. ) |
|
| 52 | 51 | ad2antll | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. ) |
| 53 | 52 | fveq2d | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( ball ` D ) ` z ) = ( ( ball ` D ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) |
| 54 | df-ov | |- ( ( 1st ` z ) ( ball ` D ) ( 2nd ` z ) ) = ( ( ball ` D ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) |
|
| 55 | 53 54 | eqtr4di | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( ball ` D ) ` z ) = ( ( 1st ` z ) ( ball ` D ) ( 2nd ` z ) ) ) |
| 56 | 8 | adantr | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> D e. ( *Met ` X ) ) |
| 57 | xp1st | |- ( z e. ( X X. RR+ ) -> ( 1st ` z ) e. X ) |
|
| 58 | 57 | ad2antll | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( 1st ` z ) e. X ) |
| 59 | xp2nd | |- ( z e. ( X X. RR+ ) -> ( 2nd ` z ) e. RR+ ) |
|
| 60 | 59 | ad2antll | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( 2nd ` z ) e. RR+ ) |
| 61 | bln0 | |- ( ( D e. ( *Met ` X ) /\ ( 1st ` z ) e. X /\ ( 2nd ` z ) e. RR+ ) -> ( ( 1st ` z ) ( ball ` D ) ( 2nd ` z ) ) =/= (/) ) |
|
| 62 | 56 58 60 61 | syl3anc | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( 1st ` z ) ( ball ` D ) ( 2nd ` z ) ) =/= (/) ) |
| 63 | 55 62 | eqnetrd | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( ball ` D ) ` z ) =/= (/) ) |
| 64 | 10 | adantr | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> J e. Top ) |
| 65 | ffvelrn | |- ( ( M : NN --> ( Clsd ` J ) /\ k e. NN ) -> ( M ` k ) e. ( Clsd ` J ) ) |
|
| 66 | 4 47 65 | syl2an | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( M ` k ) e. ( Clsd ` J ) ) |
| 67 | 12 | cldss | |- ( ( M ` k ) e. ( Clsd ` J ) -> ( M ` k ) C_ U. J ) |
| 68 | 66 67 | syl | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( M ` k ) C_ U. J ) |
| 69 | 60 | rpxrd | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( 2nd ` z ) e. RR* ) |
| 70 | 1 | blopn | |- ( ( D e. ( *Met ` X ) /\ ( 1st ` z ) e. X /\ ( 2nd ` z ) e. RR* ) -> ( ( 1st ` z ) ( ball ` D ) ( 2nd ` z ) ) e. J ) |
| 71 | 56 58 69 70 | syl3anc | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( 1st ` z ) ( ball ` D ) ( 2nd ` z ) ) e. J ) |
| 72 | 55 71 | eqeltrd | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( ball ` D ) ` z ) e. J ) |
| 73 | 12 | ssntr | |- ( ( ( J e. Top /\ ( M ` k ) C_ U. J ) /\ ( ( ( ball ` D ) ` z ) e. J /\ ( ( ball ` D ) ` z ) C_ ( M ` k ) ) ) -> ( ( ball ` D ) ` z ) C_ ( ( int ` J ) ` ( M ` k ) ) ) |
| 74 | 73 | expr | |- ( ( ( J e. Top /\ ( M ` k ) C_ U. J ) /\ ( ( ball ` D ) ` z ) e. J ) -> ( ( ( ball ` D ) ` z ) C_ ( M ` k ) -> ( ( ball ` D ) ` z ) C_ ( ( int ` J ) ` ( M ` k ) ) ) ) |
| 75 | 64 68 72 74 | syl21anc | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( ( ball ` D ) ` z ) C_ ( M ` k ) -> ( ( ball ` D ) ` z ) C_ ( ( int ` J ) ` ( M ` k ) ) ) ) |
| 76 | ssn0 | |- ( ( ( ( ball ` D ) ` z ) C_ ( ( int ` J ) ` ( M ` k ) ) /\ ( ( ball ` D ) ` z ) =/= (/) ) -> ( ( int ` J ) ` ( M ` k ) ) =/= (/) ) |
|
| 77 | 76 | expcom | |- ( ( ( ball ` D ) ` z ) =/= (/) -> ( ( ( ball ` D ) ` z ) C_ ( ( int ` J ) ` ( M ` k ) ) -> ( ( int ` J ) ` ( M ` k ) ) =/= (/) ) ) |
| 78 | 63 75 77 | sylsyld | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( ( ball ` D ) ` z ) C_ ( M ` k ) -> ( ( int ` J ) ` ( M ` k ) ) =/= (/) ) ) |
| 79 | 50 78 | syl5bir | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) = (/) -> ( ( int ` J ) ` ( M ` k ) ) =/= (/) ) ) |
| 80 | 79 | necon2d | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( ( int ` J ) ` ( M ` k ) ) = (/) -> ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) =/= (/) ) ) |
| 81 | 49 80 | mpd | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) =/= (/) ) |
| 82 | n0 | |- ( ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) =/= (/) <-> E. x x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) |
|
| 83 | 8 | 3ad2ant1 | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) /\ x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> D e. ( *Met ` X ) ) |
| 84 | 12 | difopn | |- ( ( ( ( ball ` D ) ` z ) e. J /\ ( M ` k ) e. ( Clsd ` J ) ) -> ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) e. J ) |
| 85 | 72 66 84 | syl2anc | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) e. J ) |
| 86 | 85 | 3adant3 | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) /\ x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) e. J ) |
| 87 | simp3 | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) /\ x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) |
|
| 88 | simp2l | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) /\ x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> k e. NN ) |
|
| 89 | nnrp | |- ( k e. NN -> k e. RR+ ) |
|
| 90 | 89 | rpreccld | |- ( k e. NN -> ( 1 / k ) e. RR+ ) |
| 91 | 88 90 | syl | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) /\ x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> ( 1 / k ) e. RR+ ) |
| 92 | 1 | mopni3 | |- ( ( ( D e. ( *Met ` X ) /\ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) e. J /\ x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) /\ ( 1 / k ) e. RR+ ) -> E. n e. RR+ ( n < ( 1 / k ) /\ ( x ( ball ` D ) n ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) |
| 93 | 83 86 87 91 92 | syl31anc | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) /\ x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> E. n e. RR+ ( n < ( 1 / k ) /\ ( x ( ball ` D ) n ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) |
| 94 | simp1 | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) /\ x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> ph ) |
|
| 95 | elssuni | |- ( ( ( ball ` D ) ` z ) e. J -> ( ( ball ` D ) ` z ) C_ U. J ) |
|
| 96 | 72 95 | syl | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( ball ` D ) ` z ) C_ U. J ) |
| 97 | 24 | adantr | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> X = U. J ) |
| 98 | 96 97 | sseqtrrd | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( ball ` D ) ` z ) C_ X ) |
| 99 | 98 | ssdifssd | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) C_ X ) |
| 100 | 99 | sseld | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) -> x e. X ) ) |
| 101 | 100 | 3impia | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) /\ x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> x e. X ) |
| 102 | simp2 | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) /\ x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> ( k e. NN /\ z e. ( X X. RR+ ) ) ) |
|
| 103 | rphalfcl | |- ( n e. RR+ -> ( n / 2 ) e. RR+ ) |
|
| 104 | rphalflt | |- ( n e. RR+ -> ( n / 2 ) < n ) |
|
| 105 | breq1 | |- ( r = ( n / 2 ) -> ( r < n <-> ( n / 2 ) < n ) ) |
|
| 106 | 105 | rspcev | |- ( ( ( n / 2 ) e. RR+ /\ ( n / 2 ) < n ) -> E. r e. RR+ r < n ) |
| 107 | 103 104 106 | syl2anc | |- ( n e. RR+ -> E. r e. RR+ r < n ) |
| 108 | 107 | ad2antlr | |- ( ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ n e. RR+ ) /\ ( n < ( 1 / k ) /\ ( x ( ball ` D ) n ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) -> E. r e. RR+ r < n ) |
| 109 | df-rex | |- ( E. r e. RR+ r < n <-> E. r ( r e. RR+ /\ r < n ) ) |
|
| 110 | simpr3 | |- ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ ( n e. RR+ /\ r < n /\ r e. RR+ ) ) -> r e. RR+ ) |
|
| 111 | 110 | rpred | |- ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ ( n e. RR+ /\ r < n /\ r e. RR+ ) ) -> r e. RR ) |
| 112 | simpr1 | |- ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ ( n e. RR+ /\ r < n /\ r e. RR+ ) ) -> n e. RR+ ) |
|
| 113 | 112 | rpred | |- ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ ( n e. RR+ /\ r < n /\ r e. RR+ ) ) -> n e. RR ) |
| 114 | simplrl | |- ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ ( n e. RR+ /\ r < n /\ r e. RR+ ) ) -> k e. NN ) |
|
| 115 | 114 | nnrecred | |- ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ ( n e. RR+ /\ r < n /\ r e. RR+ ) ) -> ( 1 / k ) e. RR ) |
| 116 | simpr2 | |- ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ ( n e. RR+ /\ r < n /\ r e. RR+ ) ) -> r < n ) |
|
| 117 | lttr | |- ( ( r e. RR /\ n e. RR /\ ( 1 / k ) e. RR ) -> ( ( r < n /\ n < ( 1 / k ) ) -> r < ( 1 / k ) ) ) |
|
| 118 | 117 | expdimp | |- ( ( ( r e. RR /\ n e. RR /\ ( 1 / k ) e. RR ) /\ r < n ) -> ( n < ( 1 / k ) -> r < ( 1 / k ) ) ) |
| 119 | 111 113 115 116 118 | syl31anc | |- ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ ( n e. RR+ /\ r < n /\ r e. RR+ ) ) -> ( n < ( 1 / k ) -> r < ( 1 / k ) ) ) |
| 120 | 8 | anim1i | |- ( ( ph /\ x e. X ) -> ( D e. ( *Met ` X ) /\ x e. X ) ) |
| 121 | 120 | adantr | |- ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( D e. ( *Met ` X ) /\ x e. X ) ) |
| 122 | rpxr | |- ( r e. RR+ -> r e. RR* ) |
|
| 123 | rpxr | |- ( n e. RR+ -> n e. RR* ) |
|
| 124 | id | |- ( r < n -> r < n ) |
|
| 125 | 122 123 124 | 3anim123i | |- ( ( r e. RR+ /\ n e. RR+ /\ r < n ) -> ( r e. RR* /\ n e. RR* /\ r < n ) ) |
| 126 | 125 | 3coml | |- ( ( n e. RR+ /\ r < n /\ r e. RR+ ) -> ( r e. RR* /\ n e. RR* /\ r < n ) ) |
| 127 | 1 | blsscls | |- ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( r e. RR* /\ n e. RR* /\ r < n ) ) -> ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( x ( ball ` D ) n ) ) |
| 128 | 121 126 127 | syl2an | |- ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ ( n e. RR+ /\ r < n /\ r e. RR+ ) ) -> ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( x ( ball ` D ) n ) ) |
| 129 | sstr2 | |- ( ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( x ( ball ` D ) n ) -> ( ( x ( ball ` D ) n ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) -> ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) |
|
| 130 | 128 129 | syl | |- ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ ( n e. RR+ /\ r < n /\ r e. RR+ ) ) -> ( ( x ( ball ` D ) n ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) -> ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) |
| 131 | 119 130 | anim12d | |- ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ ( n e. RR+ /\ r < n /\ r e. RR+ ) ) -> ( ( n < ( 1 / k ) /\ ( x ( ball ` D ) n ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) |
| 132 | simpllr | |- ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ ( n e. RR+ /\ r < n /\ r e. RR+ ) ) -> x e. X ) |
|
| 133 | 132 110 | jca | |- ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ ( n e. RR+ /\ r < n /\ r e. RR+ ) ) -> ( x e. X /\ r e. RR+ ) ) |
| 134 | 131 133 | jctild | |- ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ ( n e. RR+ /\ r < n /\ r e. RR+ ) ) -> ( ( n < ( 1 / k ) /\ ( x ( ball ` D ) n ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) ) |
| 135 | 134 | 3exp2 | |- ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( n e. RR+ -> ( r < n -> ( r e. RR+ -> ( ( n < ( 1 / k ) /\ ( x ( ball ` D ) n ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) ) ) ) ) |
| 136 | 135 | com35 | |- ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( n e. RR+ -> ( ( n < ( 1 / k ) /\ ( x ( ball ` D ) n ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> ( r e. RR+ -> ( r < n -> ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) ) ) ) ) |
| 137 | 136 | imp5d | |- ( ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ n e. RR+ ) /\ ( n < ( 1 / k ) /\ ( x ( ball ` D ) n ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) -> ( ( r e. RR+ /\ r < n ) -> ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) ) |
| 138 | 137 | eximdv | |- ( ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ n e. RR+ ) /\ ( n < ( 1 / k ) /\ ( x ( ball ` D ) n ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) -> ( E. r ( r e. RR+ /\ r < n ) -> E. r ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) ) |
| 139 | 109 138 | syl5bi | |- ( ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ n e. RR+ ) /\ ( n < ( 1 / k ) /\ ( x ( ball ` D ) n ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) -> ( E. r e. RR+ r < n -> E. r ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) ) |
| 140 | 108 139 | mpd | |- ( ( ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) /\ n e. RR+ ) /\ ( n < ( 1 / k ) /\ ( x ( ball ` D ) n ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) -> E. r ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) |
| 141 | 140 | rexlimdva2 | |- ( ( ( ph /\ x e. X ) /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( E. n e. RR+ ( n < ( 1 / k ) /\ ( x ( ball ` D ) n ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> E. r ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) ) |
| 142 | 94 101 102 141 | syl21anc | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) /\ x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> ( E. n e. RR+ ( n < ( 1 / k ) /\ ( x ( ball ` D ) n ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> E. r ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) ) |
| 143 | 93 142 | mpd | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) /\ x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) -> E. r ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) |
| 144 | 143 | 3expia | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) -> E. r ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) ) |
| 145 | 144 | eximdv | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( E. x x e. ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) -> E. x E. r ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) ) |
| 146 | 82 145 | syl5bi | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> ( ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) =/= (/) -> E. x E. r ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) ) |
| 147 | 81 146 | mpd | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> E. x E. r ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) |
| 148 | opabn0 | |- ( { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } =/= (/) <-> E. x E. r ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) ) |
|
| 149 | 147 148 | sylibr | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } =/= (/) ) |
| 150 | eldifsn | |- ( { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } e. ( ~P ( X X. RR+ ) \ { (/) } ) <-> ( { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } e. ~P ( X X. RR+ ) /\ { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } =/= (/) ) ) |
|
| 151 | 46 149 150 | sylanbrc | |- ( ( ph /\ ( k e. NN /\ z e. ( X X. RR+ ) ) ) -> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } e. ( ~P ( X X. RR+ ) \ { (/) } ) ) |
| 152 | 151 | ralrimivva | |- ( ph -> A. k e. NN A. z e. ( X X. RR+ ) { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } e. ( ~P ( X X. RR+ ) \ { (/) } ) ) |
| 153 | 3 | fmpo | |- ( A. k e. NN A. z e. ( X X. RR+ ) { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } e. ( ~P ( X X. RR+ ) \ { (/) } ) <-> F : ( NN X. ( X X. RR+ ) ) --> ( ~P ( X X. RR+ ) \ { (/) } ) ) |
| 154 | 152 153 | sylib | |- ( ph -> F : ( NN X. ( X X. RR+ ) ) --> ( ~P ( X X. RR+ ) \ { (/) } ) ) |
| 155 | 154 | 3ad2ant1 | |- ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) -> F : ( NN X. ( X X. RR+ ) ) --> ( ~P ( X X. RR+ ) \ { (/) } ) ) |
| 156 | 1z | |- 1 e. ZZ |
|
| 157 | nnuz | |- NN = ( ZZ>= ` 1 ) |
|
| 158 | 156 157 | axdc4uz | |- ( ( ( X X. RR+ ) e. _V /\ <. n , m >. e. ( X X. RR+ ) /\ F : ( NN X. ( X X. RR+ ) ) --> ( ~P ( X X. RR+ ) \ { (/) } ) ) -> E. g ( g : NN --> ( X X. RR+ ) /\ ( g ` 1 ) = <. n , m >. /\ A. n e. NN ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) ) ) |
| 159 | 33 41 155 158 | syl3anc | |- ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) -> E. g ( g : NN --> ( X X. RR+ ) /\ ( g ` 1 ) = <. n , m >. /\ A. n e. NN ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) ) ) |
| 160 | simpl1 | |- ( ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) /\ ( g : NN --> ( X X. RR+ ) /\ ( g ` 1 ) = <. n , m >. /\ A. n e. NN ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) ) ) -> ph ) |
|
| 161 | 160 2 | syl | |- ( ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) /\ ( g : NN --> ( X X. RR+ ) /\ ( g ` 1 ) = <. n , m >. /\ A. n e. NN ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) ) ) -> D e. ( CMet ` X ) ) |
| 162 | 160 4 | syl | |- ( ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) /\ ( g : NN --> ( X X. RR+ ) /\ ( g ` 1 ) = <. n , m >. /\ A. n e. NN ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) ) ) -> M : NN --> ( Clsd ` J ) ) |
| 163 | simpl3 | |- ( ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) /\ ( g : NN --> ( X X. RR+ ) /\ ( g ` 1 ) = <. n , m >. /\ A. n e. NN ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) ) ) -> m e. RR+ ) |
|
| 164 | 39 | adantr | |- ( ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) /\ ( g : NN --> ( X X. RR+ ) /\ ( g ` 1 ) = <. n , m >. /\ A. n e. NN ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) ) ) -> n e. X ) |
| 165 | simpr1 | |- ( ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) /\ ( g : NN --> ( X X. RR+ ) /\ ( g ` 1 ) = <. n , m >. /\ A. n e. NN ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) ) ) -> g : NN --> ( X X. RR+ ) ) |
|
| 166 | simpr2 | |- ( ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) /\ ( g : NN --> ( X X. RR+ ) /\ ( g ` 1 ) = <. n , m >. /\ A. n e. NN ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) ) ) -> ( g ` 1 ) = <. n , m >. ) |
|
| 167 | simpr3 | |- ( ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) /\ ( g : NN --> ( X X. RR+ ) /\ ( g ` 1 ) = <. n , m >. /\ A. n e. NN ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) ) ) -> A. n e. NN ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) ) |
|
| 168 | fvoveq1 | |- ( n = k -> ( g ` ( n + 1 ) ) = ( g ` ( k + 1 ) ) ) |
|
| 169 | id | |- ( n = k -> n = k ) |
|
| 170 | fveq2 | |- ( n = k -> ( g ` n ) = ( g ` k ) ) |
|
| 171 | 169 170 | oveq12d | |- ( n = k -> ( n F ( g ` n ) ) = ( k F ( g ` k ) ) ) |
| 172 | 168 171 | eleq12d | |- ( n = k -> ( ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) <-> ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) ) ) |
| 173 | 172 | cbvralvw | |- ( A. n e. NN ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) <-> A. k e. NN ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) ) |
| 174 | 167 173 | sylib | |- ( ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) /\ ( g : NN --> ( X X. RR+ ) /\ ( g ` 1 ) = <. n , m >. /\ A. n e. NN ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) ) ) -> A. k e. NN ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) ) |
| 175 | 1 161 3 162 163 164 165 166 174 | bcthlem4 | |- ( ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) /\ ( g : NN --> ( X X. RR+ ) /\ ( g ` 1 ) = <. n , m >. /\ A. n e. NN ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) ) ) -> ( ( n ( ball ` D ) m ) \ U. ran M ) =/= (/) ) |
| 176 | 159 175 | exlimddv | |- ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) -> ( ( n ( ball ` D ) m ) \ U. ran M ) =/= (/) ) |
| 177 | 12 | ntrss2 | |- ( ( J e. Top /\ U. ran M C_ U. J ) -> ( ( int ` J ) ` U. ran M ) C_ U. ran M ) |
| 178 | 10 16 177 | syl2anc | |- ( ph -> ( ( int ` J ) ` U. ran M ) C_ U. ran M ) |
| 179 | sstr2 | |- ( ( n ( ball ` D ) m ) C_ ( ( int ` J ) ` U. ran M ) -> ( ( ( int ` J ) ` U. ran M ) C_ U. ran M -> ( n ( ball ` D ) m ) C_ U. ran M ) ) |
|
| 180 | 178 179 | syl5com | |- ( ph -> ( ( n ( ball ` D ) m ) C_ ( ( int ` J ) ` U. ran M ) -> ( n ( ball ` D ) m ) C_ U. ran M ) ) |
| 181 | ssdif0 | |- ( ( n ( ball ` D ) m ) C_ U. ran M <-> ( ( n ( ball ` D ) m ) \ U. ran M ) = (/) ) |
|
| 182 | 180 181 | syl6ib | |- ( ph -> ( ( n ( ball ` D ) m ) C_ ( ( int ` J ) ` U. ran M ) -> ( ( n ( ball ` D ) m ) \ U. ran M ) = (/) ) ) |
| 183 | 182 | necon3ad | |- ( ph -> ( ( ( n ( ball ` D ) m ) \ U. ran M ) =/= (/) -> -. ( n ( ball ` D ) m ) C_ ( ( int ` J ) ` U. ran M ) ) ) |
| 184 | 183 | 3ad2ant1 | |- ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) -> ( ( ( n ( ball ` D ) m ) \ U. ran M ) =/= (/) -> -. ( n ( ball ` D ) m ) C_ ( ( int ` J ) ` U. ran M ) ) ) |
| 185 | 176 184 | mpd | |- ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) /\ m e. RR+ ) -> -. ( n ( ball ` D ) m ) C_ ( ( int ` J ) ` U. ran M ) ) |
| 186 | 185 | 3expa | |- ( ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) ) /\ m e. RR+ ) -> -. ( n ( ball ` D ) m ) C_ ( ( int ` J ) ` U. ran M ) ) |
| 187 | 186 | nrexdv | |- ( ( ph /\ n e. ( ( int ` J ) ` U. ran M ) ) -> -. E. m e. RR+ ( n ( ball ` D ) m ) C_ ( ( int ` J ) ` U. ran M ) ) |
| 188 | 22 187 | pm2.65da | |- ( ph -> -. n e. ( ( int ` J ) ` U. ran M ) ) |
| 189 | 188 | eq0rdv | |- ( ph -> ( ( int ` J ) ` U. ran M ) = (/) ) |