Metamath Proof Explorer

Theorem nmopsetretALT

Description: The set in the supremum of the operator norm definition df-nmop is a set of reals. (Contributed by NM, 2-Feb-2006) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ffvelrn 
 |-  ( ( T : ~H --> ~H /\ y e. ~H ) -> ( T ` y ) e. ~H )
2 normcl 
 |-  ( ( T ` y ) e. ~H -> ( normh ` ( T ` y ) ) e. RR )
3 1 2 syl 
 |-  ( ( T : ~H --> ~H /\ y e. ~H ) -> ( normh ` ( T ` y ) ) e. RR )
4 eleq1 
 |-  ( x = ( normh ` ( T ` y ) ) -> ( x e. RR <-> ( normh ` ( T ` y ) ) e. RR ) )
5 3 4 syl5ibr 
 |-  ( x = ( normh ` ( T ` y ) ) -> ( ( T : ~H --> ~H /\ y e. ~H ) -> x e. RR ) )
6 5 impcom 
 |-  ( ( ( T : ~H --> ~H /\ y e. ~H ) /\ x = ( normh ` ( T ` y ) ) ) -> x e. RR )
7 6 adantrl 
 |-  ( ( ( T : ~H --> ~H /\ y e. ~H ) /\ ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) ) -> x e. RR )
8 7 exp31 
 |-  ( T : ~H --> ~H -> ( y e. ~H -> ( ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) -> x e. RR ) ) )
9 8 rexlimdv 
 |-  ( T : ~H --> ~H -> ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) -> x e. RR ) )
10 9 abssdv 
 |-  ( T : ~H --> ~H -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR )