# 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 ) ) )`