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 = norm CV U
nmoubi.m M = norm CV W
nmoubi.3 N = U normOp OLD W
nmoubi.u U NrmCVec
nmoubi.w W NrmCVec
Assertion nmobndseqiALT T : X Y f f : X k L f k 1 k M T f k k N T

Proof

Step Hyp Ref Expression
1 nmoubi.1 X = BaseSet U
2 nmoubi.y Y = BaseSet W
3 nmoubi.l L = norm CV U
4 nmoubi.m M = norm CV W
5 nmoubi.3 N = U normOp OLD W
6 nmoubi.u U NrmCVec
7 nmoubi.w W NrmCVec
8 impexp f : X k L f k 1 k M T f k k f : X k L f k 1 k M T f k k
9 r19.35 k L f k 1 M T f k k k L f k 1 k M T f k k
10 9 imbi2i f : X k L f k 1 M T f k k f : X k L f k 1 k M T f k k
11 8 10 bitr4i f : X k L f k 1 k M T f k k f : X k L f k 1 M T f k k
12 11 albii f f : X k L f k 1 k M T f k k f f : X k L f k 1 M T f k k
13 nnex 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 f f : X k L f k 1 M T f k k k y X L y 1 M T y k
21 nnre k k
22 21 anim1i k y X L y 1 M T y k k y X L y 1 M T y k
23 22 reximi2 k y X L y 1 M T y k k y X L y 1 M T y k
24 20 23 syl f f : X k L f k 1 M T f k k k y X L y 1 M T y k
25 12 24 sylbi f f : X k L f k 1 k M T f k k k y X L y 1 M T y k
26 1 2 3 4 5 6 7 nmobndi T : X Y N T k y X L y 1 M T y k
27 25 26 syl5ibr T : X Y f f : X k L f k 1 k M T f k k N T
28 27 imp T : X Y f f : X k L f k 1 k M T f k k N T