Metamath Proof Explorer

Theorem cncfi

Description: Defining property of a continuous function. (Contributed by Mario Carneiro, 30-Apr-2014) (Revised by Mario Carneiro, 25-Aug-2014)

Ref Expression
Assertion cncfi 
|- ( ( F e. ( A -cn-> B ) /\ C e. A /\ R e. RR+ ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - C ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` C ) ) ) < R ) )

Proof

Step Hyp Ref Expression
1 cncfrss 
 |-  ( F e. ( A -cn-> B ) -> A C_ CC )
2 cncfrss2 
 |-  ( F e. ( A -cn-> B ) -> B C_ CC )
3 elcncf2 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( F e. ( A -cn-> B ) <-> ( F : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) ) )
4 1 2 3 syl2anc 
 |-  ( F e. ( A -cn-> B ) -> ( F e. ( A -cn-> B ) <-> ( F : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) ) )
5 4 ibi 
 |-  ( F e. ( A -cn-> B ) -> ( F : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) )
6 5 simprd 
 |-  ( F e. ( A -cn-> B ) -> A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) )
7 oveq2 
 |-  ( x = C -> ( w - x ) = ( w - C ) )
8 7 fveq2d 
 |-  ( x = C -> ( abs ` ( w - x ) ) = ( abs ` ( w - C ) ) )
9 8 breq1d 
 |-  ( x = C -> ( ( abs ` ( w - x ) ) < z <-> ( abs ` ( w - C ) ) < z ) )
10 fveq2 
 |-  ( x = C -> ( F ` x ) = ( F ` C ) )
11 10 oveq2d 
 |-  ( x = C -> ( ( F ` w ) - ( F ` x ) ) = ( ( F ` w ) - ( F ` C ) ) )
12 11 fveq2d 
 |-  ( x = C -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) = ( abs ` ( ( F ` w ) - ( F ` C ) ) ) )
13 12 breq1d 
 |-  ( x = C -> ( ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y <-> ( abs ` ( ( F ` w ) - ( F ` C ) ) ) < y ) )
14 9 13 imbi12d 
 |-  ( x = C -> ( ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) <-> ( ( abs ` ( w - C ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` C ) ) ) < y ) ) )
15 14 rexralbidv 
 |-  ( x = C -> ( E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) <-> E. z e. RR+ A. w e. A ( ( abs ` ( w - C ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` C ) ) ) < y ) ) )
16 breq2 
 |-  ( y = R -> ( ( abs ` ( ( F ` w ) - ( F ` C ) ) ) < y <-> ( abs ` ( ( F ` w ) - ( F ` C ) ) ) < R ) )
17 16 imbi2d 
 |-  ( y = R -> ( ( ( abs ` ( w - C ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` C ) ) ) < y ) <-> ( ( abs ` ( w - C ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` C ) ) ) < R ) ) )
18 17 rexralbidv 
 |-  ( y = R -> ( E. z e. RR+ A. w e. A ( ( abs ` ( w - C ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` C ) ) ) < y ) <-> E. z e. RR+ A. w e. A ( ( abs ` ( w - C ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` C ) ) ) < R ) ) )
19 15 18 rspc2v 
 |-  ( ( C e. A /\ R e. RR+ ) -> ( A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - C ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` C ) ) ) < R ) ) )
20 6 19 mpan9 
 |-  ( ( F e. ( A -cn-> B ) /\ ( C e. A /\ R e. RR+ ) ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - C ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` C ) ) ) < R ) )
21 20 3impb 
 |-  ( ( F e. ( A -cn-> B ) /\ C e. A /\ R e. RR+ ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - C ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` C ) ) ) < R ) )