# Metamath Proof Explorer

## Theorem cnfnc

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

Ref Expression
Assertion cnfnc
`|- ( ( T e. ContFn /\ A e. ~H /\ B e. RR+ ) -> E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` A ) ) ) < B ) )`

### Proof

Step Hyp Ref Expression
1 elcnfn
` |-  ( T e. ContFn <-> ( T : ~H --> CC /\ A. z e. ~H A. w e. RR+ E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h z ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` z ) ) ) < w ) ) )`
2 1 simprbi
` |-  ( T e. ContFn -> A. z e. ~H A. w e. RR+ E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h z ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` z ) ) ) < w ) )`
3 oveq2
` |-  ( z = A -> ( y -h z ) = ( y -h A ) )`
4 3 fveq2d
` |-  ( z = A -> ( normh ` ( y -h z ) ) = ( normh ` ( y -h A ) ) )`
5 4 breq1d
` |-  ( z = A -> ( ( normh ` ( y -h z ) ) < x <-> ( normh ` ( y -h A ) ) < x ) )`
6 fveq2
` |-  ( z = A -> ( T ` z ) = ( T ` A ) )`
7 6 oveq2d
` |-  ( z = A -> ( ( T ` y ) - ( T ` z ) ) = ( ( T ` y ) - ( T ` A ) ) )`
8 7 fveq2d
` |-  ( z = A -> ( abs ` ( ( T ` y ) - ( T ` z ) ) ) = ( abs ` ( ( T ` y ) - ( T ` A ) ) ) )`
9 8 breq1d
` |-  ( z = A -> ( ( abs ` ( ( T ` y ) - ( T ` z ) ) ) < w <-> ( abs ` ( ( T ` y ) - ( T ` A ) ) ) < w ) )`
10 5 9 imbi12d
` |-  ( z = A -> ( ( ( normh ` ( y -h z ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` z ) ) ) < w ) <-> ( ( normh ` ( y -h A ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` A ) ) ) < w ) ) )`
11 10 rexralbidv
` |-  ( z = A -> ( E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h z ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` z ) ) ) < w ) <-> E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` A ) ) ) < w ) ) )`
12 breq2
` |-  ( w = B -> ( ( abs ` ( ( T ` y ) - ( T ` A ) ) ) < w <-> ( abs ` ( ( T ` y ) - ( T ` A ) ) ) < B ) )`
13 12 imbi2d
` |-  ( w = B -> ( ( ( normh ` ( y -h A ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` A ) ) ) < w ) <-> ( ( normh ` ( y -h A ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` A ) ) ) < B ) ) )`
14 13 rexralbidv
` |-  ( w = B -> ( E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` A ) ) ) < w ) <-> E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` A ) ) ) < B ) ) )`
15 11 14 rspc2v
` |-  ( ( A e. ~H /\ B e. RR+ ) -> ( A. z e. ~H A. w e. RR+ E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h z ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` z ) ) ) < w ) -> E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` A ) ) ) < B ) ) )`
16 2 15 syl5com
` |-  ( T e. ContFn -> ( ( A e. ~H /\ B e. RR+ ) -> E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` A ) ) ) < B ) ) )`
17 16 3impib
` |-  ( ( T e. ContFn /\ A e. ~H /\ B e. RR+ ) -> E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( abs ` ( ( T ` y ) - ( T ` A ) ) ) < B ) )`