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