Metamath Proof Explorer

Theorem caublcls

Description: The convergent point of a sequence of nested balls is in the closures of any of the balls (i.e. it is in the intersection of the closures). Indeed, it is the only point in the intersection because a metric space is Hausdorff, but we don't prove this here. (Contributed by Mario Carneiro, 21-Jan-2014) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses caubl.2 
|- ( ph -> D e. ( *Met ` X ) )
caubl.3 
|- ( ph -> F : NN --> ( X X. RR+ ) )
caubl.4 
|- ( ph -> A. n e. NN ( ( ball ` D ) ` ( F ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) )
caublcls.6 
|- J = ( MetOpen ` D )
Assertion caublcls 
|- ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> P e. ( ( cls ` J ) ` ( ( ball ` D ) ` ( F ` A ) ) ) )

Proof

Step Hyp Ref Expression
1 caubl.2 
 |-  ( ph -> D e. ( *Met ` X ) )
2 caubl.3 
 |-  ( ph -> F : NN --> ( X X. RR+ ) )
3 caubl.4 
 |-  ( ph -> A. n e. NN ( ( ball ` D ) ` ( F ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) )
4 caublcls.6 
 |-  J = ( MetOpen ` D )
5 eqid 
 |-  ( ZZ>= ` A ) = ( ZZ>= ` A )
6 1 3ad2ant1 
 |-  ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> D e. ( *Met ` X ) )
7 4 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
8 6 7 syl 
 |-  ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> J e. ( TopOn ` X ) )
9 simp3 
 |-  ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> A e. NN )
10 9 nnzd 
 |-  ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> A e. ZZ )
11 simp2 
 |-  ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> ( 1st o. F ) ( ~~>t ` J ) P )
12 2fveq3 
 |-  ( r = A -> ( ( ball ` D ) ` ( F ` r ) ) = ( ( ball ` D ) ` ( F ` A ) ) )
13 12 sseq1d 
 |-  ( r = A -> ( ( ( ball ` D ) ` ( F ` r ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) <-> ( ( ball ` D ) ` ( F ` A ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) )
14 13 imbi2d 
 |-  ( r = A -> ( ( ( ph /\ A e. NN ) -> ( ( ball ` D ) ` ( F ` r ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) <-> ( ( ph /\ A e. NN ) -> ( ( ball ` D ) ` ( F ` A ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) ) )
15 2fveq3 
 |-  ( r = k -> ( ( ball ` D ) ` ( F ` r ) ) = ( ( ball ` D ) ` ( F ` k ) ) )
16 15 sseq1d 
 |-  ( r = k -> ( ( ( ball ` D ) ` ( F ` r ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) <-> ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) )
17 16 imbi2d 
 |-  ( r = k -> ( ( ( ph /\ A e. NN ) -> ( ( ball ` D ) ` ( F ` r ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) <-> ( ( ph /\ A e. NN ) -> ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) ) )
18 2fveq3 
 |-  ( r = ( k + 1 ) -> ( ( ball ` D ) ` ( F ` r ) ) = ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) )
19 18 sseq1d 
 |-  ( r = ( k + 1 ) -> ( ( ( ball ` D ) ` ( F ` r ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) <-> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) )
20 19 imbi2d 
 |-  ( r = ( k + 1 ) -> ( ( ( ph /\ A e. NN ) -> ( ( ball ` D ) ` ( F ` r ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) <-> ( ( ph /\ A e. NN ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) ) )
21 ssid 
 |-  ( ( ball ` D ) ` ( F ` A ) ) C_ ( ( ball ` D ) ` ( F ` A ) )
22 21 2a1i 
 |-  ( A e. ZZ -> ( ( ph /\ A e. NN ) -> ( ( ball ` D ) ` ( F ` A ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) )
23 eluznn 
 |-  ( ( A e. NN /\ k e. ( ZZ>= ` A ) ) -> k e. NN )
24 fvoveq1 
 |-  ( n = k -> ( F ` ( n + 1 ) ) = ( F ` ( k + 1 ) ) )
25 24 fveq2d 
 |-  ( n = k -> ( ( ball ` D ) ` ( F ` ( n + 1 ) ) ) = ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) )
26 2fveq3 
 |-  ( n = k -> ( ( ball ` D ) ` ( F ` n ) ) = ( ( ball ` D ) ` ( F ` k ) ) )
27 25 26 sseq12d 
 |-  ( n = k -> ( ( ( ball ` D ) ` ( F ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) <-> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` k ) ) ) )
28 27 rspccva 
 |-  ( ( A. n e. NN ( ( ball ` D ) ` ( F ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) /\ k e. NN ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` k ) ) )
29 3 23 28 syl2an 
 |-  ( ( ph /\ ( A e. NN /\ k e. ( ZZ>= ` A ) ) ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` k ) ) )
30 29 anassrs 
 |-  ( ( ( ph /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` k ) ) )
31 sstr2 
 |-  ( ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` k ) ) -> ( ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) )
32 30 31 syl 
 |-  ( ( ( ph /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) )
33 32 expcom 
 |-  ( k e. ( ZZ>= ` A ) -> ( ( ph /\ A e. NN ) -> ( ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) ) )
34 33 a2d 
 |-  ( k e. ( ZZ>= ` A ) -> ( ( ( ph /\ A e. NN ) -> ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) -> ( ( ph /\ A e. NN ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) ) )
35 14 17 20 17 22 34 uzind4 
 |-  ( k e. ( ZZ>= ` A ) -> ( ( ph /\ A e. NN ) -> ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) ) )
36 35 impcom 
 |-  ( ( ( ph /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) )
37 36 3adantl2 
 |-  ( ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` A ) ) )
38 6 adantr 
 |-  ( ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> D e. ( *Met ` X ) )
39 simpl1 
 |-  ( ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ph )
40 39 2 syl 
 |-  ( ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> F : NN --> ( X X. RR+ ) )
41 23 3ad2antl3 
 |-  ( ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> k e. NN )
42 40 41 ffvelcdmd 
 |-  ( ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( F ` k ) e. ( X X. RR+ ) )
43 xp1st 
 |-  ( ( F ` k ) e. ( X X. RR+ ) -> ( 1st ` ( F ` k ) ) e. X )
44 42 43 syl 
 |-  ( ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( 1st ` ( F ` k ) ) e. X )
45 xp2nd 
 |-  ( ( F ` k ) e. ( X X. RR+ ) -> ( 2nd ` ( F ` k ) ) e. RR+ )
46 42 45 syl 
 |-  ( ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( 2nd ` ( F ` k ) ) e. RR+ )
47 blcntr 
 |-  ( ( D e. ( *Met ` X ) /\ ( 1st ` ( F ` k ) ) e. X /\ ( 2nd ` ( F ` k ) ) e. RR+ ) -> ( 1st ` ( F ` k ) ) e. ( ( 1st ` ( F ` k ) ) ( ball ` D ) ( 2nd ` ( F ` k ) ) ) )
48 38 44 46 47 syl3anc 
 |-  ( ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( 1st ` ( F ` k ) ) e. ( ( 1st ` ( F ` k ) ) ( ball ` D ) ( 2nd ` ( F ` k ) ) ) )
49 fvco3 
 |-  ( ( F : NN --> ( X X. RR+ ) /\ k e. NN ) -> ( ( 1st o. F ) ` k ) = ( 1st ` ( F ` k ) ) )
50 40 41 49 syl2anc 
 |-  ( ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( ( 1st o. F ) ` k ) = ( 1st ` ( F ` k ) ) )
51 1st2nd2 
 |-  ( ( F ` k ) e. ( X X. RR+ ) -> ( F ` k ) = <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. )
52 42 51 syl 
 |-  ( ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( F ` k ) = <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. )
53 52 fveq2d 
 |-  ( ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( ( ball ` D ) ` ( F ` k ) ) = ( ( ball ` D ) ` <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. ) )
54 df-ov 
 |-  ( ( 1st ` ( F ` k ) ) ( ball ` D ) ( 2nd ` ( F ` k ) ) ) = ( ( ball ` D ) ` <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. )
55 53 54 eqtr4di 
 |-  ( ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( ( ball ` D ) ` ( F ` k ) ) = ( ( 1st ` ( F ` k ) ) ( ball ` D ) ( 2nd ` ( F ` k ) ) ) )
56 48 50 55 3eltr4d 
 |-  ( ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( ( 1st o. F ) ` k ) e. ( ( ball ` D ) ` ( F ` k ) ) )
57 37 56 sseldd 
 |-  ( ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( ( 1st o. F ) ` k ) e. ( ( ball ` D ) ` ( F ` A ) ) )
58 2 ffvelcdmda 
 |-  ( ( ph /\ A e. NN ) -> ( F ` A ) e. ( X X. RR+ ) )
59 58 3adant2 
 |-  ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> ( F ` A ) e. ( X X. RR+ ) )
60 1st2nd2 
 |-  ( ( F ` A ) e. ( X X. RR+ ) -> ( F ` A ) = <. ( 1st ` ( F ` A ) ) , ( 2nd ` ( F ` A ) ) >. )
61 59 60 syl 
 |-  ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> ( F ` A ) = <. ( 1st ` ( F ` A ) ) , ( 2nd ` ( F ` A ) ) >. )
62 61 fveq2d 
 |-  ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> ( ( ball ` D ) ` ( F ` A ) ) = ( ( ball ` D ) ` <. ( 1st ` ( F ` A ) ) , ( 2nd ` ( F ` A ) ) >. ) )
63 df-ov 
 |-  ( ( 1st ` ( F ` A ) ) ( ball ` D ) ( 2nd ` ( F ` A ) ) ) = ( ( ball ` D ) ` <. ( 1st ` ( F ` A ) ) , ( 2nd ` ( F ` A ) ) >. )
64 62 63 eqtr4di 
 |-  ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> ( ( ball ` D ) ` ( F ` A ) ) = ( ( 1st ` ( F ` A ) ) ( ball ` D ) ( 2nd ` ( F ` A ) ) ) )
65 xp1st 
 |-  ( ( F ` A ) e. ( X X. RR+ ) -> ( 1st ` ( F ` A ) ) e. X )
66 59 65 syl 
 |-  ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> ( 1st ` ( F ` A ) ) e. X )
67 xp2nd 
 |-  ( ( F ` A ) e. ( X X. RR+ ) -> ( 2nd ` ( F ` A ) ) e. RR+ )
68 59 67 syl 
 |-  ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> ( 2nd ` ( F ` A ) ) e. RR+ )
69 68 rpxrd 
 |-  ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> ( 2nd ` ( F ` A ) ) e. RR* )
70 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ ( 1st ` ( F ` A ) ) e. X /\ ( 2nd ` ( F ` A ) ) e. RR* ) -> ( ( 1st ` ( F ` A ) ) ( ball ` D ) ( 2nd ` ( F ` A ) ) ) C_ X )
71 6 66 69 70 syl3anc 
 |-  ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> ( ( 1st ` ( F ` A ) ) ( ball ` D ) ( 2nd ` ( F ` A ) ) ) C_ X )
72 64 71 eqsstrd 
 |-  ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> ( ( ball ` D ) ` ( F ` A ) ) C_ X )
73 5 8 10 11 57 72 lmcls 
 |-  ( ( ph /\ ( 1st o. F ) ( ~~>t ` J ) P /\ A e. NN ) -> P e. ( ( cls ` J ) ` ( ( ball ` D ) ` ( F ` A ) ) ) )