Metamath Proof Explorer

Theorem ellimc3

Description: Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses ellimc3.f 
|- ( ph -> F : A --> CC )
ellimc3.a 
|- ( ph -> A C_ CC )
ellimc3.b 
|- ( ph -> B e. CC )
Assertion ellimc3 
|- ( ph -> ( C e. ( F limCC B ) <-> ( C e. CC /\ A. x e. RR+ E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) )

Proof

Step Hyp Ref Expression
1 ellimc3.f 
 |-  ( ph -> F : A --> CC )
2 ellimc3.a 
 |-  ( ph -> A C_ CC )
3 ellimc3.b 
 |-  ( ph -> B e. CC )
4 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
5 1 2 3 4 ellimc2 
 |-  ( ph -> ( C e. ( F limCC B ) <-> ( C e. CC /\ A. u e. ( TopOpen ` CCfld ) ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) ) ) )
6 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
7 simplr 
 |-  ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) -> C e. CC )
8 simpr 
 |-  ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) -> x e. RR+ )
9 blcntr 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ C e. CC /\ x e. RR+ ) -> C e. ( C ( ball ` ( abs o. - ) ) x ) )
10 6 7 8 9 mp3an2i 
 |-  ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) -> C e. ( C ( ball ` ( abs o. - ) ) x ) )
11 rpxr 
 |-  ( x e. RR+ -> x e. RR* )
12 11 adantl 
 |-  ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) -> x e. RR* )
13 4 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
14 13 blopn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ C e. CC /\ x e. RR* ) -> ( C ( ball ` ( abs o. - ) ) x ) e. ( TopOpen ` CCfld ) )
15 6 7 12 14 mp3an2i 
 |-  ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) -> ( C ( ball ` ( abs o. - ) ) x ) e. ( TopOpen ` CCfld ) )
16 eleq2 
 |-  ( u = ( C ( ball ` ( abs o. - ) ) x ) -> ( C e. u <-> C e. ( C ( ball ` ( abs o. - ) ) x ) ) )
17 sseq2 
 |-  ( u = ( C ( ball ` ( abs o. - ) ) x ) -> ( ( F " ( v i^i ( A \ { B } ) ) ) C_ u <-> ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) )
18 17 anbi2d 
 |-  ( u = ( C ( ball ` ( abs o. - ) ) x ) -> ( ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) <-> ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) ) )
19 18 rexbidv 
 |-  ( u = ( C ( ball ` ( abs o. - ) ) x ) -> ( E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) <-> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) ) )
20 16 19 imbi12d 
 |-  ( u = ( C ( ball ` ( abs o. - ) ) x ) -> ( ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) <-> ( C e. ( C ( ball ` ( abs o. - ) ) x ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) ) ) )
21 20 rspcv 
 |-  ( ( C ( ball ` ( abs o. - ) ) x ) e. ( TopOpen ` CCfld ) -> ( A. u e. ( TopOpen ` CCfld ) ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) -> ( C e. ( C ( ball ` ( abs o. - ) ) x ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) ) ) )
22 15 21 syl 
 |-  ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) -> ( A. u e. ( TopOpen ` CCfld ) ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) -> ( C e. ( C ( ball ` ( abs o. - ) ) x ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) ) ) )
23 10 22 mpid 
 |-  ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) -> ( A. u e. ( TopOpen ` CCfld ) ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) ) )
24 13 mopni2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ v e. ( TopOpen ` CCfld ) /\ B e. v ) -> E. y e. RR+ ( B ( ball ` ( abs o. - ) ) y ) C_ v )
25 6 24 mp3an1 
 |-  ( ( v e. ( TopOpen ` CCfld ) /\ B e. v ) -> E. y e. RR+ ( B ( ball ` ( abs o. - ) ) y ) C_ v )
26 ssrin 
 |-  ( ( B ( ball ` ( abs o. - ) ) y ) C_ v -> ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) C_ ( v i^i ( A \ { B } ) ) )
27 imass2 
 |-  ( ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) C_ ( v i^i ( A \ { B } ) ) -> ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( F " ( v i^i ( A \ { B } ) ) ) )
28 sstr2 
 |-  ( ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( F " ( v i^i ( A \ { B } ) ) ) -> ( ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) )
29 26 27 28 3syl 
 |-  ( ( B ( ball ` ( abs o. - ) ) y ) C_ v -> ( ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) )
30 29 com12 
 |-  ( ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> ( ( B ( ball ` ( abs o. - ) ) y ) C_ v -> ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) )
31 30 reximdv 
 |-  ( ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> ( E. y e. RR+ ( B ( ball ` ( abs o. - ) ) y ) C_ v -> E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) )
32 25 31 syl5com 
 |-  ( ( v e. ( TopOpen ` CCfld ) /\ B e. v ) -> ( ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) )
33 32 impr 
 |-  ( ( v e. ( TopOpen ` CCfld ) /\ ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) ) -> E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) )
34 33 rexlimiva 
 |-  ( E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) -> E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) )
35 23 34 syl6 
 |-  ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) -> ( A. u e. ( TopOpen ` CCfld ) ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) -> E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) )
36 35 ralrimdva 
 |-  ( ( ph /\ C e. CC ) -> ( A. u e. ( TopOpen ` CCfld ) ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) -> A. x e. RR+ E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) )
37 13 mopni2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ u e. ( TopOpen ` CCfld ) /\ C e. u ) -> E. x e. RR+ ( C ( ball ` ( abs o. - ) ) x ) C_ u )
38 6 37 mp3an1 
 |-  ( ( u e. ( TopOpen ` CCfld ) /\ C e. u ) -> E. x e. RR+ ( C ( ball ` ( abs o. - ) ) x ) C_ u )
39 r19.29r 
 |-  ( ( E. x e. RR+ ( C ( ball ` ( abs o. - ) ) x ) C_ u /\ A. x e. RR+ E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) -> E. x e. RR+ ( ( C ( ball ` ( abs o. - ) ) x ) C_ u /\ E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) )
40 3 ad3antrrr 
 |-  ( ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) /\ y e. RR+ ) -> B e. CC )
41 simpr 
 |-  ( ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) /\ y e. RR+ ) -> y e. RR+ )
42 41 rpxrd 
 |-  ( ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) /\ y e. RR+ ) -> y e. RR* )
43 13 blopn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ B e. CC /\ y e. RR* ) -> ( B ( ball ` ( abs o. - ) ) y ) e. ( TopOpen ` CCfld ) )
44 6 40 42 43 mp3an2i 
 |-  ( ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) /\ y e. RR+ ) -> ( B ( ball ` ( abs o. - ) ) y ) e. ( TopOpen ` CCfld ) )
45 blcntr 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ B e. CC /\ y e. RR+ ) -> B e. ( B ( ball ` ( abs o. - ) ) y ) )
46 6 40 41 45 mp3an2i 
 |-  ( ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) /\ y e. RR+ ) -> B e. ( B ( ball ` ( abs o. - ) ) y ) )
47 eleq2 
 |-  ( v = ( B ( ball ` ( abs o. - ) ) y ) -> ( B e. v <-> B e. ( B ( ball ` ( abs o. - ) ) y ) ) )
48 ineq1 
 |-  ( v = ( B ( ball ` ( abs o. - ) ) y ) -> ( v i^i ( A \ { B } ) ) = ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) )
49 48 imaeq2d 
 |-  ( v = ( B ( ball ` ( abs o. - ) ) y ) -> ( F " ( v i^i ( A \ { B } ) ) ) = ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) )
50 49 sseq1d 
 |-  ( v = ( B ( ball ` ( abs o. - ) ) y ) -> ( ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) <-> ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) )
51 47 50 anbi12d 
 |-  ( v = ( B ( ball ` ( abs o. - ) ) y ) -> ( ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) <-> ( B e. ( B ( ball ` ( abs o. - ) ) y ) /\ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) ) )
52 51 rspcev 
 |-  ( ( ( B ( ball ` ( abs o. - ) ) y ) e. ( TopOpen ` CCfld ) /\ ( B e. ( B ( ball ` ( abs o. - ) ) y ) /\ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) )
53 52 expr 
 |-  ( ( ( B ( ball ` ( abs o. - ) ) y ) e. ( TopOpen ` CCfld ) /\ B e. ( B ( ball ` ( abs o. - ) ) y ) ) -> ( ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) ) )
54 44 46 53 syl2anc 
 |-  ( ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) /\ y e. RR+ ) -> ( ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) ) )
55 54 rexlimdva 
 |-  ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) -> ( E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) ) )
56 sstr2 
 |-  ( ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> ( ( C ( ball ` ( abs o. - ) ) x ) C_ u -> ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) )
57 56 com12 
 |-  ( ( C ( ball ` ( abs o. - ) ) x ) C_ u -> ( ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) )
58 57 anim2d 
 |-  ( ( C ( ball ` ( abs o. - ) ) x ) C_ u -> ( ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) -> ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) )
59 58 reximdv 
 |-  ( ( C ( ball ` ( abs o. - ) ) x ) C_ u -> ( E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) )
60 55 59 syl9 
 |-  ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) -> ( ( C ( ball ` ( abs o. - ) ) x ) C_ u -> ( E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) ) )
61 60 impd 
 |-  ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) -> ( ( ( C ( ball ` ( abs o. - ) ) x ) C_ u /\ E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) )
62 61 rexlimdva 
 |-  ( ( ph /\ C e. CC ) -> ( E. x e. RR+ ( ( C ( ball ` ( abs o. - ) ) x ) C_ u /\ E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) )
63 39 62 syl5 
 |-  ( ( ph /\ C e. CC ) -> ( ( E. x e. RR+ ( C ( ball ` ( abs o. - ) ) x ) C_ u /\ A. x e. RR+ E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) )
64 63 expd 
 |-  ( ( ph /\ C e. CC ) -> ( E. x e. RR+ ( C ( ball ` ( abs o. - ) ) x ) C_ u -> ( A. x e. RR+ E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) ) )
65 38 64 syl5 
 |-  ( ( ph /\ C e. CC ) -> ( ( u e. ( TopOpen ` CCfld ) /\ C e. u ) -> ( A. x e. RR+ E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) ) )
66 65 expdimp 
 |-  ( ( ( ph /\ C e. CC ) /\ u e. ( TopOpen ` CCfld ) ) -> ( C e. u -> ( A. x e. RR+ E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) ) )
67 66 com23 
 |-  ( ( ( ph /\ C e. CC ) /\ u e. ( TopOpen ` CCfld ) ) -> ( A. x e. RR+ E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) ) )
68 67 ralrimdva 
 |-  ( ( ph /\ C e. CC ) -> ( A. x e. RR+ E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) -> A. u e. ( TopOpen ` CCfld ) ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) ) )
69 36 68 impbid 
 |-  ( ( ph /\ C e. CC ) -> ( A. u e. ( TopOpen ` CCfld ) ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) <-> A. x e. RR+ E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) ) )
70 1 ad2antrr 
 |-  ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) -> F : A --> CC )
71 70 ffund 
 |-  ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) -> Fun F )
72 inss2 
 |-  ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) C_ ( A \ { B } )
73 difss 
 |-  ( A \ { B } ) C_ A
74 70 fdmd 
 |-  ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) -> dom F = A )
75 73 74 sseqtrrid 
 |-  ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) -> ( A \ { B } ) C_ dom F )
76 72 75 sstrid 
 |-  ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) -> ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) C_ dom F )
77 funimass4 
 |-  ( ( Fun F /\ ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) C_ dom F ) -> ( ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) <-> A. z e. ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) ) )
78 71 76 77 syl2anc 
 |-  ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) -> ( ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) <-> A. z e. ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) ) )
79 6 a1i 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> ( abs o. - ) e. ( *Met ` CC ) )
80 simplrr 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> y e. RR+ )
81 80 rpxrd 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> y e. RR* )
82 3 ad3antrrr 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> B e. CC )
83 73 2 sstrid 
 |-  ( ph -> ( A \ { B } ) C_ CC )
84 83 ad2antrr 
 |-  ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) -> ( A \ { B } ) C_ CC )
85 84 sselda 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> z e. CC )
86 elbl3 
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ y e. RR* ) /\ ( B e. CC /\ z e. CC ) ) -> ( z e. ( B ( ball ` ( abs o. - ) ) y ) <-> ( z ( abs o. - ) B ) < y ) )
87 79 81 82 85 86 syl22anc 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> ( z e. ( B ( ball ` ( abs o. - ) ) y ) <-> ( z ( abs o. - ) B ) < y ) )
88 eqid 
 |-  ( abs o. - ) = ( abs o. - )
89 88 cnmetdval 
 |-  ( ( z e. CC /\ B e. CC ) -> ( z ( abs o. - ) B ) = ( abs ` ( z - B ) ) )
90 85 82 89 syl2anc 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> ( z ( abs o. - ) B ) = ( abs ` ( z - B ) ) )
91 90 breq1d 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> ( ( z ( abs o. - ) B ) < y <-> ( abs ` ( z - B ) ) < y ) )
92 87 91 bitrd 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> ( z e. ( B ( ball ` ( abs o. - ) ) y ) <-> ( abs ` ( z - B ) ) < y ) )
93 simplrl 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> x e. RR+ )
94 93 rpxrd 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> x e. RR* )
95 simpllr 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> C e. CC )
96 eldifi 
 |-  ( z e. ( A \ { B } ) -> z e. A )
97 ffvelrn 
 |-  ( ( F : A --> CC /\ z e. A ) -> ( F ` z ) e. CC )
98 70 96 97 syl2an 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> ( F ` z ) e. CC )
99 elbl3 
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ x e. RR* ) /\ ( C e. CC /\ ( F ` z ) e. CC ) ) -> ( ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) <-> ( ( F ` z ) ( abs o. - ) C ) < x ) )
100 79 94 95 98 99 syl22anc 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> ( ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) <-> ( ( F ` z ) ( abs o. - ) C ) < x ) )
101 88 cnmetdval 
 |-  ( ( ( F ` z ) e. CC /\ C e. CC ) -> ( ( F ` z ) ( abs o. - ) C ) = ( abs ` ( ( F ` z ) - C ) ) )
102 98 95 101 syl2anc 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> ( ( F ` z ) ( abs o. - ) C ) = ( abs ` ( ( F ` z ) - C ) ) )
103 102 breq1d 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> ( ( ( F ` z ) ( abs o. - ) C ) < x <-> ( abs ` ( ( F ` z ) - C ) ) < x ) )
104 100 103 bitrd 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> ( ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) <-> ( abs ` ( ( F ` z ) - C ) ) < x ) )
105 92 104 imbi12d 
 |-  ( ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) /\ z e. ( A \ { B } ) ) -> ( ( z e. ( B ( ball ` ( abs o. - ) ) y ) -> ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) ) <-> ( ( abs ` ( z - B ) ) < y -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
106 105 ralbidva 
 |-  ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) -> ( A. z e. ( A \ { B } ) ( z e. ( B ( ball ` ( abs o. - ) ) y ) -> ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) ) <-> A. z e. ( A \ { B } ) ( ( abs ` ( z - B ) ) < y -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
107 elin 
 |-  ( z e. ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) <-> ( z e. ( B ( ball ` ( abs o. - ) ) y ) /\ z e. ( A \ { B } ) ) )
108 107 biancomi 
 |-  ( z e. ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) <-> ( z e. ( A \ { B } ) /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) )
109 108 imbi1i 
 |-  ( ( z e. ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) -> ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) ) <-> ( ( z e. ( A \ { B } ) /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) ) )
110 impexp 
 |-  ( ( ( z e. ( A \ { B } ) /\ z e. ( B ( ball ` ( abs o. - ) ) y ) ) -> ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) ) <-> ( z e. ( A \ { B } ) -> ( z e. ( B ( ball ` ( abs o. - ) ) y ) -> ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) ) ) )
111 109 110 bitr2i 
 |-  ( ( z e. ( A \ { B } ) -> ( z e. ( B ( ball ` ( abs o. - ) ) y ) -> ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) ) ) <-> ( z e. ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) -> ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) ) )
112 111 ralbii2 
 |-  ( A. z e. ( A \ { B } ) ( z e. ( B ( ball ` ( abs o. - ) ) y ) -> ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) ) <-> A. z e. ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) )
113 impexp 
 |-  ( ( ( z e. A /\ z =/= B ) -> ( ( abs ` ( z - B ) ) < y -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) <-> ( z e. A -> ( z =/= B -> ( ( abs ` ( z - B ) ) < y -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) )
114 eldifsn 
 |-  ( z e. ( A \ { B } ) <-> ( z e. A /\ z =/= B ) )
115 114 imbi1i 
 |-  ( ( z e. ( A \ { B } ) -> ( ( abs ` ( z - B ) ) < y -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) <-> ( ( z e. A /\ z =/= B ) -> ( ( abs ` ( z - B ) ) < y -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
116 impexp 
 |-  ( ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) <-> ( z =/= B -> ( ( abs ` ( z - B ) ) < y -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
117 116 imbi2i 
 |-  ( ( z e. A -> ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) <-> ( z e. A -> ( z =/= B -> ( ( abs ` ( z - B ) ) < y -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) )
118 113 115 117 3bitr4i 
 |-  ( ( z e. ( A \ { B } ) -> ( ( abs ` ( z - B ) ) < y -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) <-> ( z e. A -> ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
119 118 ralbii2 
 |-  ( A. z e. ( A \ { B } ) ( ( abs ` ( z - B ) ) < y -> ( abs ` ( ( F ` z ) - C ) ) < x ) <-> A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) )
120 106 112 119 3bitr3g 
 |-  ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) -> ( A. z e. ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ( F ` z ) e. ( C ( ball ` ( abs o. - ) ) x ) <-> A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
121 78 120 bitrd 
 |-  ( ( ( ph /\ C e. CC ) /\ ( x e. RR+ /\ y e. RR+ ) ) -> ( ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) <-> A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
122 121 anassrs 
 |-  ( ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) /\ y e. RR+ ) -> ( ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) <-> A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
123 122 rexbidva 
 |-  ( ( ( ph /\ C e. CC ) /\ x e. RR+ ) -> ( E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) <-> E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
124 123 ralbidva 
 |-  ( ( ph /\ C e. CC ) -> ( A. x e. RR+ E. y e. RR+ ( F " ( ( B ( ball ` ( abs o. - ) ) y ) i^i ( A \ { B } ) ) ) C_ ( C ( ball ` ( abs o. - ) ) x ) <-> A. x e. RR+ E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
125 69 124 bitrd 
 |-  ( ( ph /\ C e. CC ) -> ( A. u e. ( TopOpen ` CCfld ) ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) <-> A. x e. RR+ E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) )
126 125 pm5.32da 
 |-  ( ph -> ( ( C e. CC /\ A. u e. ( TopOpen ` CCfld ) ( C e. u -> E. v e. ( TopOpen ` CCfld ) ( B e. v /\ ( F " ( v i^i ( A \ { B } ) ) ) C_ u ) ) ) <-> ( C e. CC /\ A. x e. RR+ E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) )
127 5 126 bitrd 
 |-  ( ph -> ( C e. ( F limCC B ) <-> ( C e. CC /\ A. x e. RR+ E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) )