Metamath Proof Explorer

Theorem rlim2

Description: Rewrite rlim for a mapping operation. (Contributed by Mario Carneiro, 16-Sep-2014) (Revised by Mario Carneiro, 28-Feb-2015)

Ref Expression
Hypotheses rlim2.1 
|- ( ph -> A. z e. A B e. CC )
rlim2.2 
|- ( ph -> A C_ RR )
rlim2.3 
|- ( ph -> C e. CC )
Assertion rlim2 
|- ( ph -> ( ( z e. A |-> B ) ~~>r C <-> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )

Proof

Step Hyp Ref Expression
1 rlim2.1 
 |-  ( ph -> A. z e. A B e. CC )
2 rlim2.2 
 |-  ( ph -> A C_ RR )
3 rlim2.3 
 |-  ( ph -> C e. CC )
4 eqid 
 |-  ( z e. A |-> B ) = ( z e. A |-> B )
5 4 fmpt 
 |-  ( A. z e. A B e. CC <-> ( z e. A |-> B ) : A --> CC )
6 1 5 sylib 
 |-  ( ph -> ( z e. A |-> B ) : A --> CC )
7 eqidd 
 |-  ( ( ph /\ w e. A ) -> ( ( z e. A |-> B ) ` w ) = ( ( z e. A |-> B ) ` w ) )
8 6 2 7 rlim 
 |-  ( ph -> ( ( z e. A |-> B ) ~~>r C <-> ( C e. CC /\ A. x e. RR+ E. y e. RR A. w e. A ( y <_ w -> ( abs ` ( ( ( z e. A |-> B ) ` w ) - C ) ) < x ) ) ) )
9 3 biantrurd 
 |-  ( ph -> ( A. x e. RR+ E. y e. RR A. w e. A ( y <_ w -> ( abs ` ( ( ( z e. A |-> B ) ` w ) - C ) ) < x ) <-> ( C e. CC /\ A. x e. RR+ E. y e. RR A. w e. A ( y <_ w -> ( abs ` ( ( ( z e. A |-> B ) ` w ) - C ) ) < x ) ) ) )
10 nfv 
 |-  F/ z y <_ w
11 nfcv 
 |-  F/_ z abs
12 nffvmpt1 
 |-  F/_ z ( ( z e. A |-> B ) ` w )
13 nfcv 
 |-  F/_ z -
14 nfcv 
 |-  F/_ z C
15 12 13 14 nfov 
 |-  F/_ z ( ( ( z e. A |-> B ) ` w ) - C )
16 11 15 nffv 
 |-  F/_ z ( abs ` ( ( ( z e. A |-> B ) ` w ) - C ) )
17 nfcv 
 |-  F/_ z <
18 nfcv 
 |-  F/_ z x
19 16 17 18 nfbr 
 |-  F/ z ( abs ` ( ( ( z e. A |-> B ) ` w ) - C ) ) < x
20 10 19 nfim 
 |-  F/ z ( y <_ w -> ( abs ` ( ( ( z e. A |-> B ) ` w ) - C ) ) < x )
21 nfv 
 |-  F/ w ( y <_ z -> ( abs ` ( ( ( z e. A |-> B ) ` z ) - C ) ) < x )
22 breq2 
 |-  ( w = z -> ( y <_ w <-> y <_ z ) )
23 22 imbrov2fvoveq 
 |-  ( w = z -> ( ( y <_ w -> ( abs ` ( ( ( z e. A |-> B ) ` w ) - C ) ) < x ) <-> ( y <_ z -> ( abs ` ( ( ( z e. A |-> B ) ` z ) - C ) ) < x ) ) )
24 20 21 23 cbvralw 
 |-  ( A. w e. A ( y <_ w -> ( abs ` ( ( ( z e. A |-> B ) ` w ) - C ) ) < x ) <-> A. z e. A ( y <_ z -> ( abs ` ( ( ( z e. A |-> B ) ` z ) - C ) ) < x ) )
25 4 fvmpt2 
 |-  ( ( z e. A /\ B e. CC ) -> ( ( z e. A |-> B ) ` z ) = B )
26 25 fvoveq1d 
 |-  ( ( z e. A /\ B e. CC ) -> ( abs ` ( ( ( z e. A |-> B ) ` z ) - C ) ) = ( abs ` ( B - C ) ) )
27 26 breq1d 
 |-  ( ( z e. A /\ B e. CC ) -> ( ( abs ` ( ( ( z e. A |-> B ) ` z ) - C ) ) < x <-> ( abs ` ( B - C ) ) < x ) )
28 27 imbi2d 
 |-  ( ( z e. A /\ B e. CC ) -> ( ( y <_ z -> ( abs ` ( ( ( z e. A |-> B ) ` z ) - C ) ) < x ) <-> ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
29 28 ralimiaa 
 |-  ( A. z e. A B e. CC -> A. z e. A ( ( y <_ z -> ( abs ` ( ( ( z e. A |-> B ) ` z ) - C ) ) < x ) <-> ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
30 ralbi 
 |-  ( A. z e. A ( ( y <_ z -> ( abs ` ( ( ( z e. A |-> B ) ` z ) - C ) ) < x ) <-> ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) -> ( A. z e. A ( y <_ z -> ( abs ` ( ( ( z e. A |-> B ) ` z ) - C ) ) < x ) <-> A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
31 1 29 30 3syl 
 |-  ( ph -> ( A. z e. A ( y <_ z -> ( abs ` ( ( ( z e. A |-> B ) ` z ) - C ) ) < x ) <-> A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
32 24 31 syl5bb 
 |-  ( ph -> ( A. w e. A ( y <_ w -> ( abs ` ( ( ( z e. A |-> B ) ` w ) - C ) ) < x ) <-> A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
33 32 rexbidv 
 |-  ( ph -> ( E. y e. RR A. w e. A ( y <_ w -> ( abs ` ( ( ( z e. A |-> B ) ` w ) - C ) ) < x ) <-> E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
34 33 ralbidv 
 |-  ( ph -> ( A. x e. RR+ E. y e. RR A. w e. A ( y <_ w -> ( abs ` ( ( ( z e. A |-> B ) ` w ) - C ) ) < x ) <-> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )
35 8 9 34 3bitr2d 
 |-  ( ph -> ( ( z e. A |-> B ) ~~>r C <-> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) )