Metamath Proof Explorer

Theorem nmfnsetn0

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

Ref Expression
Assertion nmfnsetn0 
|- ( abs ` ( T ` 0h ) ) e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) }

Proof

Step Hyp Ref Expression
1 ax-hv0cl 
 |-  0h e. ~H
2 norm0 
 |-  ( normh ` 0h ) = 0
3 0le1 
 |-  0 <_ 1
4 2 3 eqbrtri 
 |-  ( normh ` 0h ) <_ 1
5 eqid 
 |-  ( abs ` ( T ` 0h ) ) = ( abs ` ( T ` 0h ) )
6 4 5 pm3.2i 
 |-  ( ( normh ` 0h ) <_ 1 /\ ( abs ` ( T ` 0h ) ) = ( abs ` ( T ` 0h ) ) )
7 fveq2 
 |-  ( y = 0h -> ( normh ` y ) = ( normh ` 0h ) )
8 7 breq1d 
 |-  ( y = 0h -> ( ( normh ` y ) <_ 1 <-> ( normh ` 0h ) <_ 1 ) )
9 2fveq3 
 |-  ( y = 0h -> ( abs ` ( T ` y ) ) = ( abs ` ( T ` 0h ) ) )
10 9 eqeq2d 
 |-  ( y = 0h -> ( ( abs ` ( T ` 0h ) ) = ( abs ` ( T ` y ) ) <-> ( abs ` ( T ` 0h ) ) = ( abs ` ( T ` 0h ) ) ) )
11 8 10 anbi12d 
 |-  ( y = 0h -> ( ( ( normh ` y ) <_ 1 /\ ( abs ` ( T ` 0h ) ) = ( abs ` ( T ` y ) ) ) <-> ( ( normh ` 0h ) <_ 1 /\ ( abs ` ( T ` 0h ) ) = ( abs ` ( T ` 0h ) ) ) ) )
12 11 rspcev 
 |-  ( ( 0h e. ~H /\ ( ( normh ` 0h ) <_ 1 /\ ( abs ` ( T ` 0h ) ) = ( abs ` ( T ` 0h ) ) ) ) -> E. y e. ~H ( ( normh ` y ) <_ 1 /\ ( abs ` ( T ` 0h ) ) = ( abs ` ( T ` y ) ) ) )
13 1 6 12 mp2an 
 |-  E. y e. ~H ( ( normh ` y ) <_ 1 /\ ( abs ` ( T ` 0h ) ) = ( abs ` ( T ` y ) ) )
14 fvex 
 |-  ( abs ` ( T ` 0h ) ) e. _V
15 eqeq1 
 |-  ( x = ( abs ` ( T ` 0h ) ) -> ( x = ( abs ` ( T ` y ) ) <-> ( abs ` ( T ` 0h ) ) = ( abs ` ( T ` y ) ) ) )
16 15 anbi2d 
 |-  ( x = ( abs ` ( T ` 0h ) ) -> ( ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) <-> ( ( normh ` y ) <_ 1 /\ ( abs ` ( T ` 0h ) ) = ( abs ` ( T ` y ) ) ) ) )
17 16 rexbidv 
 |-  ( x = ( abs ` ( T ` 0h ) ) -> ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ ( abs ` ( T ` 0h ) ) = ( abs ` ( T ` y ) ) ) ) )
18 14 17 elab 
 |-  ( ( abs ` ( T ` 0h ) ) e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) } <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ ( abs ` ( T ` 0h ) ) = ( abs ` ( T ` y ) ) ) )
19 13 18 mpbir 
 |-  ( abs ` ( T ` 0h ) ) e. { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( T ` y ) ) ) }