MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xporderlem Structured version   Unicode version

Theorem xporderlem 6681
Description: Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011.)
Hypothesis
Ref Expression
xporderlem.1  |-  T  =  { <. x ,  y
>.  |  ( (
x  e.  ( A  X.  B )  /\  y  e.  ( A  X.  B ) )  /\  ( ( 1st `  x
) R ( 1st `  y )  \/  (
( 1st `  x
)  =  ( 1st `  y )  /\  ( 2nd `  x ) S ( 2nd `  y
) ) ) ) }
Assertion
Ref Expression
xporderlem  |-  ( <.
a ,  b >. T <. c ,  d
>. 
<->  ( ( ( a  e.  A  /\  c  e.  A )  /\  (
b  e.  B  /\  d  e.  B )
)  /\  ( a R c  \/  (
a  =  c  /\  b S d ) ) ) )
Distinct variable groups:    x, A, y    x, B, y    x, R, y    x, S, y   
x, a, y    x, b, y    x, c, y   
x, d, y
Allowed substitution hints:    A( a, b, c, d)    B( a, b, c, d)    R( a, b, c, d)    S( a, b, c, d)    T( x, y, a, b, c, d)

Proof of Theorem xporderlem
StepHypRef Expression
1 df-br 4291 . . 3  |-  ( <.
a ,  b >. T <. c ,  d
>. 
<-> 
<. <. a ,  b
>. ,  <. c ,  d >. >.  e.  T )
2 xporderlem.1 . . . 4  |-  T  =  { <. x ,  y
>.  |  ( (
x  e.  ( A  X.  B )  /\  y  e.  ( A  X.  B ) )  /\  ( ( 1st `  x
) R ( 1st `  y )  \/  (
( 1st `  x
)  =  ( 1st `  y )  /\  ( 2nd `  x ) S ( 2nd `  y
) ) ) ) }
32eleq2i 2505 . . 3  |-  ( <. <. a ,  b >. ,  <. c ,  d
>. >.  e.  T  <->  <. <. a ,  b >. ,  <. c ,  d >. >.  e.  { <. x ,  y >.  |  ( ( x  e.  ( A  X.  B )  /\  y  e.  ( A  X.  B
) )  /\  (
( 1st `  x
) R ( 1st `  y )  \/  (
( 1st `  x
)  =  ( 1st `  y )  /\  ( 2nd `  x ) S ( 2nd `  y
) ) ) ) } )
41, 3bitri 249 . 2  |-  ( <.
a ,  b >. T <. c ,  d
>. 
<-> 
<. <. a ,  b
>. ,  <. c ,  d >. >.  e.  { <. x ,  y >.  |  ( ( x  e.  ( A  X.  B )  /\  y  e.  ( A  X.  B ) )  /\  ( ( 1st `  x ) R ( 1st `  y
)  \/  ( ( 1st `  x )  =  ( 1st `  y
)  /\  ( 2nd `  x ) S ( 2nd `  y ) ) ) ) } )
5 opex 4554 . . 3  |-  <. a ,  b >.  e.  _V
6 opex 4554 . . 3  |-  <. c ,  d >.  e.  _V
7 eleq1 2501 . . . . . 6  |-  ( x  =  <. a ,  b
>.  ->  ( x  e.  ( A  X.  B
)  <->  <. a ,  b
>.  e.  ( A  X.  B ) ) )
8 opelxp 4867 . . . . . 6  |-  ( <.
a ,  b >.  e.  ( A  X.  B
)  <->  ( a  e.  A  /\  b  e.  B ) )
97, 8syl6bb 261 . . . . 5  |-  ( x  =  <. a ,  b
>.  ->  ( x  e.  ( A  X.  B
)  <->  ( a  e.  A  /\  b  e.  B ) ) )
109anbi1d 704 . . . 4  |-  ( x  =  <. a ,  b
>.  ->  ( ( x  e.  ( A  X.  B )  /\  y  e.  ( A  X.  B
) )  <->  ( (
a  e.  A  /\  b  e.  B )  /\  y  e.  ( A  X.  B ) ) ) )
11 vex 2973 . . . . . . 7  |-  a  e. 
_V
12 vex 2973 . . . . . . 7  |-  b  e. 
_V
1311, 12op1std 6585 . . . . . 6  |-  ( x  =  <. a ,  b
>.  ->  ( 1st `  x
)  =  a )
1413breq1d 4300 . . . . 5  |-  ( x  =  <. a ,  b
>.  ->  ( ( 1st `  x ) R ( 1st `  y )  <-> 
a R ( 1st `  y ) ) )
1513eqeq1d 2449 . . . . . 6  |-  ( x  =  <. a ,  b
>.  ->  ( ( 1st `  x )  =  ( 1st `  y )  <-> 
a  =  ( 1st `  y ) ) )
1611, 12op2ndd 6586 . . . . . . 7  |-  ( x  =  <. a ,  b
>.  ->  ( 2nd `  x
)  =  b )
1716breq1d 4300 . . . . . 6  |-  ( x  =  <. a ,  b
>.  ->  ( ( 2nd `  x ) S ( 2nd `  y )  <-> 
b S ( 2nd `  y ) ) )
1815, 17anbi12d 710 . . . . 5  |-  ( x  =  <. a ,  b
>.  ->  ( ( ( 1st `  x )  =  ( 1st `  y
)  /\  ( 2nd `  x ) S ( 2nd `  y ) )  <->  ( a  =  ( 1st `  y
)  /\  b S
( 2nd `  y
) ) ) )
1914, 18orbi12d 709 . . . 4  |-  ( x  =  <. a ,  b
>.  ->  ( ( ( 1st `  x ) R ( 1st `  y
)  \/  ( ( 1st `  x )  =  ( 1st `  y
)  /\  ( 2nd `  x ) S ( 2nd `  y ) ) )  <->  ( a R ( 1st `  y
)  \/  ( a  =  ( 1st `  y
)  /\  b S
( 2nd `  y
) ) ) ) )
2010, 19anbi12d 710 . . 3  |-  ( x  =  <. a ,  b
>.  ->  ( ( ( x  e.  ( A  X.  B )  /\  y  e.  ( A  X.  B ) )  /\  ( ( 1st `  x
) R ( 1st `  y )  \/  (
( 1st `  x
)  =  ( 1st `  y )  /\  ( 2nd `  x ) S ( 2nd `  y
) ) ) )  <-> 
( ( ( a  e.  A  /\  b  e.  B )  /\  y  e.  ( A  X.  B
) )  /\  (
a R ( 1st `  y )  \/  (
a  =  ( 1st `  y )  /\  b S ( 2nd `  y
) ) ) ) ) )
21 eleq1 2501 . . . . . 6  |-  ( y  =  <. c ,  d
>.  ->  ( y  e.  ( A  X.  B
)  <->  <. c ,  d
>.  e.  ( A  X.  B ) ) )
22 opelxp 4867 . . . . . 6  |-  ( <.
c ,  d >.  e.  ( A  X.  B
)  <->  ( c  e.  A  /\  d  e.  B ) )
2321, 22syl6bb 261 . . . . 5  |-  ( y  =  <. c ,  d
>.  ->  ( y  e.  ( A  X.  B
)  <->  ( c  e.  A  /\  d  e.  B ) ) )
2423anbi2d 703 . . . 4  |-  ( y  =  <. c ,  d
>.  ->  ( ( ( a  e.  A  /\  b  e.  B )  /\  y  e.  ( A  X.  B ) )  <-> 
( ( a  e.  A  /\  b  e.  B )  /\  (
c  e.  A  /\  d  e.  B )
) ) )
25 vex 2973 . . . . . . 7  |-  c  e. 
_V
26 vex 2973 . . . . . . 7  |-  d  e. 
_V
2725, 26op1std 6585 . . . . . 6  |-  ( y  =  <. c ,  d
>.  ->  ( 1st `  y
)  =  c )
2827breq2d 4302 . . . . 5  |-  ( y  =  <. c ,  d
>.  ->  ( a R ( 1st `  y
)  <->  a R c ) )
2927eqeq2d 2452 . . . . . 6  |-  ( y  =  <. c ,  d
>.  ->  ( a  =  ( 1st `  y
)  <->  a  =  c ) )
3025, 26op2ndd 6586 . . . . . . 7  |-  ( y  =  <. c ,  d
>.  ->  ( 2nd `  y
)  =  d )
3130breq2d 4302 . . . . . 6  |-  ( y  =  <. c ,  d
>.  ->  ( b S ( 2nd `  y
)  <->  b S d ) )
3229, 31anbi12d 710 . . . . 5  |-  ( y  =  <. c ,  d
>.  ->  ( ( a  =  ( 1st `  y
)  /\  b S
( 2nd `  y
) )  <->  ( a  =  c  /\  b S d ) ) )
3328, 32orbi12d 709 . . . 4  |-  ( y  =  <. c ,  d
>.  ->  ( ( a R ( 1st `  y
)  \/  ( a  =  ( 1st `  y
)  /\  b S
( 2nd `  y
) ) )  <->  ( a R c  \/  (
a  =  c  /\  b S d ) ) ) )
3424, 33anbi12d 710 . . 3  |-  ( y  =  <. c ,  d
>.  ->  ( ( ( ( a  e.  A  /\  b  e.  B
)  /\  y  e.  ( A  X.  B
) )  /\  (
a R ( 1st `  y )  \/  (
a  =  ( 1st `  y )  /\  b S ( 2nd `  y
) ) ) )  <-> 
( ( ( a  e.  A  /\  b  e.  B )  /\  (
c  e.  A  /\  d  e.  B )
)  /\  ( a R c  \/  (
a  =  c  /\  b S d ) ) ) ) )
355, 6, 20, 34opelopab 4608 . 2  |-  ( <. <. a ,  b >. ,  <. c ,  d
>. >.  e.  { <. x ,  y >.  |  ( ( x  e.  ( A  X.  B )  /\  y  e.  ( A  X.  B ) )  /\  ( ( 1st `  x ) R ( 1st `  y
)  \/  ( ( 1st `  x )  =  ( 1st `  y
)  /\  ( 2nd `  x ) S ( 2nd `  y ) ) ) ) }  <-> 
( ( ( a  e.  A  /\  b  e.  B )  /\  (
c  e.  A  /\  d  e.  B )
)  /\  ( a R c  \/  (
a  =  c  /\  b S d ) ) ) )
36 an4 820 . . 3  |-  ( ( ( a  e.  A  /\  b  e.  B
)  /\  ( c  e.  A  /\  d  e.  B ) )  <->  ( (
a  e.  A  /\  c  e.  A )  /\  ( b  e.  B  /\  d  e.  B
) ) )
3736anbi1i 695 . 2  |-  ( ( ( ( a  e.  A  /\  b  e.  B )  /\  (
c  e.  A  /\  d  e.  B )
)  /\  ( a R c  \/  (
a  =  c  /\  b S d ) ) )  <->  ( ( ( a  e.  A  /\  c  e.  A )  /\  ( b  e.  B  /\  d  e.  B
) )  /\  (
a R c  \/  ( a  =  c  /\  b S d ) ) ) )
384, 35, 373bitri 271 1  |-  ( <.
a ,  b >. T <. c ,  d
>. 
<->  ( ( ( a  e.  A  /\  c  e.  A )  /\  (
b  e.  B  /\  d  e.  B )
)  /\  ( a R c  \/  (
a  =  c  /\  b S d ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1369    e. wcel 1756   <.cop 3881   class class class wbr 4290   {copab 4347    X. cxp 4836   ` cfv 5416   1stc1st 6573   2ndc2nd 6574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-sep 4411  ax-nul 4419  ax-pow 4468  ax-pr 4529  ax-un 6370
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3185  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-nul 3636  df-if 3790  df-sn 3876  df-pr 3878  df-op 3882  df-uni 4090  df-br 4291  df-opab 4349  df-mpt 4350  df-id 4634  df-xp 4844  df-rel 4845  df-cnv 4846  df-co 4847  df-dm 4848  df-rn 4849  df-iota 5379  df-fun 5418  df-fv 5424  df-1st 6575  df-2nd 6576
This theorem is referenced by:  poxp  6682  soxp  6683
  Copyright terms: Public domain W3C validator