Metamath Proof Explorer


Theorem rlimcn3

Description: Image of a limit under a continuous map, two-arg version. Originally a subproof of rlimcn2 . (Contributed by SN, 27-Sep-2024)

Ref Expression
Hypotheses rlimcn3.1a
|- ( ( ph /\ z e. A ) -> B e. X )
rlimcn3.1b
|- ( ( ph /\ z e. A ) -> C e. Y )
rlimcn3.1c
|- ( ( ph /\ z e. A ) -> ( B F C ) e. CC )
rlimcn3.2
|- ( ph -> ( R F S ) e. CC )
rlimcn3.3a
|- ( ph -> ( z e. A |-> B ) ~~>r R )
rlimcn3.3b
|- ( ph -> ( z e. A |-> C ) ~~>r S )
rlimcn3.4
|- ( ( ph /\ x e. RR+ ) -> E. r e. RR+ E. s e. RR+ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) )
Assertion rlimcn3
|- ( ph -> ( z e. A |-> ( B F C ) ) ~~>r ( R F S ) )

Proof

Step Hyp Ref Expression
1 rlimcn3.1a
 |-  ( ( ph /\ z e. A ) -> B e. X )
2 rlimcn3.1b
 |-  ( ( ph /\ z e. A ) -> C e. Y )
3 rlimcn3.1c
 |-  ( ( ph /\ z e. A ) -> ( B F C ) e. CC )
4 rlimcn3.2
 |-  ( ph -> ( R F S ) e. CC )
5 rlimcn3.3a
 |-  ( ph -> ( z e. A |-> B ) ~~>r R )
6 rlimcn3.3b
 |-  ( ph -> ( z e. A |-> C ) ~~>r S )
7 rlimcn3.4
 |-  ( ( ph /\ x e. RR+ ) -> E. r e. RR+ E. s e. RR+ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) )
8 1 ralrimiva
 |-  ( ph -> A. z e. A B e. X )
9 8 adantr
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> A. z e. A B e. X )
10 simprl
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> r e. RR+ )
11 5 adantr
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> ( z e. A |-> B ) ~~>r R )
12 9 10 11 rlimi
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> E. a e. RR A. z e. A ( a <_ z -> ( abs ` ( B - R ) ) < r ) )
13 2 ralrimiva
 |-  ( ph -> A. z e. A C e. Y )
14 13 adantr
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> A. z e. A C e. Y )
15 simprr
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> s e. RR+ )
16 6 adantr
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> ( z e. A |-> C ) ~~>r S )
17 14 15 16 rlimi
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> E. b e. RR A. z e. A ( b <_ z -> ( abs ` ( C - S ) ) < s ) )
18 reeanv
 |-  ( E. a e. RR E. b e. RR ( A. z e. A ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ A. z e. A ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) <-> ( E. a e. RR A. z e. A ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ E. b e. RR A. z e. A ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) )
19 r19.26
 |-  ( A. z e. A ( ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) <-> ( A. z e. A ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ A. z e. A ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) )
20 anim12
 |-  ( ( ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) -> ( ( a <_ z /\ b <_ z ) -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) )
21 simplrl
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ z e. A ) -> a e. RR )
22 simplrr
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ z e. A ) -> b e. RR )
23 eqid
 |-  ( z e. A |-> B ) = ( z e. A |-> B )
24 23 1 dmmptd
 |-  ( ph -> dom ( z e. A |-> B ) = A )
25 rlimss
 |-  ( ( z e. A |-> B ) ~~>r R -> dom ( z e. A |-> B ) C_ RR )
26 5 25 syl
 |-  ( ph -> dom ( z e. A |-> B ) C_ RR )
27 24 26 eqsstrrd
 |-  ( ph -> A C_ RR )
28 27 ad2antrr
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) -> A C_ RR )
29 28 sselda
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ z e. A ) -> z e. RR )
30 maxle
 |-  ( ( a e. RR /\ b e. RR /\ z e. RR ) -> ( if ( a <_ b , b , a ) <_ z <-> ( a <_ z /\ b <_ z ) ) )
31 21 22 29 30 syl3anc
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ z e. A ) -> ( if ( a <_ b , b , a ) <_ z <-> ( a <_ z /\ b <_ z ) ) )
32 31 imbi1d
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ z e. A ) -> ( ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) <-> ( ( a <_ z /\ b <_ z ) -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) ) )
33 20 32 syl5ibr
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ z e. A ) -> ( ( ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) -> ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) ) )
34 33 ralimdva
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) -> ( A. z e. A ( ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) -> A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) ) )
35 ifcl
 |-  ( ( b e. RR /\ a e. RR ) -> if ( a <_ b , b , a ) e. RR )
36 35 ancoms
 |-  ( ( a e. RR /\ b e. RR ) -> if ( a <_ b , b , a ) e. RR )
37 36 ad2antlr
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> if ( a <_ b , b , a ) e. RR )
38 1 adantlr
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ z e. A ) -> B e. X )
39 2 adantlr
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ z e. A ) -> C e. Y )
40 38 39 jca
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ z e. A ) -> ( B e. X /\ C e. Y ) )
41 fvoveq1
 |-  ( u = B -> ( abs ` ( u - R ) ) = ( abs ` ( B - R ) ) )
42 41 breq1d
 |-  ( u = B -> ( ( abs ` ( u - R ) ) < r <-> ( abs ` ( B - R ) ) < r ) )
43 42 anbi1d
 |-  ( u = B -> ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) <-> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) ) )
44 oveq1
 |-  ( u = B -> ( u F v ) = ( B F v ) )
45 44 fvoveq1d
 |-  ( u = B -> ( abs ` ( ( u F v ) - ( R F S ) ) ) = ( abs ` ( ( B F v ) - ( R F S ) ) ) )
46 45 breq1d
 |-  ( u = B -> ( ( abs ` ( ( u F v ) - ( R F S ) ) ) < x <-> ( abs ` ( ( B F v ) - ( R F S ) ) ) < x ) )
47 43 46 imbi12d
 |-  ( u = B -> ( ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) <-> ( ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( B F v ) - ( R F S ) ) ) < x ) ) )
48 fvoveq1
 |-  ( v = C -> ( abs ` ( v - S ) ) = ( abs ` ( C - S ) ) )
49 48 breq1d
 |-  ( v = C -> ( ( abs ` ( v - S ) ) < s <-> ( abs ` ( C - S ) ) < s ) )
50 49 anbi2d
 |-  ( v = C -> ( ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) <-> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) )
51 oveq2
 |-  ( v = C -> ( B F v ) = ( B F C ) )
52 51 fvoveq1d
 |-  ( v = C -> ( abs ` ( ( B F v ) - ( R F S ) ) ) = ( abs ` ( ( B F C ) - ( R F S ) ) ) )
53 52 breq1d
 |-  ( v = C -> ( ( abs ` ( ( B F v ) - ( R F S ) ) ) < x <-> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) )
54 50 53 imbi12d
 |-  ( v = C -> ( ( ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( B F v ) - ( R F S ) ) ) < x ) <-> ( ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
55 47 54 rspc2va
 |-  ( ( ( B e. X /\ C e. Y ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> ( ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) )
56 40 55 sylan
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ z e. A ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> ( ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) )
57 56 imim2d
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ z e. A ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> ( ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) -> ( if ( a <_ b , b , a ) <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
58 57 an32s
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) /\ z e. A ) -> ( ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) -> ( if ( a <_ b , b , a ) <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
59 58 ralimdva
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> ( A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) -> A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
60 59 adantlr
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> ( A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) -> A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
61 breq1
 |-  ( c = if ( a <_ b , b , a ) -> ( c <_ z <-> if ( a <_ b , b , a ) <_ z ) )
62 61 rspceaimv
 |-  ( ( if ( a <_ b , b , a ) e. RR /\ A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) )
63 37 60 62 syl6an
 |-  ( ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) /\ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> ( A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
64 63 ex
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) -> ( A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> ( A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) ) )
65 64 com23
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) -> ( A. z e. A ( if ( a <_ b , b , a ) <_ z -> ( ( abs ` ( B - R ) ) < r /\ ( abs ` ( C - S ) ) < s ) ) -> ( A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) ) )
66 34 65 syld
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) -> ( A. z e. A ( ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) -> ( A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) ) )
67 19 66 syl5bir
 |-  ( ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) /\ ( a e. RR /\ b e. RR ) ) -> ( ( A. z e. A ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ A. z e. A ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) -> ( A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) ) )
68 67 rexlimdvva
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> ( E. a e. RR E. b e. RR ( A. z e. A ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ A. z e. A ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) -> ( A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) ) )
69 18 68 syl5bir
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> ( ( E. a e. RR A. z e. A ( a <_ z -> ( abs ` ( B - R ) ) < r ) /\ E. b e. RR A. z e. A ( b <_ z -> ( abs ` ( C - S ) ) < s ) ) -> ( A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) ) )
70 12 17 69 mp2and
 |-  ( ( ph /\ ( r e. RR+ /\ s e. RR+ ) ) -> ( A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
71 70 rexlimdvva
 |-  ( ph -> ( E. r e. RR+ E. s e. RR+ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
72 71 imp
 |-  ( ( ph /\ E. r e. RR+ E. s e. RR+ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) )
73 7 72 syldan
 |-  ( ( ph /\ x e. RR+ ) -> E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) )
74 73 ralrimiva
 |-  ( ph -> A. x e. RR+ E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) )
75 3 ralrimiva
 |-  ( ph -> A. z e. A ( B F C ) e. CC )
76 75 27 4 rlim2
 |-  ( ph -> ( ( z e. A |-> ( B F C ) ) ~~>r ( R F S ) <-> A. x e. RR+ E. c e. RR A. z e. A ( c <_ z -> ( abs ` ( ( B F C ) - ( R F S ) ) ) < x ) ) )
77 74 76 mpbird
 |-  ( ph -> ( z e. A |-> ( B F C ) ) ~~>r ( R F S ) )