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

Metamath Proof Explorer

Theorem ubthlem3

Description: Lemma for ubth . Prove the reverse implication, using nmblolbi . (Contributed by Mario Carneiro, 11-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses ubth.1 
|- X = ( BaseSet ` U )
ubth.2 
|- N = ( normCV ` W )
ubthlem.3 
|- D = ( IndMet ` U )
ubthlem.4 
|- J = ( MetOpen ` D )
ubthlem.5 
|- U e. CBan
ubthlem.6 
|- W e. NrmCVec
ubthlem.7 
|- ( ph -> T C_ ( U BLnOp W ) )
Assertion ubthlem3 
|- ( ph -> ( A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d ) )

Proof

Step Hyp Ref Expression
1 ubth.1 
 |-  X = ( BaseSet ` U )
2 ubth.2 
 |-  N = ( normCV ` W )
3 ubthlem.3 
 |-  D = ( IndMet ` U )
4 ubthlem.4 
 |-  J = ( MetOpen ` D )
5 ubthlem.5 
 |-  U e. CBan
6 ubthlem.6 
 |-  W e. NrmCVec
7 ubthlem.7 
 |-  ( ph -> T C_ ( U BLnOp W ) )
8 fveq1 
 |-  ( u = t -> ( u ` z ) = ( t ` z ) )
9 8 fveq2d 
 |-  ( u = t -> ( N ` ( u ` z ) ) = ( N ` ( t ` z ) ) )
10 9 breq1d 
 |-  ( u = t -> ( ( N ` ( u ` z ) ) <_ d <-> ( N ` ( t ` z ) ) <_ d ) )
11 10 cbvralvw 
 |-  ( A. u e. T ( N ` ( u ` z ) ) <_ d <-> A. t e. T ( N ` ( t ` z ) ) <_ d )
12 breq2 
 |-  ( d = c -> ( ( N ` ( t ` z ) ) <_ d <-> ( N ` ( t ` z ) ) <_ c ) )
13 12 ralbidv 
 |-  ( d = c -> ( A. t e. T ( N ` ( t ` z ) ) <_ d <-> A. t e. T ( N ` ( t ` z ) ) <_ c ) )
14 11 13 bitrid 
 |-  ( d = c -> ( A. u e. T ( N ` ( u ` z ) ) <_ d <-> A. t e. T ( N ` ( t ` z ) ) <_ c ) )
15 14 cbvrexvw 
 |-  ( E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d <-> E. c e. RR A. t e. T ( N ` ( t ` z ) ) <_ c )
16 2fveq3 
 |-  ( z = x -> ( N ` ( t ` z ) ) = ( N ` ( t ` x ) ) )
17 16 breq1d 
 |-  ( z = x -> ( ( N ` ( t ` z ) ) <_ c <-> ( N ` ( t ` x ) ) <_ c ) )
18 17 rexralbidv 
 |-  ( z = x -> ( E. c e. RR A. t e. T ( N ` ( t ` z ) ) <_ c <-> E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c ) )
19 15 18 bitrid 
 |-  ( z = x -> ( E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d <-> E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c ) )
20 19 cbvralvw 
 |-  ( A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d <-> A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c )
21 7 adantr 
 |-  ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) -> T C_ ( U BLnOp W ) )
22 simpr 
 |-  ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) -> A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d )
23 22 20 sylib 
 |-  ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) -> A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c )
24 fveq1 
 |-  ( u = t -> ( u ` d ) = ( t ` d ) )
25 24 fveq2d 
 |-  ( u = t -> ( N ` ( u ` d ) ) = ( N ` ( t ` d ) ) )
26 25 breq1d 
 |-  ( u = t -> ( ( N ` ( u ` d ) ) <_ m <-> ( N ` ( t ` d ) ) <_ m ) )
27 26 cbvralvw 
 |-  ( A. u e. T ( N ` ( u ` d ) ) <_ m <-> A. t e. T ( N ` ( t ` d ) ) <_ m )
28 2fveq3 
 |-  ( d = z -> ( N ` ( t ` d ) ) = ( N ` ( t ` z ) ) )
29 28 breq1d 
 |-  ( d = z -> ( ( N ` ( t ` d ) ) <_ m <-> ( N ` ( t ` z ) ) <_ m ) )
30 29 ralbidv 
 |-  ( d = z -> ( A. t e. T ( N ` ( t ` d ) ) <_ m <-> A. t e. T ( N ` ( t ` z ) ) <_ m ) )
31 27 30 bitrid 
 |-  ( d = z -> ( A. u e. T ( N ` ( u ` d ) ) <_ m <-> A. t e. T ( N ` ( t ` z ) ) <_ m ) )
32 31 cbvrabv 
 |-  { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ m }
33 breq2 
 |-  ( m = k -> ( ( N ` ( t ` z ) ) <_ m <-> ( N ` ( t ` z ) ) <_ k ) )
34 33 ralbidv 
 |-  ( m = k -> ( A. t e. T ( N ` ( t ` z ) ) <_ m <-> A. t e. T ( N ` ( t ` z ) ) <_ k ) )
35 34 rabbidv 
 |-  ( m = k -> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ m } = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
36 32 35 eqtrid 
 |-  ( m = k -> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } = { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
37 36 cbvmptv 
 |-  ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) = ( k e. NN |-> { z e. X | A. t e. T ( N ` ( t ` z ) ) <_ k } )
38 1 2 3 4 5 6 21 23 37 ubthlem1 
 |-  ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) -> E. n e. NN E. y e. X E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) )
39 7 ad3antrrr 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ ( r e. RR+ /\ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) ) ) -> T C_ ( U BLnOp W ) )
40 23 ad2antrr 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ ( r e. RR+ /\ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) ) ) -> A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c )
41 simplrl 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ ( r e. RR+ /\ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) ) ) -> n e. NN )
42 simplrr 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ ( r e. RR+ /\ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) ) ) -> y e. X )
43 simprl 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ ( r e. RR+ /\ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) ) ) -> r e. RR+ )
44 simprr 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ ( r e. RR+ /\ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) ) ) -> { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) )
45 1 2 3 4 5 6 39 40 37 41 42 43 44 ubthlem2 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ ( r e. RR+ /\ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) ) ) -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d )
46 45 expr 
 |-  ( ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) /\ r e. RR+ ) -> ( { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d ) )
47 46 rexlimdva 
 |-  ( ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) /\ ( n e. NN /\ y e. X ) ) -> ( E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d ) )
48 47 rexlimdvva 
 |-  ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) -> ( E. n e. NN E. y e. X E. r e. RR+ { z e. X | ( y D z ) <_ r } C_ ( ( m e. NN |-> { d e. X | A. u e. T ( N ` ( u ` d ) ) <_ m } ) ` n ) -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d ) )
49 38 48 mpd 
 |-  ( ( ph /\ A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d ) -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d )
50 49 ex 
 |-  ( ph -> ( A. z e. X E. d e. RR A. u e. T ( N ` ( u ` z ) ) <_ d -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d ) )
51 20 50 biimtrrid 
 |-  ( ph -> ( A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c -> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d ) )
52 simpr 
 |-  ( ( ph /\ d e. RR ) -> d e. RR )
53 bnnv 
 |-  ( U e. CBan -> U e. NrmCVec )
54 5 53 ax-mp 
 |-  U e. NrmCVec
55 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
56 1 55 nvcl 
 |-  ( ( U e. NrmCVec /\ x e. X ) -> ( ( normCV ` U ) ` x ) e. RR )
57 54 56 mpan 
 |-  ( x e. X -> ( ( normCV ` U ) ` x ) e. RR )
58 remulcl 
 |-  ( ( d e. RR /\ ( ( normCV ` U ) ` x ) e. RR ) -> ( d x. ( ( normCV ` U ) ` x ) ) e. RR )
59 52 57 58 syl2an 
 |-  ( ( ( ph /\ d e. RR ) /\ x e. X ) -> ( d x. ( ( normCV ` U ) ` x ) ) e. RR )
60 7 sselda 
 |-  ( ( ph /\ t e. T ) -> t e. ( U BLnOp W ) )
61 60 adantlr 
 |-  ( ( ( ph /\ d e. RR ) /\ t e. T ) -> t e. ( U BLnOp W ) )
62 61 ad2ant2r 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> t e. ( U BLnOp W ) )
63 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
64 eqid 
 |-  ( U BLnOp W ) = ( U BLnOp W )
65 1 63 64 blof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ t e. ( U BLnOp W ) ) -> t : X --> ( BaseSet ` W ) )
66 54 6 65 mp3an12 
 |-  ( t e. ( U BLnOp W ) -> t : X --> ( BaseSet ` W ) )
67 62 66 syl 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> t : X --> ( BaseSet ` W ) )
68 simplr 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> x e. X )
69 67 68 ffvelcdmd 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( t ` x ) e. ( BaseSet ` W ) )
70 63 2 nvcl 
 |-  ( ( W e. NrmCVec /\ ( t ` x ) e. ( BaseSet ` W ) ) -> ( N ` ( t ` x ) ) e. RR )
71 6 70 mpan 
 |-  ( ( t ` x ) e. ( BaseSet ` W ) -> ( N ` ( t ` x ) ) e. RR )
72 69 71 syl 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( N ` ( t ` x ) ) e. RR )
73 eqid 
 |-  ( U normOpOLD W ) = ( U normOpOLD W )
74 1 63 73 nmoxr 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ t : X --> ( BaseSet ` W ) ) -> ( ( U normOpOLD W ) ` t ) e. RR* )
75 54 6 74 mp3an12 
 |-  ( t : X --> ( BaseSet ` W ) -> ( ( U normOpOLD W ) ` t ) e. RR* )
76 67 75 syl 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( U normOpOLD W ) ` t ) e. RR* )
77 simpllr 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> d e. RR )
78 1 63 73 nmogtmnf 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ t : X --> ( BaseSet ` W ) ) -> -oo < ( ( U normOpOLD W ) ` t ) )
79 54 6 78 mp3an12 
 |-  ( t : X --> ( BaseSet ` W ) -> -oo < ( ( U normOpOLD W ) ` t ) )
80 67 79 syl 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> -oo < ( ( U normOpOLD W ) ` t ) )
81 simprr 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( U normOpOLD W ) ` t ) <_ d )
82 xrre 
 |-  ( ( ( ( ( U normOpOLD W ) ` t ) e. RR* /\ d e. RR ) /\ ( -oo < ( ( U normOpOLD W ) ` t ) /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( U normOpOLD W ) ` t ) e. RR )
83 76 77 80 81 82 syl22anc 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( U normOpOLD W ) ` t ) e. RR )
84 57 ad2antlr 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( normCV ` U ) ` x ) e. RR )
85 remulcl 
 |-  ( ( ( ( U normOpOLD W ) ` t ) e. RR /\ ( ( normCV ` U ) ` x ) e. RR ) -> ( ( ( U normOpOLD W ) ` t ) x. ( ( normCV ` U ) ` x ) ) e. RR )
86 83 84 85 syl2anc 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( ( U normOpOLD W ) ` t ) x. ( ( normCV ` U ) ` x ) ) e. RR )
87 59 adantr 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( d x. ( ( normCV ` U ) ` x ) ) e. RR )
88 1 55 2 73 64 54 6 nmblolbi 
 |-  ( ( t e. ( U BLnOp W ) /\ x e. X ) -> ( N ` ( t ` x ) ) <_ ( ( ( U normOpOLD W ) ` t ) x. ( ( normCV ` U ) ` x ) ) )
89 62 68 88 syl2anc 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( N ` ( t ` x ) ) <_ ( ( ( U normOpOLD W ) ` t ) x. ( ( normCV ` U ) ` x ) ) )
90 1 55 nvge0 
 |-  ( ( U e. NrmCVec /\ x e. X ) -> 0 <_ ( ( normCV ` U ) ` x ) )
91 54 90 mpan 
 |-  ( x e. X -> 0 <_ ( ( normCV ` U ) ` x ) )
92 57 91 jca 
 |-  ( x e. X -> ( ( ( normCV ` U ) ` x ) e. RR /\ 0 <_ ( ( normCV ` U ) ` x ) ) )
93 92 ad2antlr 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( ( normCV ` U ) ` x ) e. RR /\ 0 <_ ( ( normCV ` U ) ` x ) ) )
94 lemul1a 
 |-  ( ( ( ( ( U normOpOLD W ) ` t ) e. RR /\ d e. RR /\ ( ( ( normCV ` U ) ` x ) e. RR /\ 0 <_ ( ( normCV ` U ) ` x ) ) ) /\ ( ( U normOpOLD W ) ` t ) <_ d ) -> ( ( ( U normOpOLD W ) ` t ) x. ( ( normCV ` U ) ` x ) ) <_ ( d x. ( ( normCV ` U ) ` x ) ) )
95 83 77 93 81 94 syl31anc 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( ( ( U normOpOLD W ) ` t ) x. ( ( normCV ` U ) ` x ) ) <_ ( d x. ( ( normCV ` U ) ` x ) ) )
96 72 86 87 89 95 letrd 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ ( t e. T /\ ( ( U normOpOLD W ) ` t ) <_ d ) ) -> ( N ` ( t ` x ) ) <_ ( d x. ( ( normCV ` U ) ` x ) ) )
97 96 expr 
 |-  ( ( ( ( ph /\ d e. RR ) /\ x e. X ) /\ t e. T ) -> ( ( ( U normOpOLD W ) ` t ) <_ d -> ( N ` ( t ` x ) ) <_ ( d x. ( ( normCV ` U ) ` x ) ) ) )
98 97 ralimdva 
 |-  ( ( ( ph /\ d e. RR ) /\ x e. X ) -> ( A. t e. T ( ( U normOpOLD W ) ` t ) <_ d -> A. t e. T ( N ` ( t ` x ) ) <_ ( d x. ( ( normCV ` U ) ` x ) ) ) )
99 brralrspcev 
 |-  ( ( ( d x. ( ( normCV ` U ) ` x ) ) e. RR /\ A. t e. T ( N ` ( t ` x ) ) <_ ( d x. ( ( normCV ` U ) ` x ) ) ) -> E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c )
100 59 98 99 syl6an 
 |-  ( ( ( ph /\ d e. RR ) /\ x e. X ) -> ( A. t e. T ( ( U normOpOLD W ) ` t ) <_ d -> E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c ) )
101 100 ralrimdva 
 |-  ( ( ph /\ d e. RR ) -> ( A. t e. T ( ( U normOpOLD W ) ` t ) <_ d -> A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c ) )
102 101 rexlimdva 
 |-  ( ph -> ( E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d -> A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c ) )
103 51 102 impbid 
 |-  ( ph -> ( A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( ( U normOpOLD W ) ` t ) <_ d ) )