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

Metamath Proof Explorer

Theorem nmounbi

Description: Two ways two express that an operator is unbounded. (Contributed by NM, 11-Jan-2008) (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 nmounbi 
|- ( T : X --> Y -> ( ( N ` T ) = +oo <-> A. r e. RR E. y e. X ( ( L ` y ) <_ 1 /\ r < ( M ` ( T ` y ) ) ) ) )

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 nmobndi 
 |-  ( T : X --> Y -> ( ( N ` T ) e. RR <-> E. r e. RR A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ r ) ) )
9 1 2 5 nmorepnf 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( N ` T ) e. RR <-> ( N ` T ) =/= +oo ) )
10 6 7 9 mp3an12 
 |-  ( T : X --> Y -> ( ( N ` T ) e. RR <-> ( N ` T ) =/= +oo ) )
11 ffvelcdm 
 |-  ( ( T : X --> Y /\ y e. X ) -> ( T ` y ) e. Y )
12 2 4 nvcl 
 |-  ( ( W e. NrmCVec /\ ( T ` y ) e. Y ) -> ( M ` ( T ` y ) ) e. RR )
13 7 11 12 sylancr 
 |-  ( ( T : X --> Y /\ y e. X ) -> ( M ` ( T ` y ) ) e. RR )
14 lenlt 
 |-  ( ( ( M ` ( T ` y ) ) e. RR /\ r e. RR ) -> ( ( M ` ( T ` y ) ) <_ r <-> -. r < ( M ` ( T ` y ) ) ) )
15 13 14 sylan 
 |-  ( ( ( T : X --> Y /\ y e. X ) /\ r e. RR ) -> ( ( M ` ( T ` y ) ) <_ r <-> -. r < ( M ` ( T ` y ) ) ) )
16 15 an32s 
 |-  ( ( ( T : X --> Y /\ r e. RR ) /\ y e. X ) -> ( ( M ` ( T ` y ) ) <_ r <-> -. r < ( M ` ( T ` y ) ) ) )
17 16 imbi2d 
 |-  ( ( ( T : X --> Y /\ r e. RR ) /\ y e. X ) -> ( ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ r ) <-> ( ( L ` y ) <_ 1 -> -. r < ( M ` ( T ` y ) ) ) ) )
18 imnan 
 |-  ( ( ( L ` y ) <_ 1 -> -. r < ( M ` ( T ` y ) ) ) <-> -. ( ( L ` y ) <_ 1 /\ r < ( M ` ( T ` y ) ) ) )
19 17 18 bitrdi 
 |-  ( ( ( T : X --> Y /\ r e. RR ) /\ y e. X ) -> ( ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ r ) <-> -. ( ( L ` y ) <_ 1 /\ r < ( M ` ( T ` y ) ) ) ) )
20 19 ralbidva 
 |-  ( ( T : X --> Y /\ r e. RR ) -> ( A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ r ) <-> A. y e. X -. ( ( L ` y ) <_ 1 /\ r < ( M ` ( T ` y ) ) ) ) )
21 ralnex 
 |-  ( A. y e. X -. ( ( L ` y ) <_ 1 /\ r < ( M ` ( T ` y ) ) ) <-> -. E. y e. X ( ( L ` y ) <_ 1 /\ r < ( M ` ( T ` y ) ) ) )
22 20 21 bitrdi 
 |-  ( ( T : X --> Y /\ r e. RR ) -> ( A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ r ) <-> -. E. y e. X ( ( L ` y ) <_ 1 /\ r < ( M ` ( T ` y ) ) ) ) )
23 22 rexbidva 
 |-  ( T : X --> Y -> ( E. r e. RR A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ r ) <-> E. r e. RR -. E. y e. X ( ( L ` y ) <_ 1 /\ r < ( M ` ( T ` y ) ) ) ) )
24 rexnal 
 |-  ( E. r e. RR -. E. y e. X ( ( L ` y ) <_ 1 /\ r < ( M ` ( T ` y ) ) ) <-> -. A. r e. RR E. y e. X ( ( L ` y ) <_ 1 /\ r < ( M ` ( T ` y ) ) ) )
25 23 24 bitrdi 
 |-  ( T : X --> Y -> ( E. r e. RR A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ r ) <-> -. A. r e. RR E. y e. X ( ( L ` y ) <_ 1 /\ r < ( M ` ( T ` y ) ) ) ) )
26 8 10 25 3bitr3d 
 |-  ( T : X --> Y -> ( ( N ` T ) =/= +oo <-> -. A. r e. RR E. y e. X ( ( L ` y ) <_ 1 /\ r < ( M ` ( T ` y ) ) ) ) )
27 26 necon4abid 
 |-  ( T : X --> Y -> ( ( N ` T ) = +oo <-> A. r e. RR E. y e. X ( ( L ` y ) <_ 1 /\ r < ( M ` ( T ` y ) ) ) ) )