Users' Mathboxes Mathbox for ML < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isbasisrelowllem1 Structured version   Unicode version

Theorem isbasisrelowllem1 31699
Description: Lemma for isbasisrelowl 31702. (Contributed by ML, 27-Jul-2020.)
Hypothesis
Ref Expression
isbasisrelowl.1  |-  I  =  ( [,) " ( RR  X.  RR ) )
Assertion
Ref Expression
isbasisrelowllem1  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  -> 
( x  i^i  y
)  e.  I )
Distinct variable groups:    x, I,
y, z    a, b, x, z    b, c, y, x, z    c, d, y, z
Allowed substitution hints:    I( a, b, c, d)

Proof of Theorem isbasisrelowllem1
StepHypRef Expression
1 simplr1 1047 . . . . 5  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  -> 
c  e.  RR )
2 simpll2 1045 . . . . . . . 8  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  -> 
b  e.  RR )
3 nfv 1751 . . . . . . . . . . . 12  |-  F/ z  a  e.  RR
4 nfv 1751 . . . . . . . . . . . 12  |-  F/ z  b  e.  RR
5 nfrab1 3009 . . . . . . . . . . . . 13  |-  F/_ z { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) }
65nfeq2 2601 . . . . . . . . . . . 12  |-  F/ z  x  =  { z  e.  RR  |  ( a  <_  z  /\  z  <  b ) }
73, 4, 6nf3an 1986 . . . . . . . . . . 11  |-  F/ z ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_  z  /\  z  <  b ) } )
8 nfv 1751 . . . . . . . . . . . 12  |-  F/ z  c  e.  RR
9 nfv 1751 . . . . . . . . . . . 12  |-  F/ z  d  e.  RR
10 nfrab1 3009 . . . . . . . . . . . . 13  |-  F/_ z { z  e.  RR  |  ( c  <_ 
z  /\  z  <  d ) }
1110nfeq2 2601 . . . . . . . . . . . 12  |-  F/ z  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) }
128, 9, 11nf3an 1986 . . . . . . . . . . 11  |-  F/ z ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } )
137, 12nfan 1984 . . . . . . . . . 10  |-  F/ z ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )
14 nfv 1751 . . . . . . . . . 10  |-  F/ z ( a  <_  c  /\  b  <_  d )
1513, 14nfan 1984 . . . . . . . . 9  |-  F/ z ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )
16 nfcv 2584 . . . . . . . . 9  |-  F/_ z
( x  i^i  y
)
17 nfrab1 3009 . . . . . . . . 9  |-  F/_ z { z  e.  RR  |  ( c  <_ 
z  /\  z  <  b ) }
18 simp3 1007 . . . . . . . . . . . . . 14  |-  ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  ->  x  =  { z  e.  RR  |  ( a  <_  z  /\  z  <  b ) } )
19 simp3 1007 . . . . . . . . . . . . . 14  |-  ( ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_ 
z  /\  z  <  d ) } )  -> 
y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } )
20 elin 3649 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  ( x  i^i  y )  <->  ( z  e.  x  /\  z  e.  y ) )
21 eleq2 2495 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  { z  e.  RR  |  ( a  <_  z  /\  z  <  b ) }  ->  ( z  e.  x  <->  z  e.  { z  e.  RR  | 
( a  <_  z  /\  z  <  b ) } ) )
22 rabid 3005 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  { z  e.  RR  |  ( a  <_  z  /\  z  <  b ) }  <->  ( z  e.  RR  /\  ( a  <_  z  /\  z  <  b ) ) )
2321, 22syl6bb 264 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  { z  e.  RR  |  ( a  <_  z  /\  z  <  b ) }  ->  ( z  e.  x  <->  ( z  e.  RR  /\  ( a  <_  z  /\  z  <  b ) ) ) )
2423anbi1d 709 . . . . . . . . . . . . . . . . 17  |-  ( x  =  { z  e.  RR  |  ( a  <_  z  /\  z  <  b ) }  ->  ( ( z  e.  x  /\  z  e.  y
)  <->  ( ( z  e.  RR  /\  (
a  <_  z  /\  z  <  b ) )  /\  z  e.  y ) ) )
2520, 24syl5bb 260 . . . . . . . . . . . . . . . 16  |-  ( x  =  { z  e.  RR  |  ( a  <_  z  /\  z  <  b ) }  ->  ( z  e.  ( x  i^i  y )  <->  ( (
z  e.  RR  /\  ( a  <_  z  /\  z  <  b ) )  /\  z  e.  y ) ) )
26 eleq2 2495 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) }  ->  ( z  e.  y  <->  z  e.  { z  e.  RR  | 
( c  <_  z  /\  z  <  d ) } ) )
27 rabid 3005 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) }  <->  ( z  e.  RR  /\  ( c  <_  z  /\  z  <  d ) ) )
2826, 27syl6bb 264 . . . . . . . . . . . . . . . . 17  |-  ( y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) }  ->  ( z  e.  y  <->  ( z  e.  RR  /\  ( c  <_  z  /\  z  <  d ) ) ) )
2928anbi2d 708 . . . . . . . . . . . . . . . 16  |-  ( y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) }  ->  ( ( ( z  e.  RR  /\  ( a  <_  z  /\  z  <  b ) )  /\  z  e.  y )  <->  ( ( z  e.  RR  /\  ( a  <_  z  /\  z  <  b ) )  /\  ( z  e.  RR  /\  (
c  <_  z  /\  z  <  d ) ) ) ) )
3025, 29sylan9bb 704 . . . . . . . . . . . . . . 15  |-  ( ( x  =  { z  e.  RR  |  ( a  <_  z  /\  z  <  b ) }  /\  y  =  {
z  e.  RR  | 
( c  <_  z  /\  z  <  d ) } )  ->  (
z  e.  ( x  i^i  y )  <->  ( (
z  e.  RR  /\  ( a  <_  z  /\  z  <  b ) )  /\  ( z  e.  RR  /\  (
c  <_  z  /\  z  <  d ) ) ) ) )
31 an4 831 . . . . . . . . . . . . . . . 16  |-  ( ( ( z  e.  RR  /\  ( a  <_  z  /\  z  <  b ) )  /\  ( z  e.  RR  /\  (
c  <_  z  /\  z  <  d ) ) )  <->  ( ( z  e.  RR  /\  z  e.  RR )  /\  (
( a  <_  z  /\  z  <  b )  /\  ( c  <_ 
z  /\  z  <  d ) ) ) )
32 anidm 648 . . . . . . . . . . . . . . . . 17  |-  ( ( z  e.  RR  /\  z  e.  RR )  <->  z  e.  RR )
3332anbi1i 699 . . . . . . . . . . . . . . . 16  |-  ( ( ( z  e.  RR  /\  z  e.  RR )  /\  ( ( a  <_  z  /\  z  <  b )  /\  (
c  <_  z  /\  z  <  d ) ) )  <->  ( z  e.  RR  /\  ( ( a  <_  z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) ) )
3431, 33bitri 252 . . . . . . . . . . . . . . 15  |-  ( ( ( z  e.  RR  /\  ( a  <_  z  /\  z  <  b ) )  /\  ( z  e.  RR  /\  (
c  <_  z  /\  z  <  d ) ) )  <->  ( z  e.  RR  /\  ( ( a  <_  z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) ) )
3530, 34syl6bb 264 . . . . . . . . . . . . . 14  |-  ( ( x  =  { z  e.  RR  |  ( a  <_  z  /\  z  <  b ) }  /\  y  =  {
z  e.  RR  | 
( c  <_  z  /\  z  <  d ) } )  ->  (
z  e.  ( x  i^i  y )  <->  ( z  e.  RR  /\  ( ( a  <_  z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) ) ) )
3618, 19, 35syl2an 479 . . . . . . . . . . . . 13  |-  ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_  z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_ 
z  /\  z  <  d ) } ) )  ->  ( z  e.  ( x  i^i  y
)  <->  ( z  e.  RR  /\  ( ( a  <_  z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) ) ) )
3736adantr 466 . . . . . . . . . . . 12  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  -> 
( z  e.  ( x  i^i  y )  <-> 
( z  e.  RR  /\  ( ( a  <_ 
z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) ) ) )
38 simpl 458 . . . . . . . . . . . . 13  |-  ( ( z  e.  RR  /\  ( ( a  <_ 
z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) )  ->  z  e.  RR )
39 simprrl 772 . . . . . . . . . . . . 13  |-  ( ( z  e.  RR  /\  ( ( a  <_ 
z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) )  ->  c  <_  z
)
40 simprlr 771 . . . . . . . . . . . . 13  |-  ( ( z  e.  RR  /\  ( ( a  <_ 
z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) )  ->  z  <  b
)
4138, 39, 40jca32 537 . . . . . . . . . . . 12  |-  ( ( z  e.  RR  /\  ( ( a  <_ 
z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) )  ->  ( z  e.  RR  /\  ( c  <_  z  /\  z  <  b ) ) )
4237, 41syl6bi 231 . . . . . . . . . . 11  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  -> 
( z  e.  ( x  i^i  y )  ->  ( z  e.  RR  /\  ( c  <_  z  /\  z  <  b ) ) ) )
43 3simpa 1002 . . . . . . . . . . . . . . . . . 18  |-  ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  -> 
( a  e.  RR  /\  b  e.  RR ) )
44 3simpa 1002 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_ 
z  /\  z  <  d ) } )  -> 
( c  e.  RR  /\  d  e.  RR ) )
4543, 44anim12i 568 . . . . . . . . . . . . . . . . 17  |-  ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_  z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_ 
z  /\  z  <  d ) } ) )  ->  ( ( a  e.  RR  /\  b  e.  RR )  /\  (
c  e.  RR  /\  d  e.  RR )
) )
46 letr 9728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( a  e.  RR  /\  c  e.  RR  /\  z  e.  RR )  ->  (
( a  <_  c  /\  c  <_  z )  ->  a  <_  z
) )
47463expia 1207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( a  e.  RR  /\  c  e.  RR )  ->  ( z  e.  RR  ->  ( ( a  <_ 
c  /\  c  <_  z )  ->  a  <_  z ) ) )
4847exp4a 609 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( a  e.  RR  /\  c  e.  RR )  ->  ( z  e.  RR  ->  ( a  <_  c  ->  ( c  <_  z  ->  a  <_  z )
) ) )
4948ad2ant2r 751 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( a  e.  RR  /\  b  e.  RR )  /\  ( c  e.  RR  /\  d  e.  RR ) )  -> 
( z  e.  RR  ->  ( a  <_  c  ->  ( c  <_  z  ->  a  <_  z )
) ) )
50 ltletr 9726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( z  e.  RR  /\  b  e.  RR  /\  d  e.  RR )  ->  (
( z  <  b  /\  b  <_  d )  ->  z  <  d
) )
51503coml 1212 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( b  e.  RR  /\  d  e.  RR  /\  z  e.  RR )  ->  (
( z  <  b  /\  b  <_  d )  ->  z  <  d
) )
5251expcomd 439 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( b  e.  RR  /\  d  e.  RR  /\  z  e.  RR )  ->  (
b  <_  d  ->  ( z  <  b  -> 
z  <  d )
) )
53523expia 1207 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( b  e.  RR  /\  d  e.  RR )  ->  ( z  e.  RR  ->  ( b  <_  d  ->  ( z  <  b  ->  z  <  d ) ) ) )
5453ad2ant2l 750 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( a  e.  RR  /\  b  e.  RR )  /\  ( c  e.  RR  /\  d  e.  RR ) )  -> 
( z  e.  RR  ->  ( b  <_  d  ->  ( z  <  b  ->  z  <  d ) ) ) )
5549, 54jcad 535 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( a  e.  RR  /\  b  e.  RR )  /\  ( c  e.  RR  /\  d  e.  RR ) )  -> 
( z  e.  RR  ->  ( ( a  <_ 
c  ->  ( c  <_  z  ->  a  <_  z ) )  /\  (
b  <_  d  ->  ( z  <  b  -> 
z  <  d )
) ) ) )
56 prth 573 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( a  <_  c  ->  ( c  <_  z  ->  a  <_  z )
)  /\  ( b  <_  d  ->  ( z  <  b  ->  z  <  d ) ) )  -> 
( ( a  <_ 
c  /\  b  <_  d )  ->  ( (
c  <_  z  ->  a  <_  z )  /\  ( z  <  b  ->  z  <  d ) ) ) )
5755, 56syl6 34 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( a  e.  RR  /\  b  e.  RR )  /\  ( c  e.  RR  /\  d  e.  RR ) )  -> 
( z  e.  RR  ->  ( ( a  <_ 
c  /\  b  <_  d )  ->  ( (
c  <_  z  ->  a  <_  z )  /\  ( z  <  b  ->  z  <  d ) ) ) ) )
5857com23 81 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( a  e.  RR  /\  b  e.  RR )  /\  ( c  e.  RR  /\  d  e.  RR ) )  -> 
( ( a  <_ 
c  /\  b  <_  d )  ->  ( z  e.  RR  ->  ( (
c  <_  z  ->  a  <_  z )  /\  ( z  <  b  ->  z  <  d ) ) ) ) )
59 prth 573 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( c  <_  z  ->  a  <_  z )  /\  ( z  <  b  ->  z  <  d ) )  ->  ( (
c  <_  z  /\  z  <  b )  -> 
( a  <_  z  /\  z  <  d ) ) )
6058, 59syl8 72 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( a  e.  RR  /\  b  e.  RR )  /\  ( c  e.  RR  /\  d  e.  RR ) )  -> 
( ( a  <_ 
c  /\  b  <_  d )  ->  ( z  e.  RR  ->  ( (
c  <_  z  /\  z  <  b )  -> 
( a  <_  z  /\  z  <  d ) ) ) ) )
6160imp31 433 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( a  e.  RR  /\  b  e.  RR )  /\  (
c  e.  RR  /\  d  e.  RR )
)  /\  ( a  <_  c  /\  b  <_ 
d ) )  /\  z  e.  RR )  ->  ( ( c  <_ 
z  /\  z  <  b )  ->  ( a  <_  z  /\  z  < 
d ) ) )
6261ancrd 556 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( a  e.  RR  /\  b  e.  RR )  /\  (
c  e.  RR  /\  d  e.  RR )
)  /\  ( a  <_  c  /\  b  <_ 
d ) )  /\  z  e.  RR )  ->  ( ( c  <_ 
z  /\  z  <  b )  ->  ( (
a  <_  z  /\  z  <  d )  /\  ( c  <_  z  /\  z  <  b ) ) ) )
63 an42 832 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( a  <_  z  /\  z  <  d )  /\  ( c  <_ 
z  /\  z  <  b ) )  <->  ( (
a  <_  z  /\  c  <_  z )  /\  ( z  <  b  /\  z  <  d ) ) )
64 an4 831 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( a  <_  z  /\  c  <_  z )  /\  ( z  < 
b  /\  z  <  d ) )  <->  ( (
a  <_  z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) )
6563, 64bitri 252 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( a  <_  z  /\  z  <  d )  /\  ( c  <_ 
z  /\  z  <  b ) )  <->  ( (
a  <_  z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) )
6662, 65syl6ib 229 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( a  e.  RR  /\  b  e.  RR )  /\  (
c  e.  RR  /\  d  e.  RR )
)  /\  ( a  <_  c  /\  b  <_ 
d ) )  /\  z  e.  RR )  ->  ( ( c  <_ 
z  /\  z  <  b )  ->  ( (
a  <_  z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) ) )
67 simpr 462 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( a  e.  RR  /\  b  e.  RR )  /\  (
c  e.  RR  /\  d  e.  RR )
)  /\  ( a  <_  c  /\  b  <_ 
d ) )  /\  z  e.  RR )  ->  z  e.  RR )
6866, 67jctild 545 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( a  e.  RR  /\  b  e.  RR )  /\  (
c  e.  RR  /\  d  e.  RR )
)  /\  ( a  <_  c  /\  b  <_ 
d ) )  /\  z  e.  RR )  ->  ( ( c  <_ 
z  /\  z  <  b )  ->  ( z  e.  RR  /\  ( ( a  <_  z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) ) ) )
6945, 68sylanl1 654 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  /\  z  e.  RR )  ->  ( ( c  <_ 
z  /\  z  <  b )  ->  ( z  e.  RR  /\  ( ( a  <_  z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) ) ) )
7069imp 430 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  /\  z  e.  RR )  /\  ( c  <_  z  /\  z  <  b ) )  ->  ( z  e.  RR  /\  ( ( a  <_  z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) ) )
7170an32s 811 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  /\  ( c  <_  z  /\  z  <  b ) )  /\  z  e.  RR )  ->  (
z  e.  RR  /\  ( ( a  <_ 
z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) ) )
7237adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  /\  ( c  <_  z  /\  z  <  b ) )  ->  ( z  e.  ( x  i^i  y
)  <->  ( z  e.  RR  /\  ( ( a  <_  z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) ) ) )
7372adantr 466 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  /\  ( c  <_  z  /\  z  <  b ) )  /\  z  e.  RR )  ->  (
z  e.  ( x  i^i  y )  <->  ( z  e.  RR  /\  ( ( a  <_  z  /\  z  <  b )  /\  ( c  <_  z  /\  z  <  d ) ) ) ) )
7471, 73mpbird 235 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  /\  ( c  <_  z  /\  z  <  b ) )  /\  z  e.  RR )  ->  z  e.  ( x  i^i  y
) )
7574expl 622 . . . . . . . . . . . 12  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  -> 
( ( ( c  <_  z  /\  z  <  b )  /\  z  e.  RR )  ->  z  e.  ( x  i^i  y
) ) )
7675ancomsd 455 . . . . . . . . . . 11  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  -> 
( ( z  e.  RR  /\  ( c  <_  z  /\  z  <  b ) )  -> 
z  e.  ( x  i^i  y ) ) )
7742, 76impbid 193 . . . . . . . . . 10  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  -> 
( z  e.  ( x  i^i  y )  <-> 
( z  e.  RR  /\  ( c  <_  z  /\  z  <  b ) ) ) )
78 rabid 3005 . . . . . . . . . 10  |-  ( z  e.  { z  e.  RR  |  ( c  <_  z  /\  z  <  b ) }  <->  ( z  e.  RR  /\  ( c  <_  z  /\  z  <  b ) ) )
7977, 78syl6bbr 266 . . . . . . . . 9  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  -> 
( z  e.  ( x  i^i  y )  <-> 
z  e.  { z  e.  RR  |  ( c  <_  z  /\  z  <  b ) } ) )
8015, 16, 17, 79eqrd 3482 . . . . . . . 8  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  -> 
( x  i^i  y
)  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  b ) } )
812, 80jca 534 . . . . . . 7  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  -> 
( b  e.  RR  /\  ( x  i^i  y
)  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  b ) } ) )
82 19.8a 1908 . . . . . . 7  |-  ( ( b  e.  RR  /\  ( x  i^i  y
)  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  b ) } )  ->  E. b
( b  e.  RR  /\  ( x  i^i  y
)  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  b ) } ) )
8381, 82syl 17 . . . . . 6  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  ->  E. b ( b  e.  RR  /\  ( x  i^i  y )  =  { z  e.  RR  |  ( c  <_ 
z  /\  z  <  b ) } ) )
84 df-rex 2781 . . . . . 6  |-  ( E. b  e.  RR  (
x  i^i  y )  =  { z  e.  RR  |  ( c  <_ 
z  /\  z  <  b ) }  <->  E. b
( b  e.  RR  /\  ( x  i^i  y
)  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  b ) } ) )
8583, 84sylibr 215 . . . . 5  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  ->  E. b  e.  RR  ( x  i^i  y
)  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  b ) } )
861, 85jca 534 . . . 4  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  -> 
( c  e.  RR  /\ 
E. b  e.  RR  ( x  i^i  y
)  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  b ) } ) )
87 19.8a 1908 . . . 4  |-  ( ( c  e.  RR  /\  E. b  e.  RR  (
x  i^i  y )  =  { z  e.  RR  |  ( c  <_ 
z  /\  z  <  b ) } )  ->  E. c ( c  e.  RR  /\  E. b  e.  RR  ( x  i^i  y )  =  {
z  e.  RR  | 
( c  <_  z  /\  z  <  b ) } ) )
8886, 87syl 17 . . 3  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  ->  E. c ( c  e.  RR  /\  E. b  e.  RR  ( x  i^i  y )  =  {
z  e.  RR  | 
( c  <_  z  /\  z  <  b ) } ) )
89 df-rex 2781 . . 3  |-  ( E. c  e.  RR  E. b  e.  RR  (
x  i^i  y )  =  { z  e.  RR  |  ( c  <_ 
z  /\  z  <  b ) }  <->  E. c
( c  e.  RR  /\ 
E. b  e.  RR  ( x  i^i  y
)  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  b ) } ) )
9088, 89sylibr 215 . 2  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  ->  E. c  e.  RR  E. b  e.  RR  (
x  i^i  y )  =  { z  e.  RR  |  ( c  <_ 
z  /\  z  <  b ) } )
91 isbasisrelowl.1 . . 3  |-  I  =  ( [,) " ( RR  X.  RR ) )
9291icoreelrnab 31698 . 2  |-  ( ( x  i^i  y )  e.  I  <->  E. c  e.  RR  E. b  e.  RR  ( x  i^i  y )  =  {
z  e.  RR  | 
( c  <_  z  /\  z  <  b ) } )
9390, 92sylibr 215 1  |-  ( ( ( ( a  e.  RR  /\  b  e.  RR  /\  x  =  { z  e.  RR  |  ( a  <_ 
z  /\  z  <  b ) } )  /\  ( c  e.  RR  /\  d  e.  RR  /\  y  =  { z  e.  RR  |  ( c  <_  z  /\  z  <  d ) } ) )  /\  ( a  <_  c  /\  b  <_  d ) )  -> 
( x  i^i  y
)  e.  I )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437   E.wex 1659    e. wcel 1868   E.wrex 2776   {crab 2779    i^i cin 3435   class class class wbr 4420    X. cxp 4848   "cima 4853   RRcr 9539    < clt 9676    <_ cle 9677   [,)cico 11638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-cnex 9596  ax-resscn 9597  ax-pre-lttri 9614  ax-pre-lttrn 9615
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-po 4771  df-so 4772  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-1st 6804  df-2nd 6805  df-er 7368  df-en 7575  df-dom 7576  df-sdom 7577  df-pnf 9678  df-mnf 9679  df-xr 9680  df-ltxr 9681  df-le 9682  df-ico 11642
This theorem is referenced by:  icoreclin  31701
  Copyright terms: Public domain W3C validator