Theorem nmfnsetre

Description: The set in the supremum of the functional norm definition df-nmfn is a set of reals. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmfnsetre	|- ( T : ~H --> CC -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } C_ RR )

Proof

Step	Hyp	Ref	Expression
1		ffvelcdm	|- ( ( T : ~H --> CC /\ y e. ~H ) -> ( T ` y ) e. CC )
2	1	abscld	|- ( ( T : ~H --> CC /\ y e. ~H ) -> ( abs ` ( T ` y ) ) e. RR )
3		eleq1	|- ( x = ( abs ` ( T ` y ) ) -> ( x e. RR <-> ( abs ` ( T ` y ) ) e. RR ) )
4	2 3	imbitrrid	|- ( x = ( abs ` ( T ` y ) ) -> ( ( T : ~H --> CC /\ y e. ~H ) -> x e. RR ) )
5	4	impcom	|- ( ( ( T : ~H --> CC /\ y e. ~H ) /\ x = ( abs ` ( T ` y ) ) ) -> x e. RR )
6	5	adantrl	|- ( ( ( T : ~H --> CC /\ y e. ~H ) /\ ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) ) -> x e. RR )
7	6	rexlimdva2	|- ( T : ~H --> CC -> ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) -> x e. RR ) )
8	7	abssdv	|- ( T : ~H --> CC -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } C_ RR )