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 101 ss2rabd 
 |-  ( ( ( 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 ) } )
103 dfin5 
 |-  ( A i^i ( k (,] +oo ) ) = { x e. A | x e. ( k (,] +oo ) }
104 103 ineqcomi 
 |-  ( ( k (,] +oo ) i^i A ) = { x e. A | x e. ( k (,] +oo ) }
105 9 mptpreima 
 |-  ( `' ( x e. A |-> R ) " ( C ( ball ` ( abs o. - ) ) r ) ) = { x e. A | R e. ( C ( ball ` ( abs o. - ) ) r ) }
106 102 104 105 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 ) ) )
107 funmpt 
 |-  Fun ( x e. A |-> R )
108 inss2 
 |-  ( ( k (,] +oo ) i^i A ) C_ A
109 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 )
110 109 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 )
111 108 110 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 ) )
112 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 ) ) ) )
113 107 111 112 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 ) ) ) )
114 106 113 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 ) )
115 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 )
116 114 115 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 )
117 eleq2 
 |-  ( z = ( ( k (,] +oo ) i^i A ) -> ( +oo e. z <-> +oo e. ( ( k (,] +oo ) i^i A ) ) )
118 imaeq2 
 |-  ( z = ( ( k (,] +oo ) i^i A ) -> ( ( x e. A |-> R ) " z ) = ( ( x e. A |-> R ) " ( ( k (,] +oo ) i^i A ) ) )
119 118 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 ) )
120 117 119 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 ) ) )
121 120 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 ) )
122 49 57 116 121 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 ) )
123 122 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 ) ) )
124 123 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 ) ) )
125 32 124 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 ) )
126 125 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 ) ) )
127 24 126 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 ) ) )
128 127 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 ) ) )
129 20 128 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 ) ) )
130 129 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 ) ) )
131 letopon 
 |-  ( ordTop ` <_ ) e. ( TopOn ` RR* )
132 resttopon 
 |-  ( ( ( ordTop ` <_ ) e. ( TopOn ` RR* ) /\ A C_ RR* ) -> ( ( ordTop ` <_ ) |`t A ) e. ( TopOn ` A ) )
133 131 40 132 sylancr 
 |-  ( ph -> ( ( ordTop ` <_ ) |`t A ) e. ( TopOn ` A ) )
134 6 133 eqeltrid 
 |-  ( ph -> K e. ( TopOn ` A ) )
135 5 cnfldtopon 
 |-  J e. ( TopOn ` CC )
136 135 a1i 
 |-  ( ph -> J e. ( TopOn ` CC ) )
137 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 ) ) ) ) )
138 134 136 14 137 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 ) ) ) ) )
139 138 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 ) ) ) ) )
140 8 130 139 mpbir2and 
 |-  ( ( ph /\ ( x e. B |-> R ) ~~>r C ) -> ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) )
141 simplr 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) )
142 17 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> C e. CC )
143 72 adantl 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> r e. RR* )
144 22 blopn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ C e. CC /\ r e. RR* ) -> ( C ( ball ` ( abs o. - ) ) r ) e. J )
145 21 142 143 144 mp3an2i 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> ( C ( ball ` ( abs o. - ) ) r ) e. J )
146 18 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> ( ( x e. A |-> R ) ` +oo ) = C )
147 simpr 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> r e. RR+ )
148 21 142 147 90 mp3an2i 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> C e. ( C ( ball ` ( abs o. - ) ) r ) )
149 146 148 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 ) )
150 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 ) ) )
151 141 145 149 150 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 ) ) )
152 vex 
 |-  w e. _V
153 152 inex1 
 |-  ( w i^i A ) e. _V
154 153 a1i 
 |-  ( ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) /\ w e. ( ordTop ` <_ ) ) -> ( w i^i A ) e. _V )
155 6 eleq2i 
 |-  ( z e. K <-> z e. ( ( ordTop ` <_ ) |`t A ) )
156 43 ad2antrr 
 |-  ( ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) /\ r e. RR+ ) -> A e. _V )
157 elrest 
 |-  ( ( ( ordTop ` <_ ) e. Top /\ A e. _V ) -> ( z e. ( ( ordTop ` <_ ) |`t A ) <-> E. w e. ( ordTop ` <_ ) z = ( w i^i A ) ) )
158 33 156 157 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 ) ) )
159 155 158 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 ) ) )
160 eleq2 
 |-  ( z = ( w i^i A ) -> ( +oo e. z <-> +oo e. ( w i^i A ) ) )
161 imaeq2 
 |-  ( z = ( w i^i A ) -> ( ( x e. A |-> R ) " z ) = ( ( x e. A |-> R ) " ( w i^i A ) ) )
162 161 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 ) ) )
163 160 162 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 ) ) ) )
164 163 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 ) ) ) )
165 154 159 164 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 ) ) ) )
166 151 165 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 ) ) )
167 elinel1 
 |-  ( +oo e. ( w i^i A ) -> +oo e. w )
168 pnfnei 
 |-  ( ( w e. ( ordTop ` <_ ) /\ +oo e. w ) -> E. k e. RR ( k (,] +oo ) C_ w )
169 167 168 sylan2 
 |-  ( ( w e. ( ordTop ` <_ ) /\ +oo e. ( w i^i A ) ) -> E. k e. RR ( k (,] +oo ) C_ w )
170 df-ima 
 |-  ( ( x e. A |-> R ) " ( w i^i A ) ) = ran ( ( x e. A |-> R ) |` ( w i^i A ) )
171 inss2 
 |-  ( w i^i A ) C_ A
172 resmpt 
 |-  ( ( w i^i A ) C_ A -> ( ( x e. A |-> R ) |` ( w i^i A ) ) = ( x e. ( w i^i A ) |-> R ) )
173 171 172 ax-mp 
 |-  ( ( x e. A |-> R ) |` ( w i^i A ) ) = ( x e. ( w i^i A ) |-> R )
174 173 rneqi 
 |-  ran ( ( x e. A |-> R ) |` ( w i^i A ) ) = ran ( x e. ( w i^i A ) |-> R )
175 170 174 eqtri 
 |-  ( ( x e. A |-> R ) " ( w i^i A ) ) = ran ( x e. ( w i^i A ) |-> R )
176 175 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 ) )
177 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 ) )
178 176 177 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 ) )
179 16 adantr 
 |-  ( ( ph /\ r e. RR+ ) -> A. x e. A R e. CC )
180 ssralv 
 |-  ( ( w i^i A ) C_ A -> ( A. x e. A R e. CC -> A. x e. ( w i^i A ) R e. CC ) )
181 171 179 180 mpsyl 
 |-  ( ( ph /\ r e. RR+ ) -> A. x e. ( w i^i A ) R e. CC )
182 eqid 
 |-  ( x e. ( w i^i A ) |-> R ) = ( x e. ( w i^i A ) |-> R )
183 eleq1 
 |-  ( z = R -> ( z e. ( C ( ball ` ( abs o. - ) ) r ) <-> R e. ( C ( ball ` ( abs o. - ) ) r ) ) )
184 182 183 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 ) ) )
185 181 184 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 ) ) )
186 185 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 ) ) )
187 178 186 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 ) ) )
188 simplrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> ( k (,] +oo ) C_ w )
189 35 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> B C_ RR* )
190 simprl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> x e. B )
191 189 190 sseldd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> x e. RR* )
192 simprr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> k < x )
193 191 pnfged 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> x <_ +oo )
194 simplrl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> k e. RR )
195 194 rexrd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> k e. RR* )
196 195 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 ) ) )
197 191 192 193 196 mpbir3and 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> x e. ( k (,] +oo ) )
198 188 197 sseldd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> x e. w )
199 26 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) -> B C_ A )
200 199 sselda 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ x e. B ) -> x e. A )
201 200 adantrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> x e. A )
202 198 201 elind 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> x e. ( w i^i A ) )
203 202 ex 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) -> ( ( x e. B /\ k < x ) -> x e. ( w i^i A ) ) )
204 203 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 ) ) ) )
205 21 a1i 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> ( abs o. - ) e. ( *Met ` CC ) )
206 72 adantl 
 |-  ( ( ph /\ r e. RR+ ) -> r e. RR* )
207 206 ad2antrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> r e. RR* )
208 17 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> C e. CC )
209 28 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) -> A. x e. B R e. CC )
210 209 r19.21bi 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ x e. B ) -> R e. CC )
211 210 adantrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( k e. RR /\ ( k (,] +oo ) C_ w ) ) /\ ( x e. B /\ k < x ) ) -> R e. CC )
212 205 207 208 211 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 ) )
213 211 208 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 ) ) )
214 213 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 ) )
215 212 214 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 ) )
216 215 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 ) ) )
217 204 216 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 ) ) )
218 217 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 ) ) ) )
219 218 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 ) ) )
220 219 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 ) )
221 220 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 ) )
222 221 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 ) ) )
223 222 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 ) ) )
224 223 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 ) ) ) )
225 187 224 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 ) ) ) )
226 225 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 ) ) ) )
227 169 226 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 ) ) ) )
228 227 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 ) ) )
229 228 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 ) ) )
230 229 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 ) ) )
231 230 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 ) ) )
232 166 231 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 ) )
233 232 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 ) )
234 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 ) ) )
235 234 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 ) ) )
236 233 235 mpbird 
 |-  ( ( ph /\ ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) -> ( x e. B |-> R ) ~~>r C )
237 140 236 impbida 
 |-  ( ph -> ( ( x e. B |-> R ) ~~>r C <-> ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) )