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

Metamath Proof Explorer

Theorem nmounbseqi

Description: An unbounded operator determines an unbounded sequence. (Contributed by NM, 11-Jan-2008) (Revised by Mario Carneiro, 7-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmoubi.1 
|- X = ( BaseSet ` U )
nmoubi.y 
|- Y = ( BaseSet ` W )
nmoubi.l 
|- L = ( normCV ` U )
nmoubi.m 
|- M = ( normCV ` W )
nmoubi.3 
|- N = ( U normOpOLD W )
nmoubi.u 
|- U e. NrmCVec
nmoubi.w 
|- W e. NrmCVec
Assertion nmounbseqi 
|- ( ( T : X --> Y /\ ( N ` T ) = +oo ) -> E. f ( f : NN --> X /\ A. k e. NN ( ( L ` ( f ` k ) ) <_ 1 /\ k < ( M ` ( T ` ( f ` k ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 nmoubi.1 
 |-  X = ( BaseSet ` U )
2 nmoubi.y 
 |-  Y = ( BaseSet ` W )
3 nmoubi.l 
 |-  L = ( normCV ` U )
4 nmoubi.m 
 |-  M = ( normCV ` W )
5 nmoubi.3 
 |-  N = ( U normOpOLD W )
6 nmoubi.u 
 |-  U e. NrmCVec
7 nmoubi.w 
 |-  W e. NrmCVec
8 1 2 3 4 5 6 7 nmounbi 
 |-  ( T : X --> Y -> ( ( N ` T ) = +oo <-> A. k e. RR E. y e. X ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) ) )
9 8 biimpa 
 |-  ( ( T : X --> Y /\ ( N ` T ) = +oo ) -> A. k e. RR E. y e. X ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) )
10 nnre 
 |-  ( k e. NN -> k e. RR )
11 10 imim1i 
 |-  ( ( k e. RR -> E. y e. X ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) ) -> ( k e. NN -> E. y e. X ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) ) )
12 11 ralimi2 
 |-  ( A. k e. RR E. y e. X ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) -> A. k e. NN E. y e. X ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) )
13 1 fvexi 
 |-  X e. _V
14 nnenom 
 |-  NN ~~ _om
15 fveq2 
 |-  ( y = ( f ` k ) -> ( L ` y ) = ( L ` ( f ` k ) ) )
16 15 breq1d 
 |-  ( y = ( f ` k ) -> ( ( L ` y ) <_ 1 <-> ( L ` ( f ` k ) ) <_ 1 ) )
17 2fveq3 
 |-  ( y = ( f ` k ) -> ( M ` ( T ` y ) ) = ( M ` ( T ` ( f ` k ) ) ) )
18 17 breq2d 
 |-  ( y = ( f ` k ) -> ( k < ( M ` ( T ` y ) ) <-> k < ( M ` ( T ` ( f ` k ) ) ) ) )
19 16 18 anbi12d 
 |-  ( y = ( f ` k ) -> ( ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) <-> ( ( L ` ( f ` k ) ) <_ 1 /\ k < ( M ` ( T ` ( f ` k ) ) ) ) ) )
20 13 14 19 axcc4 
 |-  ( A. k e. NN E. y e. X ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) -> E. f ( f : NN --> X /\ A. k e. NN ( ( L ` ( f ` k ) ) <_ 1 /\ k < ( M ` ( T ` ( f ` k ) ) ) ) ) )
21 9 12 20 3syl 
 |-  ( ( T : X --> Y /\ ( N ` T ) = +oo ) -> E. f ( f : NN --> X /\ A. k e. NN ( ( L ` ( f ` k ) ) <_ 1 /\ k < ( M ` ( T ` ( f ` k ) ) ) ) ) )