Metamath Proof Explorer

Theorem nmobndseqiALT

Description: Alternate shorter proof of nmobndseqi based on Axioms ax-reg and ax-ac2 instead of ax-cc . (Contributed by NM, 18-Jan-2008) (New usage is discouraged.) (Proof modification 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 nmobndseqiALT 
|- ( ( T : X --> Y /\ A. f ( ( f : NN --> X /\ A. k e. NN ( L ` ( f ` k ) ) <_ 1 ) -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) -> ( N ` T ) e. RR )

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 impexp 
 |-  ( ( ( f : NN --> X /\ A. k e. NN ( L ` ( f ` k ) ) <_ 1 ) -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) <-> ( f : NN --> X -> ( A. k e. NN ( L ` ( f ` k ) ) <_ 1 -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
9 r19.35 
 |-  ( E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) <-> ( A. k e. NN ( L ` ( f ` k ) ) <_ 1 -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) )
10 9 imbi2i 
 |-  ( ( f : NN --> X -> E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) <-> ( f : NN --> X -> ( A. k e. NN ( L ` ( f ` k ) ) <_ 1 -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
11 8 10 bitr4i 
 |-  ( ( ( f : NN --> X /\ A. k e. NN ( L ` ( f ` k ) ) <_ 1 ) -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) <-> ( f : NN --> X -> E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
12 11 albii 
 |-  ( A. f ( ( f : NN --> X /\ A. k e. NN ( L ` ( f ` k ) ) <_ 1 ) -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) <-> A. f ( f : NN --> X -> E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
13 nnex 
 |-  NN e. _V
14 fveq2 
 |-  ( y = ( f ` k ) -> ( L ` y ) = ( L ` ( f ` k ) ) )
15 14 breq1d 
 |-  ( y = ( f ` k ) -> ( ( L ` y ) <_ 1 <-> ( L ` ( f ` k ) ) <_ 1 ) )
16 fveq2 
 |-  ( y = ( f ` k ) -> ( T ` y ) = ( T ` ( f ` k ) ) )
17 16 fveq2d 
 |-  ( y = ( f ` k ) -> ( M ` ( T ` y ) ) = ( M ` ( T ` ( f ` k ) ) ) )
18 17 breq1d 
 |-  ( y = ( f ` k ) -> ( ( M ` ( T ` y ) ) <_ k <-> ( M ` ( T ` ( f ` k ) ) ) <_ k ) )
19 15 18 imbi12d 
 |-  ( y = ( f ` k ) -> ( ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) <-> ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
20 13 19 ac6n 
 |-  ( A. f ( f : NN --> X -> E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) -> E. k e. NN A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) )
21 nnre 
 |-  ( k e. NN -> k e. RR )
22 21 anim1i 
 |-  ( ( k e. NN /\ A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) ) -> ( k e. RR /\ A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) ) )
23 22 reximi2 
 |-  ( E. k e. NN A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) -> E. k e. RR A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) )
24 20 23 syl 
 |-  ( A. f ( f : NN --> X -> E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) -> E. k e. RR A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) )
25 12 24 sylbi 
 |-  ( A. f ( ( f : NN --> X /\ A. k e. NN ( L ` ( f ` k ) ) <_ 1 ) -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) -> E. k e. RR A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) )
26 1 2 3 4 5 6 7 nmobndi 
 |-  ( T : X --> Y -> ( ( N ` T ) e. RR <-> E. k e. RR A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) ) )
27 25 26 syl5ibr 
 |-  ( T : X --> Y -> ( A. f ( ( f : NN --> X /\ A. k e. NN ( L ` ( f ` k ) ) <_ 1 ) -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) -> ( N ` T ) e. RR ) )
28 27 imp 
 |-  ( ( T : X --> Y /\ A. f ( ( f : NN --> X /\ A. k e. NN ( L ` ( f ` k ) ) <_ 1 ) -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) -> ( N ` T ) e. RR )