Metamath Proof Explorer

Theorem bcthlem2

Description: Lemma for bcth . The balls in the sequence form an inclusion chain. (Contributed by Mario Carneiro, 7-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 ) )
bcthlem.7 
|- ( ph -> R e. RR+ )
bcthlem.8 
|- ( ph -> C e. X )
bcthlem.9 
|- ( ph -> g : NN --> ( X X. RR+ ) )
bcthlem.10 
|- ( ph -> ( g ` 1 ) = <. C , R >. )
bcthlem.11 
|- ( ph -> A. k e. NN ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) )
Assertion bcthlem2 
|- ( ph -> A. n e. NN ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( g ` n ) ) )

Proof

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 bcthlem.7 
 |-  ( ph -> R e. RR+ )
6 bcthlem.8 
 |-  ( ph -> C e. X )
7 bcthlem.9 
 |-  ( ph -> g : NN --> ( X X. RR+ ) )
8 bcthlem.10 
 |-  ( ph -> ( g ` 1 ) = <. C , R >. )
9 bcthlem.11 
 |-  ( ph -> A. k e. NN ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) )
10 fvoveq1 
 |-  ( k = n -> ( g ` ( k + 1 ) ) = ( g ` ( n + 1 ) ) )
11 id 
 |-  ( k = n -> k = n )
12 fveq2 
 |-  ( k = n -> ( g ` k ) = ( g ` n ) )
13 11 12 oveq12d 
 |-  ( k = n -> ( k F ( g ` k ) ) = ( n F ( g ` n ) ) )
14 10 13 eleq12d 
 |-  ( k = n -> ( ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) <-> ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) ) )
15 14 rspccva 
 |-  ( ( A. k e. NN ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) /\ n e. NN ) -> ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) )
16 9 15 sylan 
 |-  ( ( ph /\ n e. NN ) -> ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) )
17 7 ffvelrnda 
 |-  ( ( ph /\ n e. NN ) -> ( g ` n ) e. ( X X. RR+ ) )
18 1 2 3 bcthlem1 
 |-  ( ( ph /\ ( n e. NN /\ ( g ` n ) e. ( X X. RR+ ) ) ) -> ( ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) <-> ( ( g ` ( n + 1 ) ) e. ( X X. RR+ ) /\ ( 2nd ` ( g ` ( n + 1 ) ) ) < ( 1 / n ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` n ) ) \ ( M ` n ) ) ) ) )
19 18 expr 
 |-  ( ( ph /\ n e. NN ) -> ( ( g ` n ) e. ( X X. RR+ ) -> ( ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) <-> ( ( g ` ( n + 1 ) ) e. ( X X. RR+ ) /\ ( 2nd ` ( g ` ( n + 1 ) ) ) < ( 1 / n ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` n ) ) \ ( M ` n ) ) ) ) ) )
20 17 19 mpd 
 |-  ( ( ph /\ n e. NN ) -> ( ( g ` ( n + 1 ) ) e. ( n F ( g ` n ) ) <-> ( ( g ` ( n + 1 ) ) e. ( X X. RR+ ) /\ ( 2nd ` ( g ` ( n + 1 ) ) ) < ( 1 / n ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` n ) ) \ ( M ` n ) ) ) ) )
21 16 20 mpbid 
 |-  ( ( ph /\ n e. NN ) -> ( ( g ` ( n + 1 ) ) e. ( X X. RR+ ) /\ ( 2nd ` ( g ` ( n + 1 ) ) ) < ( 1 / n ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` n ) ) \ ( M ` n ) ) ) )
22 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
23 2 22 syl 
 |-  ( ph -> D e. ( Met ` X ) )
24 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
25 23 24 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
26 1 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
27 25 26 syl 
 |-  ( ph -> J e. Top )
28 xp1st 
 |-  ( ( g ` ( n + 1 ) ) e. ( X X. RR+ ) -> ( 1st ` ( g ` ( n + 1 ) ) ) e. X )
29 xp2nd 
 |-  ( ( g ` ( n + 1 ) ) e. ( X X. RR+ ) -> ( 2nd ` ( g ` ( n + 1 ) ) ) e. RR+ )
30 29 rpxrd 
 |-  ( ( g ` ( n + 1 ) ) e. ( X X. RR+ ) -> ( 2nd ` ( g ` ( n + 1 ) ) ) e. RR* )
31 28 30 jca 
 |-  ( ( g ` ( n + 1 ) ) e. ( X X. RR+ ) -> ( ( 1st ` ( g ` ( n + 1 ) ) ) e. X /\ ( 2nd ` ( g ` ( n + 1 ) ) ) e. RR* ) )
32 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ ( 1st ` ( g ` ( n + 1 ) ) ) e. X /\ ( 2nd ` ( g ` ( n + 1 ) ) ) e. RR* ) -> ( ( 1st ` ( g ` ( n + 1 ) ) ) ( ball ` D ) ( 2nd ` ( g ` ( n + 1 ) ) ) ) C_ X )
33 32 3expb 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( 1st ` ( g ` ( n + 1 ) ) ) e. X /\ ( 2nd ` ( g ` ( n + 1 ) ) ) e. RR* ) ) -> ( ( 1st ` ( g ` ( n + 1 ) ) ) ( ball ` D ) ( 2nd ` ( g ` ( n + 1 ) ) ) ) C_ X )
34 25 31 33 syl2an 
 |-  ( ( ph /\ ( g ` ( n + 1 ) ) e. ( X X. RR+ ) ) -> ( ( 1st ` ( g ` ( n + 1 ) ) ) ( ball ` D ) ( 2nd ` ( g ` ( n + 1 ) ) ) ) C_ X )
35 df-ov 
 |-  ( ( 1st ` ( g ` ( n + 1 ) ) ) ( ball ` D ) ( 2nd ` ( g ` ( n + 1 ) ) ) ) = ( ( ball ` D ) ` <. ( 1st ` ( g ` ( n + 1 ) ) ) , ( 2nd ` ( g ` ( n + 1 ) ) ) >. )
36 1st2nd2 
 |-  ( ( g ` ( n + 1 ) ) e. ( X X. RR+ ) -> ( g ` ( n + 1 ) ) = <. ( 1st ` ( g ` ( n + 1 ) ) ) , ( 2nd ` ( g ` ( n + 1 ) ) ) >. )
37 36 fveq2d 
 |-  ( ( g ` ( n + 1 ) ) e. ( X X. RR+ ) -> ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) = ( ( ball ` D ) ` <. ( 1st ` ( g ` ( n + 1 ) ) ) , ( 2nd ` ( g ` ( n + 1 ) ) ) >. ) )
38 35 37 eqtr4id 
 |-  ( ( g ` ( n + 1 ) ) e. ( X X. RR+ ) -> ( ( 1st ` ( g ` ( n + 1 ) ) ) ( ball ` D ) ( 2nd ` ( g ` ( n + 1 ) ) ) ) = ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) )
39 38 adantl 
 |-  ( ( ph /\ ( g ` ( n + 1 ) ) e. ( X X. RR+ ) ) -> ( ( 1st ` ( g ` ( n + 1 ) ) ) ( ball ` D ) ( 2nd ` ( g ` ( n + 1 ) ) ) ) = ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) )
40 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
41 25 40 syl 
 |-  ( ph -> X = U. J )
42 41 adantr 
 |-  ( ( ph /\ ( g ` ( n + 1 ) ) e. ( X X. RR+ ) ) -> X = U. J )
43 34 39 42 3sstr3d 
 |-  ( ( ph /\ ( g ` ( n + 1 ) ) e. ( X X. RR+ ) ) -> ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ U. J )
44 eqid 
 |-  U. J = U. J
45 44 sscls 
 |-  ( ( J e. Top /\ ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ U. J ) -> ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) ) )
46 27 43 45 syl2an2r 
 |-  ( ( ph /\ ( g ` ( n + 1 ) ) e. ( X X. RR+ ) ) -> ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) ) )
47 difss2 
 |-  ( ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` n ) ) \ ( M ` n ) ) -> ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) ) C_ ( ( ball ` D ) ` ( g ` n ) ) )
48 sstr2 
 |-  ( ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) ) -> ( ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) ) C_ ( ( ball ` D ) ` ( g ` n ) ) -> ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( g ` n ) ) ) )
49 46 47 48 syl2im 
 |-  ( ( ph /\ ( g ` ( n + 1 ) ) e. ( X X. RR+ ) ) -> ( ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` n ) ) \ ( M ` n ) ) -> ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( g ` n ) ) ) )
50 49 a1d 
 |-  ( ( ph /\ ( g ` ( n + 1 ) ) e. ( X X. RR+ ) ) -> ( ( 2nd ` ( g ` ( n + 1 ) ) ) < ( 1 / n ) -> ( ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` n ) ) \ ( M ` n ) ) -> ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( g ` n ) ) ) ) )
51 50 ex 
 |-  ( ph -> ( ( g ` ( n + 1 ) ) e. ( X X. RR+ ) -> ( ( 2nd ` ( g ` ( n + 1 ) ) ) < ( 1 / n ) -> ( ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` n ) ) \ ( M ` n ) ) -> ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( g ` n ) ) ) ) ) )
52 51 3impd 
 |-  ( ph -> ( ( ( g ` ( n + 1 ) ) e. ( X X. RR+ ) /\ ( 2nd ` ( g ` ( n + 1 ) ) ) < ( 1 / n ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` n ) ) \ ( M ` n ) ) ) -> ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( g ` n ) ) ) )
53 52 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( g ` ( n + 1 ) ) e. ( X X. RR+ ) /\ ( 2nd ` ( g ` ( n + 1 ) ) ) < ( 1 / n ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) ) C_ ( ( ( ball ` D ) ` ( g ` n ) ) \ ( M ` n ) ) ) -> ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( g ` n ) ) ) )
54 21 53 mpd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( g ` n ) ) )
55 54 ralrimiva 
 |-  ( ph -> A. n e. NN ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( g ` n ) ) )