Metamath Proof Explorer

Theorem elcnfn

Description: Property defining a continuous functional. (Contributed by NM, 11-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion elcnfn 
|- ( T e. ContFn <-> ( T : ~H --> CC /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( T ` w ) - ( T ` x ) ) ) < y ) ) )

Proof

Step Hyp Ref Expression
1 fveq1 
 |-  ( t = T -> ( t ` w ) = ( T ` w ) )
2 fveq1 
 |-  ( t = T -> ( t ` x ) = ( T ` x ) )
3 1 2 oveq12d 
 |-  ( t = T -> ( ( t ` w ) - ( t ` x ) ) = ( ( T ` w ) - ( T ` x ) ) )
4 3 fveq2d 
 |-  ( t = T -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) = ( abs ` ( ( T ` w ) - ( T ` x ) ) ) )
5 4 breq1d 
 |-  ( t = T -> ( ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y <-> ( abs ` ( ( T ` w ) - ( T ` x ) ) ) < y ) )
6 5 imbi2d 
 |-  ( t = T -> ( ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) <-> ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( T ` w ) - ( T ` x ) ) ) < y ) ) )
7 6 rexralbidv 
 |-  ( t = T -> ( E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) <-> E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( T ` w ) - ( T ` x ) ) ) < y ) ) )
8 7 2ralbidv 
 |-  ( t = T -> ( A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) <-> A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( T ` w ) - ( T ` x ) ) ) < y ) ) )
9 df-cnfn 
 |-  ContFn = { t e. ( CC ^m ~H ) | A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) }
10 8 9 elrab2 
 |-  ( T e. ContFn <-> ( T e. ( CC ^m ~H ) /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( T ` w ) - ( T ` x ) ) ) < y ) ) )
11 cnex 
 |-  CC e. _V
12 ax-hilex 
 |-  ~H e. _V
13 11 12 elmap 
 |-  ( T e. ( CC ^m ~H ) <-> T : ~H --> CC )
14 13 anbi1i 
 |-  ( ( T e. ( CC ^m ~H ) /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( T ` w ) - ( T ` x ) ) ) < y ) ) <-> ( T : ~H --> CC /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( T ` w ) - ( T ` x ) ) ) < y ) ) )
15 10 14 bitri 
 |-  ( T e. ContFn <-> ( T : ~H --> CC /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( T ` w ) - ( T ` x ) ) ) < y ) ) )