Metamath Proof Explorer

Theorem xrlimcnp

Description: Relate a limit of a real-valued sequence at infinity to the continuity of the corresponding extended real function at +oo . Since any ~>r limit can be written in the form on the left side of the implication, this shows that real limits are a special case of topological continuity at a point. (Contributed by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypotheses xrlimcnp.a 
|- ( ph -> A = ( B u. { +oo } ) )
xrlimcnp.b 
|- ( ph -> B C_ RR )
xrlimcnp.r 
|- ( ( ph /\ x e. A ) -> R e. CC )
xrlimcnp.c 
|- ( x = +oo -> R = C )
xrlimcnp.j 
|- J = ( TopOpen ` CCfld )
xrlimcnp.k 
|- K = ( ( ordTop ` <_ ) |`t A )
Assertion xrlimcnp 
|- ( ph -> ( ( x e. B |-> R ) ~~>r C <-> ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) )

Proof

Step Hyp Ref Expression
1 xrlimcnp.a 
 |-  ( ph -> A = ( B u. { +oo } ) )
2 xrlimcnp.b 
 |-  ( ph -> B C_ RR )
3 xrlimcnp.r 
 |-  ( ( ph /\ x e. A ) -> R e. CC )
4 xrlimcnp.c 
 |-  ( x = +oo -> R = C )
5 xrlimcnp.j 
 |-  J = ( TopOpen ` CCfld )
6 xrlimcnp.k 
 |-  K = ( ( ordTop ` <_ ) |`t A )
7 3 fmpttd 
 |-  ( ph -> ( x e. A |-> R ) : A --> CC )
8 7 adantr 
 |-  ( ( ph /\ ( x e. B |-> R ) ~~>r C ) -> ( x e. A |-> R ) : A --> CC )
9 eqid 
 |-  ( x e. A |-> R ) = ( x e. A |-> R )
10 ssun2 
 |-  { +oo } C_ ( B u. { +oo } )
11 pnfex 
 |-  +oo e. _V
12 11 snid 
 |-  +oo e. { +oo }
13 10 12 sselii 
 |-  +oo e. ( B u. { +oo } )
14 13 1 eleqtrrid 
 |-  ( ph -> +oo e. A )
15 4 eleq1d 
 |-  ( x = +oo -> ( R e. CC <-> C e. CC ) )
16 3 ralrimiva 
 |-  ( ph -> A. x e. A R e. CC )
17 15 16 14 rspcdva 
 |-  ( ph -> C e. CC )
18 9 4 14 17 fvmptd3 
 |-  ( ph -> ( ( x e. A |-> R ) ` +oo ) = C )
19 18 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B |-> R ) ~~>r C ) /\ y e. J ) -> ( ( x e. A |-> R ) ` +oo ) = C )
20 19 eleq1d 
 |-  ( ( ( ph /\ ( x e. B |-> R ) ~~>r C ) /\ y e. J ) -> ( ( ( x e. A |-> R ) ` +oo ) e. y <-> C e. y ) )
21 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
22 5 cnfldtopn 
 |-  J = ( MetOpen ` ( abs o. - ) )
23 22 mopni2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ y e. J /\ C e. y ) -> E. r e. RR+ ( C ( ball ` ( abs o. - ) ) r ) C_ y )
24 21 23 mp3an1 
 |-  ( ( y e. J /\ C e. y ) -> E. r e. RR+ ( C ( ball ` ( abs o. - ) ) r ) C_ y )
25 ssun1 
 |-  B C_ ( B u. { +oo } )
26 25 1 sseqtrrid 
 |-  ( ph -> B C_ A )
27 ssralv 
 |-  ( B C_ A -> ( A. x e. A R e. CC -> A. x e. B R e. CC ) )
28 26 16 27 sylc 
 |-  ( ph -> A. x e. B R e. CC )
29 28 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B |-> R ) ~~>r C ) /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) -> A. x e. B R e. CC )
30 simprl 
 |-  ( ( ( ph /\ ( x e. B |-> R ) ~~>r C ) /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) -> r e. RR+ )
31 simplr 
 |-  ( ( ( ph /\ ( x e. B |-> R ) ~~>r C ) /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) -> ( x e. B |-> R ) ~~>r C )
32 29 30 31 rlimi 
 |-  ( ( ( ph /\ ( x e. B |-> R ) ~~>r C ) /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) -> E. k e. RR A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) )
33 letop 
 |-  ( ordTop ` <_ ) e. Top
34 ressxr 
 |-  RR C_ RR*
35 2 34 sstrdi 
 |-  ( ph -> B C_ RR* )
36 pnfxr 
 |-  +oo e. RR*
37 36 a1i 
 |-  ( ph -> +oo e. RR* )
38 37 snssd 
 |-  ( ph -> { +oo } C_ RR* )
39 35 38 unssd 
 |-  ( ph -> ( B u. { +oo } ) C_ RR* )
40 1 39 eqsstrd 
 |-  ( ph -> A C_ RR* )
41 xrex 
 |-  RR* e. _V
42 41 ssex 
 |-  ( A C_ RR* -> A e. _V )
43 40 42 syl 
 |-  ( ph -> A e. _V )
44 43 ad2antrr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> A e. _V )
45 iocpnfordt 
 |-  ( k (,] +oo ) e. ( ordTop ` <_ )
46 45 a1i 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> ( k (,] +oo ) e. ( ordTop ` <_ ) )
47 elrestr 
 |-  ( ( ( ordTop ` <_ ) e. Top /\ A e. _V /\ ( k (,] +oo ) e. ( ordTop ` <_ ) ) -> ( ( k (,] +oo ) i^i A ) e. ( ( ordTop ` <_ ) |`t A ) )
48 33 44 46 47 mp3an2i 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> ( ( k (,] +oo ) i^i A ) e. ( ( ordTop ` <_ ) |`t A ) )
49 48 6 eleqtrrdi 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> ( ( k (,] +oo ) i^i A ) e. K )
50 simprl 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> k e. RR )
51 50 rexrd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> k e. RR* )
52 36 a1i 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> +oo e. RR* )
53 50 ltpnfd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> k < +oo )
54 ubioc1 
 |-  ( ( k e. RR* /\ +oo e. RR* /\ k < +oo ) -> +oo e. ( k (,] +oo ) )
55 51 52 53 54 syl3anc 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> +oo e. ( k (,] +oo ) )
56 14 ad2antrr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> +oo e. A )
57 55 56 elind 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> +oo e. ( ( k (,] +oo ) i^i A ) )
58 simplr 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> k e. RR )
59 58 rexrd 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> k e. RR* )
60 elioc1 
 |-  ( ( k e. RR* /\ +oo e. RR* ) -> ( x e. ( k (,] +oo ) <-> ( x e. RR* /\ k < x /\ x <_ +oo ) ) )
61 59 36 60 sylancl 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> ( x e. ( k (,] +oo ) <-> ( x e. RR* /\ k < x /\ x <_ +oo ) ) )
62 simp2 
 |-  ( ( x e. RR* /\ k < x /\ x <_ +oo ) -> k < x )
63 61 62 biimtrdi 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> ( x e. ( k (,] +oo ) -> k < x ) )
64 2 ad2antrr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) -> B C_ RR )
65 64 sselda 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> x e. RR )
66 ltle 
 |-  ( ( k e. RR /\ x e. RR ) -> ( k < x -> k <_ x ) )
67 58 65 66 syl2anc 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> ( k < x -> k <_ x ) )
68 63 67 syld 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> ( x e. ( k (,] +oo ) -> k <_ x ) )
69 21 a1i 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> ( abs o. - ) e. ( *Met ` CC ) )
70 simprl 
 |-  ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) -> r e. RR+ )
71 70 ad2antrr 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> r e. RR+ )
72 rpxr 
 |-  ( r e. RR+ -> r e. RR* )
73 71 72 syl 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> r e. RR* )
74 17 ad3antrrr 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> C e. CC )
75 28 ad2antrr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) -> A. x e. B R e. CC )
76 75 r19.21bi 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> R e. CC )
77 elbl3 
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ r e. RR* ) /\ ( C e. CC /\ R e. CC ) ) -> ( R e. ( C ( ball ` ( abs o. - ) ) r ) <-> ( R ( abs o. - ) C ) < r ) )
78 69 73 74 76 77 syl22anc 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> ( R e. ( C ( ball ` ( abs o. - ) ) r ) <-> ( R ( abs o. - ) C ) < r ) )
79 eqid 
 |-  ( abs o. - ) = ( abs o. - )
80 79 cnmetdval 
 |-  ( ( R e. CC /\ C e. CC ) -> ( R ( abs o. - ) C ) = ( abs ` ( R - C ) ) )
81 76 74 80 syl2anc 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> ( R ( abs o. - ) C ) = ( abs ` ( R - C ) ) )
82 81 breq1d 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> ( ( R ( abs o. - ) C ) < r <-> ( abs ` ( R - C ) ) < r ) )
83 78 82 bitrd 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> ( R e. ( C ( ball ` ( abs o. - ) ) r ) <-> ( abs ` ( R - C ) ) < r ) )
84 83 biimprd 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> ( ( abs ` ( R - C ) ) < r -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) )
85 68 84 imim12d 
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) /\ x e. B ) -> ( ( k <_ x -> ( abs ` ( R - C ) ) < r ) -> ( x e. ( k (,] +oo ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) ) )
86 85 ralimdva 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ k e. RR ) -> ( A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) -> A. x e. B ( x e. ( k (,] +oo ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) ) )
87 86 impr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> A. x e. B ( x e. ( k (,] +oo ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) )
88 17 ad2antrr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> C e. CC )
89 simplrl 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> r e. RR+ )
90 blcntr 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ C e. CC /\ r e. RR+ ) -> C e. ( C ( ball ` ( abs o. - ) ) r ) )
91 21 88 89 90 mp3an2i 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> C e. ( C ( ball ` ( abs o. - ) ) r ) )
92 91 a1d 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> ( +oo e. ( k (,] +oo ) -> C e. ( C ( ball ` ( abs o. - ) ) r ) ) )
93 eleq1 
 |-  ( x = +oo -> ( x e. ( k (,] +oo ) <-> +oo e. ( k (,] +oo ) ) )
94 4 eleq1d 
 |-  ( x = +oo -> ( R e. ( C ( ball ` ( abs o. - ) ) r ) <-> C e. ( C ( ball ` ( abs o. - ) ) r ) ) )
95 93 94 imbi12d 
 |-  ( x = +oo -> ( ( x e. ( k (,] +oo ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) <-> ( +oo e. ( k (,] +oo ) -> C e. ( C ( ball ` ( abs o. - ) ) r ) ) ) )
96 11 95 ralsn 
 |-  ( A. x e. { +oo } ( x e. ( k (,] +oo ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) <-> ( +oo e. ( k (,] +oo ) -> C e. ( C ( ball ` ( abs o. - ) ) r ) ) )
97 92 96 sylibr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> A. x e. { +oo } ( x e. ( k (,] +oo ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) )
98 ralunb 
 |-  ( A. x e. ( B u. { +oo } ) ( x e. ( k (,] +oo ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) <-> ( A. x e. B ( x e. ( k (,] +oo ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) /\ A. x e. { +oo } ( x e. ( k (,] +oo ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) ) )
99 87 97 98 sylanbrc 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> A. x e. ( B u. { +oo } ) ( x e. ( k (,] +oo ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) )
100 1 ad2antrr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> A = ( B u. { +oo } ) )
101 99 100 raleqtrrdv 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> A. x e. A ( x e. ( k (,] +oo ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) )
102 ss2rab 
 |-  ( { x e. A | x e. ( k (,] +oo ) } C_ { x e. A | R e. ( C ( ball ` ( abs o. - ) ) r ) } <-> A. x e. A ( x e. ( k (,] +oo ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) )
103 101 102 sylibr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> { x e. A | x e. ( k (,] +oo ) } C_ { x e. A | R e. ( C ( ball ` ( abs o. - ) ) r ) } )
104 incom 
 |-  ( ( k (,] +oo ) i^i A ) = ( A i^i ( k (,] +oo ) )
105 dfin5 
 |-  ( A i^i ( k (,] +oo ) ) = { x e. A | x e. ( k (,] +oo ) }
106 104 105 eqtri 
 |-  ( ( k (,] +oo ) i^i A ) = { x e. A | x e. ( k (,] +oo ) }
107 9 mptpreima 
 |-  ( `' ( x e. A |-> R ) " ( C ( ball ` ( abs o. - ) ) r ) ) = { x e. A | R e. ( C ( ball ` ( abs o. - ) ) r ) }
108 103 106 107 3sstr4g 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> ( ( k (,] +oo ) i^i A ) C_ ( `' ( x e. A |-> R ) " ( C ( ball ` ( abs o. - ) ) r ) ) )
109 funmpt 
 |-  Fun ( x e. A |-> R )
110 inss2 
 |-  ( ( k (,] +oo ) i^i A ) C_ A
111 7 ad2antrr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> ( x e. A |-> R ) : A --> CC )
112 111 fdmd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> dom ( x e. A |-> R ) = A )
113 110 112 sseqtrrid 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> ( ( k (,] +oo ) i^i A ) C_ dom ( x e. A |-> R ) )
114 funimass3 
 |-  ( ( Fun ( x e. A |-> R ) /\ ( ( k (,] +oo ) i^i A ) C_ dom ( x e. A |-> R ) ) -> ( ( ( x e. A |-> R ) " ( ( k (,] +oo ) i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) <-> ( ( k (,] +oo ) i^i A ) C_ ( `' ( x e. A |-> R ) " ( C ( ball ` ( abs o. - ) ) r ) ) ) )
115 109 113 114 sylancr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> ( ( ( x e. A |-> R ) " ( ( k (,] +oo ) i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) <-> ( ( k (,] +oo ) i^i A ) C_ ( `' ( x e. A |-> R ) " ( C ( ball ` ( abs o. - ) ) r ) ) ) )
116 108 115 mpbird 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> ( ( x e. A |-> R ) " ( ( k (,] +oo ) i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) )
117 simplrr 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> ( C ( ball ` ( abs o. - ) ) r ) C_ y )
118 116 117 sstrd 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> ( ( x e. A |-> R ) " ( ( k (,] +oo ) i^i A ) ) C_ y )
119 eleq2 
 |-  ( z = ( ( k (,] +oo ) i^i A ) -> ( +oo e. z <-> +oo e. ( ( k (,] +oo ) i^i A ) ) )
120 imaeq2 
 |-  ( z = ( ( k (,] +oo ) i^i A ) -> ( ( x e. A |-> R ) " z ) = ( ( x e. A |-> R ) " ( ( k (,] +oo ) i^i A ) ) )
121 120 sseq1d 
 |-  ( z = ( ( k (,] +oo ) i^i A ) -> ( ( ( x e. A |-> R ) " z ) C_ y <-> ( ( x e. A |-> R ) " ( ( k (,] +oo ) i^i A ) ) C_ y ) )
122 119 121 anbi12d 
 |-  ( z = ( ( k (,] +oo ) i^i A ) -> ( ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ y ) <-> ( +oo e. ( ( k (,] +oo ) i^i A ) /\ ( ( x e. A |-> R ) " ( ( k (,] +oo ) i^i A ) ) C_ y ) ) )
123 122 rspcev 
 |-  ( ( ( ( k (,] +oo ) i^i A ) e. K /\ ( +oo e. ( ( k (,] +oo ) i^i A ) /\ ( ( x e. A |-> R ) " ( ( k (,] +oo ) i^i A ) ) C_ y ) ) -> E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ y ) )
124 49 57 118 123 syl12anc 
 |-  ( ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) /\ ( k e. RR /\ A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) ) ) -> E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ y ) )
125 124 rexlimdvaa 
 |-  ( ( ph /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) -> ( E. k e. RR A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) -> E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ y ) ) )
126 125 adantlr 
 |-  ( ( ( ph /\ ( x e. B |-> R ) ~~>r C ) /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) -> ( E. k e. RR A. x e. B ( k <_ x -> ( abs ` ( R - C ) ) < r ) -> E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ y ) ) )
127 32 126 mpd 
 |-  ( ( ( ph /\ ( x e. B |-> R ) ~~>r C ) /\ ( r e. RR+ /\ ( C ( ball ` ( abs o. - ) ) r ) C_ y ) ) -> E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ y ) )
128 127 rexlimdvaa 
 |-  ( ( ph /\ ( x e. B |-> R ) ~~>r C ) -> ( E. r e. RR+ ( C ( ball ` ( abs o. - ) ) r ) C_ y -> E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ y ) ) )
129 24 128 syl5 
 |-  ( ( ph /\ ( x e. B |-> R ) ~~>r C ) -> ( ( y e. J /\ C e. y ) -> E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ y ) ) )
130 129 expdimp 
 |-  ( ( ( ph /\ ( x e. B |-> R ) ~~>r C ) /\ y e. J ) -> ( C e. y -> E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ y ) ) )
131 20 130 sylbid 
 |-  ( ( ( ph /\ ( x e. B |-> R ) ~~>r C ) /\ y e. J ) -> ( ( ( x e. A |-> R ) ` +oo ) e. y -> E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ y ) ) )
132 131 ralrimiva 
 |-  ( ( ph /\ ( x e. B |-> R ) ~~>r C ) -> A. y e. J ( ( ( x e. A |-> R ) ` +oo ) e. y -> E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ y ) ) )
133 letopon 
 |-  ( ordTop ` <_ ) e. ( TopOn ` RR* )
134 resttopon 
 |-  ( ( ( ordTop ` <_ ) e. ( TopOn ` RR* ) /\ A C_ RR* ) -> ( ( ordTop ` <_ ) |`t A ) e. ( TopOn ` A ) )
135 133 40 134 sylancr 
 |-  ( ph -> ( ( ordTop ` <_ ) |`t A ) e. ( TopOn ` A ) )
136 6 135 eqeltrid 
 |-  ( ph -> K e. ( TopOn ` A ) )
137 5 cnfldtopon 
 |-  J e. ( TopOn ` CC )
138 137 a1i 
 |-  ( ph -> J e. ( TopOn ` CC ) )
139 iscnp 
 |-  ( ( K e. ( TopOn ` A ) /\ J e. ( TopOn ` CC ) /\ +oo e. A ) -> ( ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) <-> ( ( x e. A |-> R ) : A --> CC /\ A. y e. J ( ( ( x e. A |-> R ) ` +oo ) e. y -> E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ y ) ) ) ) )
140 136 138 14 139 syl3anc 
 |-  ( ph -> ( ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) <-> ( ( x e. A |-> R ) : A --> CC /\ A. y e. J ( ( ( x e. A |-> R ) ` +oo ) e. y -> E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ y ) ) ) ) )
141 140 adantr 
 |-  ( ( ph /\ ( x e. B |-> R ) ~~>r C ) -> ( ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) <-> ( ( x e. A |-> R ) : A --> CC /\ A. y e. J ( ( ( x e. A |-> R ) ` +oo ) e. y -> E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ y ) ) ) ) )
142 8 132 141 mpbir2and 
 |-  ( ( ph /\ ( x e. B |-> R ) ~~>r C ) -> ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) )
143 simplr 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) )
144 17 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> C e. CC )
145 72 adantl 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> r e. RR* )
146 22 blopn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ C e. CC /\ r e. RR* ) -> ( C ( ball ` ( abs o. - ) ) r ) e. J )
147 21 144 145 146 mp3an2i 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> ( C ( ball ` ( abs o. - ) ) r ) e. J )
148 18 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> ( ( x e. A |-> R ) ` +oo ) = C )
149 simpr 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> r e. RR+ )
150 21 144 149 90 mp3an2i 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> C e. ( C ( ball ` ( abs o. - ) ) r ) )
151 148 150 eqeltrd 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> ( ( x e. A |-> R ) ` +oo ) e. ( C ( ball ` ( abs o. - ) ) r ) )
152 cnpimaex 
 |-  ( ( ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) /\ ( C ( ball ` ( abs o. - ) ) r ) e. J /\ ( ( x e. A |-> R ) ` +oo ) e. ( C ( ball ` ( abs o. - ) ) r ) ) -> E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ ( C ( ball ` ( abs o. - ) ) r ) ) )
153 143 147 151 152 syl3anc 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ ( C ( ball ` ( abs o. - ) ) r ) ) )
154 vex 
 |-  w e. _V
155 154 inex1 
 |-  ( w i^i A ) e. _V
156 155 a1i 
 |-  ( ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) /\ w e. ( ordTop ` <_ ) ) -> ( w i^i A ) e. _V )
157 6 eleq2i 
 |-  ( z e. K <-> z e. ( ( ordTop ` <_ ) |`t A ) )
158 43 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> A e. _V )
159 elrest 
 |-  ( ( ( ordTop ` <_ ) e. Top /\ A e. _V ) -> ( z e. ( ( ordTop ` <_ ) |`t A ) <-> E. w e. ( ordTop ` <_ ) z = ( w i^i A ) ) )
160 33 158 159 sylancr 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> ( z e. ( ( ordTop ` <_ ) |`t A ) <-> E. w e. ( ordTop ` <_ ) z = ( w i^i A ) ) )
161 157 160 bitrid 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> ( z e. K <-> E. w e. ( ordTop ` <_ ) z = ( w i^i A ) ) )
162 eleq2 
 |-  ( z = ( w i^i A ) -> ( +oo e. z <-> +oo e. ( w i^i A ) ) )
163 imaeq2 
 |-  ( z = ( w i^i A ) -> ( ( x e. A |-> R ) " z ) = ( ( x e. A |-> R ) " ( w i^i A ) ) )
164 163 sseq1d 
 |-  ( z = ( w i^i A ) -> ( ( ( x e. A |-> R ) " z ) C_ ( C ( ball ` ( abs o. - ) ) r ) <-> ( ( x e. A |-> R ) " ( w i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) ) )
165 162 164 anbi12d 
 |-  ( z = ( w i^i A ) -> ( ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ ( C ( ball ` ( abs o. - ) ) r ) ) <-> ( +oo e. ( w i^i A ) /\ ( ( x e. A |-> R ) " ( w i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) ) ) )
166 165 adantl 
 |-  ( ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) /\ z = ( w i^i A ) ) -> ( ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ ( C ( ball ` ( abs o. - ) ) r ) ) <-> ( +oo e. ( w i^i A ) /\ ( ( x e. A |-> R ) " ( w i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) ) ) )
167 156 161 166 rexxfr2d 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> ( E. z e. K ( +oo e. z /\ ( ( x e. A |-> R ) " z ) C_ ( C ( ball ` ( abs o. - ) ) r ) ) <-> E. w e. ( ordTop ` <_ ) ( +oo e. ( w i^i A ) /\ ( ( x e. A |-> R ) " ( w i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) ) ) )
168 153 167 mpbid 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> E. w e. ( ordTop ` <_ ) ( +oo e. ( w i^i A ) /\ ( ( x e. A |-> R ) " ( w i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) ) )
169 elinel1 
 |-  ( +oo e. ( w i^i A ) -> +oo e. w )
170 pnfnei 
 |-  ( ( w e. ( ordTop ` <_ ) /\ +oo e. w ) -> E. k e. RR ( k (,] +oo ) C_ w )
171 169 170 sylan2 
 |-  ( ( w e. ( ordTop ` <_ ) /\ +oo e. ( w i^i A ) ) -> E. k e. RR ( k (,] +oo ) C_ w )
172 df-ima 
 |-  ( ( x e. A |-> R ) " ( w i^i A ) ) = ran ( ( x e. A |-> R ) |` ( w i^i A ) )
173 inss2 
 |-  ( w i^i A ) C_ A
174 resmpt 
 |-  ( ( w i^i A ) C_ A -> ( ( x e. A |-> R ) |` ( w i^i A ) ) = ( x e. ( w i^i A ) |-> R ) )
175 173 174 ax-mp 
 |-  ( ( x e. A |-> R ) |` ( w i^i A ) ) = ( x e. ( w i^i A ) |-> R )
176 175 rneqi 
 |-  ran ( ( x e. A |-> R ) |` ( w i^i A ) ) = ran ( x e. ( w i^i A ) |-> R )
177 172 176 eqtri 
 |-  ( ( x e. A |-> R ) " ( w i^i A ) ) = ran ( x e. ( w i^i A ) |-> R )
178 177 sseq1i 
 |-  ( ( ( x e. A |-> R ) " ( w i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) <-> ran ( x e. ( w i^i A ) |-> R ) C_ ( C ( ball ` ( abs o. - ) ) r ) )
179 dfss3 
 |-  ( ran ( x e. ( w i^i A ) |-> R ) C_ ( C ( ball ` ( abs o. - ) ) r ) <-> A. z e. ran ( x e. ( w i^i A ) |-> R ) z e. ( C ( ball ` ( abs o. - ) ) r ) )
180 178 179 bitri 
 |-  ( ( ( x e. A |-> R ) " ( w i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) <-> A. z e. ran ( x e. ( w i^i A ) |-> R ) z e. ( C ( ball ` ( abs o. - ) ) r ) )
181 16 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> A. x e. A R e. CC )
182 ssralv 
 |-  ( ( w i^i A ) C_ A -> ( A. x e. A R e. CC -> A. x e. ( w i^i A ) R e. CC ) )
183 173 181 182 mpsyl 
 |-  ( ( ph /\ r e. RR+ ) -> A. x e. ( w i^i A ) R e. CC )
184 eqid 
 |-  ( x e. ( w i^i A ) |-> R ) = ( x e. ( w i^i A ) |-> R )
185 eleq1 
 |-  ( z = R -> ( z e. ( C ( ball ` ( abs o. - ) ) r ) <-> R e. ( C ( ball ` ( abs o. - ) ) r ) ) )
186 184 185 ralrnmptw 
 |-  ( A. x e. ( w i^i A ) R e. CC -> ( A. z e. ran ( x e. ( w i^i A ) |-> R ) z e. ( C ( ball ` ( abs o. - ) ) r ) <-> A. x e. ( w i^i A ) R e. ( C ( ball ` ( abs o. - ) ) r ) ) )
187 183 186 syl 
 |-  ( ( ph /\ r e. RR+ ) -> ( A. z e. ran ( x e. ( w i^i A ) |-> R ) z e. ( C ( ball ` ( abs o. - ) ) r ) <-> A. x e. ( w i^i A ) R e. ( C ( ball ` ( abs o. - ) ) r ) ) )
188 187 biimpd 
 |-  ( ( ph /\ r e. RR+ ) -> ( A. z e. ran ( x e. ( w i^i A ) |-> R ) z e. ( C ( ball ` ( abs o. - ) ) r ) -> A. x e. ( w i^i A ) R e. ( C ( ball ` ( abs o. - ) ) r ) ) )
189 180 188 biimtrid 
 |-  ( ( ph /\ r e. RR+ ) -> ( ( ( x e. A |-> R ) " ( w i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) -> A. x e. ( w i^i A ) R e. ( C ( ball ` ( abs o. - ) ) r ) ) )
190 simplrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> ( k (,] +oo ) C_ w )
191 35 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> B C_ RR* )
192 simprl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> x e. B )
193 191 192 sseldd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> x e. RR* )
194 simprr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> k < x )
195 pnfge 
 |-  ( x e. RR* -> x <_ +oo )
196 193 195 syl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> x <_ +oo )
197 simplrl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> k e. RR )
198 197 rexrd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> k e. RR* )
199 198 36 60 sylancl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> ( x e. ( k (,] +oo ) <-> ( x e. RR* /\ k < x /\ x <_ +oo ) ) )
200 193 194 196 199 mpbir3and 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> x e. ( k (,] +oo ) )
201 190 200 sseldd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> x e. w )
202 26 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) -> B C_ A )
203 202 sselda 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ x e. B ) -> x e. A )
204 203 adantrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> x e. A )
205 201 204 elind 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> x e. ( w i^i A ) )
206 205 ex 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) -> ( ( x e. B /\ k < x ) -> x e. ( w i^i A ) ) )
207 206 imim1d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) -> ( ( x e. ( w i^i A ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) -> ( ( x e. B /\ k < x ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) ) )
208 21 a1i 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> ( abs o. - ) e. ( *Met ` CC ) )
209 72 adantl 
 |-  ( ( ph /\ r e. RR+ ) -> r e. RR* )
210 209 ad2antrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> r e. RR* )
211 17 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> C e. CC )
212 28 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) -> A. x e. B R e. CC )
213 212 r19.21bi 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ x e. B ) -> R e. CC )
214 213 adantrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> R e. CC )
215 208 210 211 214 77 syl22anc 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> ( R e. ( C ( ball ` ( abs o. - ) ) r ) <-> ( R ( abs o. - ) C ) < r ) )
216 214 211 80 syl2anc 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> ( R ( abs o. - ) C ) = ( abs ` ( R - C ) ) )
217 216 breq1d 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> ( ( R ( abs o. - ) C ) < r <-> ( abs ` ( R - C ) ) < r ) )
218 215 217 bitrd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> ( R e. ( C ( ball ` ( abs o. - ) ) r ) <-> ( abs ` ( R - C ) ) < r ) )
219 218 pm5.74da 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) -> ( ( ( x e. B /\ k < x ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) <-> ( ( x e. B /\ k < x ) -> ( abs ` ( R - C ) ) < r ) ) )
220 207 219 sylibd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) -> ( ( x e. ( w i^i A ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) -> ( ( x e. B /\ k < x ) -> ( abs ` ( R - C ) ) < r ) ) )
221 220 exp4a 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) -> ( ( x e. ( w i^i A ) -> R e. ( C ( ball ` ( abs o. - ) ) r ) ) -> ( x e. B -> ( k < x -> ( abs ` ( R - C ) ) < r ) ) ) )
222 221 ralimdv2 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) -> ( A. x e. ( w i^i A ) R e. ( C ( ball ` ( abs o. - ) ) r ) -> A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) ) )
223 222 imp 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ A. x e. ( w i^i A ) R e. ( C ( ball ` ( abs o. - ) ) r ) ) -> A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) )
224 223 an32s 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ A. x e. ( w i^i A ) R e. ( C ( ball ` ( abs o. - ) ) r ) ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) -> A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) )
225 224 expr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ A. x e. ( w i^i A ) R e. ( C ( ball ` ( abs o. - ) ) r ) ) /\ k e. RR ) -> ( ( k (,] +oo ) C_ w -> A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) ) )
226 225 reximdva 
 |-  ( ( ( ph /\ r e. RR+ ) /\ A. x e. ( w i^i A ) R e. ( C ( ball ` ( abs o. - ) ) r ) ) -> ( E. k e. RR ( k (,] +oo ) C_ w -> E. k e. RR A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) ) )
227 226 ex 
 |-  ( ( ph /\ r e. RR+ ) -> ( A. x e. ( w i^i A ) R e. ( C ( ball ` ( abs o. - ) ) r ) -> ( E. k e. RR ( k (,] +oo ) C_ w -> E. k e. RR A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) ) ) )
228 189 227 syld 
 |-  ( ( ph /\ r e. RR+ ) -> ( ( ( x e. A |-> R ) " ( w i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) -> ( E. k e. RR ( k (,] +oo ) C_ w -> E. k e. RR A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) ) ) )
229 228 com23 
 |-  ( ( ph /\ r e. RR+ ) -> ( E. k e. RR ( k (,] +oo ) C_ w -> ( ( ( x e. A |-> R ) " ( w i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) -> E. k e. RR A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) ) ) )
230 171 229 syl5 
 |-  ( ( ph /\ r e. RR+ ) -> ( ( w e. ( ordTop ` <_ ) /\ +oo e. ( w i^i A ) ) -> ( ( ( x e. A |-> R ) " ( w i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) -> E. k e. RR A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) ) ) )
231 230 impl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ w e. ( ordTop ` <_ ) ) /\ +oo e. ( w i^i A ) ) -> ( ( ( x e. A |-> R ) " ( w i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) -> E. k e. RR A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) ) )
232 231 expimpd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ w e. ( ordTop ` <_ ) ) -> ( ( +oo e. ( w i^i A ) /\ ( ( x e. A |-> R ) " ( w i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) ) -> E. k e. RR A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) ) )
233 232 rexlimdva 
 |-  ( ( ph /\ r e. RR+ ) -> ( E. w e. ( ordTop ` <_ ) ( +oo e. ( w i^i A ) /\ ( ( x e. A |-> R ) " ( w i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) ) -> E. k e. RR A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) ) )
234 233 adantlr 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> ( E. w e. ( ordTop ` <_ ) ( +oo e. ( w i^i A ) /\ ( ( x e. A |-> R ) " ( w i^i A ) ) C_ ( C ( ball ` ( abs o. - ) ) r ) ) -> E. k e. RR A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) ) )
235 168 234 mpd 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> E. k e. RR A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) )
236 235 ralrimiva 
 |-  ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) -> A. r e. RR+ E. k e. RR A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) )
237 28 2 17 rlim2lt 
 |-  ( ph -> ( ( x e. B |-> R ) ~~>r C <-> A. r e. RR+ E. k e. RR A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) ) )
238 237 adantr 
 |-  ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) -> ( ( x e. B |-> R ) ~~>r C <-> A. r e. RR+ E. k e. RR A. x e. B ( k < x -> ( abs ` ( R - C ) ) < r ) ) )
239 236 238 mpbird 
 |-  ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) -> ( x e. B |-> R ) ~~>r C )
240 142 239 impbida 
 |-  ( ph -> ( ( x e. B |-> R ) ~~>r C <-> ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) )