This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )