This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscmet3lem2

Description: Lemma for iscmet3 . (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses iscmet3.1 
|- Z = ( ZZ>= ` M )
iscmet3.2 
|- J = ( MetOpen ` D )
iscmet3.3 
|- ( ph -> M e. ZZ )
iscmet3.4 
|- ( ph -> D e. ( Met ` X ) )
iscmet3.6 
|- ( ph -> F : Z --> X )
iscmet3.9 
|- ( ph -> A. k e. ZZ A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) )
iscmet3.10 
|- ( ph -> A. k e. Z A. n e. ( M ... k ) ( F ` k ) e. ( S ` n ) )
iscmet3.7 
|- ( ph -> G e. ( Fil ` X ) )
iscmet3.8 
|- ( ph -> S : ZZ --> G )
iscmet3.5 
|- ( ph -> F e. dom ( ~~>t ` J ) )
Assertion iscmet3lem2 
|- ( ph -> ( J fLim G ) =/= (/) )

Proof

Step Hyp Ref Expression
1 iscmet3.1 
 |-  Z = ( ZZ>= ` M )
2 iscmet3.2 
 |-  J = ( MetOpen ` D )
3 iscmet3.3 
 |-  ( ph -> M e. ZZ )
4 iscmet3.4 
 |-  ( ph -> D e. ( Met ` X ) )
5 iscmet3.6 
 |-  ( ph -> F : Z --> X )
6 iscmet3.9 
 |-  ( ph -> A. k e. ZZ A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) )
7 iscmet3.10 
 |-  ( ph -> A. k e. Z A. n e. ( M ... k ) ( F ` k ) e. ( S ` n ) )
8 iscmet3.7 
 |-  ( ph -> G e. ( Fil ` X ) )
9 iscmet3.8 
 |-  ( ph -> S : ZZ --> G )
10 iscmet3.5 
 |-  ( ph -> F e. dom ( ~~>t ` J ) )
11 eldmg 
 |-  ( F e. dom ( ~~>t ` J ) -> ( F e. dom ( ~~>t ` J ) <-> E. x F ( ~~>t ` J ) x ) )
12 11 ibi 
 |-  ( F e. dom ( ~~>t ` J ) -> E. x F ( ~~>t ` J ) x )
13 10 12 syl 
 |-  ( ph -> E. x F ( ~~>t ` J ) x )
14 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
15 4 14 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
16 2 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
17 15 16 syl 
 |-  ( ph -> J e. ( TopOn ` X ) )
18 lmcl 
 |-  ( ( J e. ( TopOn ` X ) /\ F ( ~~>t ` J ) x ) -> x e. X )
19 17 18 sylan 
 |-  ( ( ph /\ F ( ~~>t ` J ) x ) -> x e. X )
20 15 adantr 
 |-  ( ( ph /\ F ( ~~>t ` J ) x ) -> D e. ( *Met ` X ) )
21 2 mopni2 
 |-  ( ( D e. ( *Met ` X ) /\ y e. J /\ x e. y ) -> E. r e. RR+ ( x ( ball ` D ) r ) C_ y )
22 21 3expia 
 |-  ( ( D e. ( *Met ` X ) /\ y e. J ) -> ( x e. y -> E. r e. RR+ ( x ( ball ` D ) r ) C_ y ) )
23 20 22 sylan 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ y e. J ) -> ( x e. y -> E. r e. RR+ ( x ( ball ` D ) r ) C_ y ) )
24 8 ad3antrrr 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ y e. J ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ y ) ) -> G e. ( Fil ` X ) )
25 3 ad2antrr 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> M e. ZZ )
26 rphalfcl 
 |-  ( r e. RR+ -> ( r / 2 ) e. RR+ )
27 26 adantl 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> ( r / 2 ) e. RR+ )
28 1 iscmet3lem3 
 |-  ( ( M e. ZZ /\ ( r / 2 ) e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( 1 / 2 ) ^ k ) < ( r / 2 ) )
29 25 27 28 syl2anc 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( 1 / 2 ) ^ k ) < ( r / 2 ) )
30 20 adantr 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> D e. ( *Met ` X ) )
31 19 adantr 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> x e. X )
32 blcntr 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ ( r / 2 ) e. RR+ ) -> x e. ( x ( ball ` D ) ( r / 2 ) ) )
33 30 31 27 32 syl3anc 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> x e. ( x ( ball ` D ) ( r / 2 ) ) )
34 simplr 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> F ( ~~>t ` J ) x )
35 27 rpxrd 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> ( r / 2 ) e. RR* )
36 2 blopn 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ ( r / 2 ) e. RR* ) -> ( x ( ball ` D ) ( r / 2 ) ) e. J )
37 30 31 35 36 syl3anc 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> ( x ( ball ` D ) ( r / 2 ) ) e. J )
38 1 33 25 34 37 lmcvg 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) )
39 1 rexanuz2 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) <-> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) )
40 1 r19.2uz 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) -> E. k e. Z ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) )
41 8 ad3antrrr 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ ( k e. Z /\ ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) ) ) -> G e. ( Fil ` X ) )
42 9 ad3antrrr 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ ( k e. Z /\ ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) ) ) -> S : ZZ --> G )
43 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
44 43 1 eleq2s 
 |-  ( k e. Z -> k e. ZZ )
45 44 ad2antrl 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ ( k e. Z /\ ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) ) ) -> k e. ZZ )
46 ffvelcdm 
 |-  ( ( S : ZZ --> G /\ k e. ZZ ) -> ( S ` k ) e. G )
47 42 45 46 syl2anc 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ ( k e. Z /\ ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) ) ) -> ( S ` k ) e. G )
48 rpxr 
 |-  ( r e. RR+ -> r e. RR* )
49 48 adantl 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> r e. RR* )
50 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ r e. RR* ) -> ( x ( ball ` D ) r ) C_ X )
51 30 31 49 50 syl3anc 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> ( x ( ball ` D ) r ) C_ X )
52 51 adantr 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ ( k e. Z /\ ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) ) ) -> ( x ( ball ` D ) r ) C_ X )
53 44 adantl 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> k e. ZZ )
54 1rp 
 |-  1 e. RR+
55 rphalfcl 
 |-  ( 1 e. RR+ -> ( 1 / 2 ) e. RR+ )
56 54 55 ax-mp 
 |-  ( 1 / 2 ) e. RR+
57 rpexpcl 
 |-  ( ( ( 1 / 2 ) e. RR+ /\ k e. ZZ ) -> ( ( 1 / 2 ) ^ k ) e. RR+ )
58 56 57 mpan 
 |-  ( k e. ZZ -> ( ( 1 / 2 ) ^ k ) e. RR+ )
59 53 58 syl 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( ( 1 / 2 ) ^ k ) e. RR+ )
60 59 rpred 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( ( 1 / 2 ) ^ k ) e. RR )
61 27 adantr 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( r / 2 ) e. RR+ )
62 61 rpred 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( r / 2 ) e. RR )
63 ltle 
 |-  ( ( ( ( 1 / 2 ) ^ k ) e. RR /\ ( r / 2 ) e. RR ) -> ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) -> ( ( 1 / 2 ) ^ k ) <_ ( r / 2 ) ) )
64 60 62 63 syl2anc 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) -> ( ( 1 / 2 ) ^ k ) <_ ( r / 2 ) ) )
65 fveq2 
 |-  ( n = k -> ( S ` n ) = ( S ` k ) )
66 65 eleq2d 
 |-  ( n = k -> ( ( F ` k ) e. ( S ` n ) <-> ( F ` k ) e. ( S ` k ) ) )
67 7 r19.21bi 
 |-  ( ( ph /\ k e. Z ) -> A. n e. ( M ... k ) ( F ` k ) e. ( S ` n ) )
68 eluzfz2 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ( M ... k ) )
69 68 1 eleq2s 
 |-  ( k e. Z -> k e. ( M ... k ) )
70 69 adantl 
 |-  ( ( ph /\ k e. Z ) -> k e. ( M ... k ) )
71 66 67 70 rspcdva 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. ( S ` k ) )
72 71 adantr 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( S ` k ) ) -> ( F ` k ) e. ( S ` k ) )
73 simpr 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( S ` k ) ) -> y e. ( S ` k ) )
74 6 ad2antrr 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( S ` k ) ) -> A. k e. ZZ A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) )
75 44 ad2antlr 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( S ` k ) ) -> k e. ZZ )
76 rsp 
 |-  ( A. k e. ZZ A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) -> ( k e. ZZ -> A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) )
77 74 75 76 sylc 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( S ` k ) ) -> A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) )
78 oveq1 
 |-  ( u = ( F ` k ) -> ( u D v ) = ( ( F ` k ) D v ) )
79 78 breq1d 
 |-  ( u = ( F ` k ) -> ( ( u D v ) < ( ( 1 / 2 ) ^ k ) <-> ( ( F ` k ) D v ) < ( ( 1 / 2 ) ^ k ) ) )
80 oveq2 
 |-  ( v = y -> ( ( F ` k ) D v ) = ( ( F ` k ) D y ) )
81 80 breq1d 
 |-  ( v = y -> ( ( ( F ` k ) D v ) < ( ( 1 / 2 ) ^ k ) <-> ( ( F ` k ) D y ) < ( ( 1 / 2 ) ^ k ) ) )
82 79 81 rspc2va 
 |-  ( ( ( ( F ` k ) e. ( S ` k ) /\ y e. ( S ` k ) ) /\ A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) ) -> ( ( F ` k ) D y ) < ( ( 1 / 2 ) ^ k ) )
83 72 73 77 82 syl21anc 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( S ` k ) ) -> ( ( F ` k ) D y ) < ( ( 1 / 2 ) ^ k ) )
84 15 ad2antrr 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( S ` k ) ) -> D e. ( *Met ` X ) )
85 44 58 syl 
 |-  ( k e. Z -> ( ( 1 / 2 ) ^ k ) e. RR+ )
86 85 rpxrd 
 |-  ( k e. Z -> ( ( 1 / 2 ) ^ k ) e. RR* )
87 86 ad2antlr 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( S ` k ) ) -> ( ( 1 / 2 ) ^ k ) e. RR* )
88 5 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. X )
89 88 adantr 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( S ` k ) ) -> ( F ` k ) e. X )
90 8 adantr 
 |-  ( ( ph /\ k e. Z ) -> G e. ( Fil ` X ) )
91 9 44 46 syl2an 
 |-  ( ( ph /\ k e. Z ) -> ( S ` k ) e. G )
92 filelss 
 |-  ( ( G e. ( Fil ` X ) /\ ( S ` k ) e. G ) -> ( S ` k ) C_ X )
93 90 91 92 syl2anc 
 |-  ( ( ph /\ k e. Z ) -> ( S ` k ) C_ X )
94 93 sselda 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( S ` k ) ) -> y e. X )
95 elbl2 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( ( 1 / 2 ) ^ k ) e. RR* ) /\ ( ( F ` k ) e. X /\ y e. X ) ) -> ( y e. ( ( F ` k ) ( ball ` D ) ( ( 1 / 2 ) ^ k ) ) <-> ( ( F ` k ) D y ) < ( ( 1 / 2 ) ^ k ) ) )
96 84 87 89 94 95 syl22anc 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( S ` k ) ) -> ( y e. ( ( F ` k ) ( ball ` D ) ( ( 1 / 2 ) ^ k ) ) <-> ( ( F ` k ) D y ) < ( ( 1 / 2 ) ^ k ) ) )
97 83 96 mpbird 
 |-  ( ( ( ph /\ k e. Z ) /\ y e. ( S ` k ) ) -> y e. ( ( F ` k ) ( ball ` D ) ( ( 1 / 2 ) ^ k ) ) )
98 97 ex 
 |-  ( ( ph /\ k e. Z ) -> ( y e. ( S ` k ) -> y e. ( ( F ` k ) ( ball ` D ) ( ( 1 / 2 ) ^ k ) ) ) )
99 98 ssrdv 
 |-  ( ( ph /\ k e. Z ) -> ( S ` k ) C_ ( ( F ` k ) ( ball ` D ) ( ( 1 / 2 ) ^ k ) ) )
100 99 ad4ant14 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( S ` k ) C_ ( ( F ` k ) ( ball ` D ) ( ( 1 / 2 ) ^ k ) ) )
101 30 adantr 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> D e. ( *Met ` X ) )
102 5 ad2antrr 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> F : Z --> X )
103 102 ffvelcdmda 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( F ` k ) e. X )
104 59 rpxrd 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( ( 1 / 2 ) ^ k ) e. RR* )
105 35 adantr 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( r / 2 ) e. RR* )
106 ssbl 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( F ` k ) e. X ) /\ ( ( ( 1 / 2 ) ^ k ) e. RR* /\ ( r / 2 ) e. RR* ) /\ ( ( 1 / 2 ) ^ k ) <_ ( r / 2 ) ) -> ( ( F ` k ) ( ball ` D ) ( ( 1 / 2 ) ^ k ) ) C_ ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) )
107 106 3expia 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( F ` k ) e. X ) /\ ( ( ( 1 / 2 ) ^ k ) e. RR* /\ ( r / 2 ) e. RR* ) ) -> ( ( ( 1 / 2 ) ^ k ) <_ ( r / 2 ) -> ( ( F ` k ) ( ball ` D ) ( ( 1 / 2 ) ^ k ) ) C_ ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) ) )
108 101 103 104 105 107 syl22anc 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( ( ( 1 / 2 ) ^ k ) <_ ( r / 2 ) -> ( ( F ` k ) ( ball ` D ) ( ( 1 / 2 ) ^ k ) ) C_ ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) ) )
109 sstr 
 |-  ( ( ( S ` k ) C_ ( ( F ` k ) ( ball ` D ) ( ( 1 / 2 ) ^ k ) ) /\ ( ( F ` k ) ( ball ` D ) ( ( 1 / 2 ) ^ k ) ) C_ ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) ) -> ( S ` k ) C_ ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) )
110 100 108 109 syl6an 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( ( ( 1 / 2 ) ^ k ) <_ ( r / 2 ) -> ( S ` k ) C_ ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) ) )
111 64 110 syld 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) -> ( S ` k ) C_ ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) ) )
112 111 adantrd 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) -> ( S ` k ) C_ ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) ) )
113 112 impr 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ ( k e. Z /\ ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) ) ) -> ( S ` k ) C_ ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) )
114 31 adantr 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> x e. X )
115 blcom 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( r / 2 ) e. RR* ) /\ ( x e. X /\ ( F ` k ) e. X ) ) -> ( ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) <-> x e. ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) ) )
116 101 105 114 103 115 syl22anc 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) <-> x e. ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) ) )
117 rpre 
 |-  ( r e. RR+ -> r e. RR )
118 117 ad2antlr 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> r e. RR )
119 blhalf 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( F ` k ) e. X ) /\ ( r e. RR /\ x e. ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) ) ) -> ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) C_ ( x ( ball ` D ) r ) )
120 119 expr 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( F ` k ) e. X ) /\ r e. RR ) -> ( x e. ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) -> ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) C_ ( x ( ball ` D ) r ) ) )
121 101 103 118 120 syl21anc 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( x e. ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) -> ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) C_ ( x ( ball ` D ) r ) ) )
122 116 121 sylbid 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) -> ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) C_ ( x ( ball ` D ) r ) ) )
123 122 adantld 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ k e. Z ) -> ( ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) -> ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) C_ ( x ( ball ` D ) r ) ) )
124 123 impr 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ ( k e. Z /\ ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) ) ) -> ( ( F ` k ) ( ball ` D ) ( r / 2 ) ) C_ ( x ( ball ` D ) r ) )
125 113 124 sstrd 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ ( k e. Z /\ ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) ) ) -> ( S ` k ) C_ ( x ( ball ` D ) r ) )
126 filss 
 |-  ( ( G e. ( Fil ` X ) /\ ( ( S ` k ) e. G /\ ( x ( ball ` D ) r ) C_ X /\ ( S ` k ) C_ ( x ( ball ` D ) r ) ) ) -> ( x ( ball ` D ) r ) e. G )
127 41 47 52 125 126 syl13anc 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) /\ ( k e. Z /\ ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) ) ) -> ( x ( ball ` D ) r ) e. G )
128 127 rexlimdvaa 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> ( E. k e. Z ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) -> ( x ( ball ` D ) r ) e. G ) )
129 40 128 syl5 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) -> ( x ( ball ` D ) r ) e. G ) )
130 39 129 biimtrrid 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> ( ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( 1 / 2 ) ^ k ) < ( r / 2 ) /\ E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. ( x ( ball ` D ) ( r / 2 ) ) ) -> ( x ( ball ` D ) r ) e. G ) )
131 29 38 130 mp2and 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ r e. RR+ ) -> ( x ( ball ` D ) r ) e. G )
132 131 ad2ant2r 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ y e. J ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ y ) ) -> ( x ( ball ` D ) r ) e. G )
133 17 adantr 
 |-  ( ( ph /\ F ( ~~>t ` J ) x ) -> J e. ( TopOn ` X ) )
134 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. J ) -> y C_ X )
135 133 134 sylan 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ y e. J ) -> y C_ X )
136 135 adantr 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ y e. J ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ y ) ) -> y C_ X )
137 simprr 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ y e. J ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ y ) ) -> ( x ( ball ` D ) r ) C_ y )
138 filss 
 |-  ( ( G e. ( Fil ` X ) /\ ( ( x ( ball ` D ) r ) e. G /\ y C_ X /\ ( x ( ball ` D ) r ) C_ y ) ) -> y e. G )
139 24 132 136 137 138 syl13anc 
 |-  ( ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ y e. J ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ y ) ) -> y e. G )
140 139 rexlimdvaa 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ y e. J ) -> ( E. r e. RR+ ( x ( ball ` D ) r ) C_ y -> y e. G ) )
141 23 140 syld 
 |-  ( ( ( ph /\ F ( ~~>t ` J ) x ) /\ y e. J ) -> ( x e. y -> y e. G ) )
142 141 ralrimiva 
 |-  ( ( ph /\ F ( ~~>t ` J ) x ) -> A. y e. J ( x e. y -> y e. G ) )
143 flimopn 
 |-  ( ( J e. ( TopOn ` X ) /\ G e. ( Fil ` X ) ) -> ( x e. ( J fLim G ) <-> ( x e. X /\ A. y e. J ( x e. y -> y e. G ) ) ) )
144 17 8 143 syl2anc 
 |-  ( ph -> ( x e. ( J fLim G ) <-> ( x e. X /\ A. y e. J ( x e. y -> y e. G ) ) ) )
145 144 adantr 
 |-  ( ( ph /\ F ( ~~>t ` J ) x ) -> ( x e. ( J fLim G ) <-> ( x e. X /\ A. y e. J ( x e. y -> y e. G ) ) ) )
146 19 142 145 mpbir2and 
 |-  ( ( ph /\ F ( ~~>t ` J ) x ) -> x e. ( J fLim G ) )
147 146 ne0d 
 |-  ( ( ph /\ F ( ~~>t ` J ) x ) -> ( J fLim G ) =/= (/) )
148 13 147 exlimddv 
 |-  ( ph -> ( J fLim G ) =/= (/) )