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