ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  xporderlem Structured version   Unicode version

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

Proof of Theorem xporderlem
StepHypRef Expression
1 df-br 3756 . . 3  <. a ,  b >. T <. c ,  d >.  <. <. a ,  b >. ,  <. c ,  d >. >.  T
2 xporderlem.1 . . . 4  T  { <. , 
>.  |  X.  X.  1st `  R 1st `  1st `  1st `  2nd `  S 2nd `  }
32eleq2i 2101 . . 3  <. <.
a ,  b >. ,  <. c ,  d
>. >.  T  <. <. a ,  b >. ,  <. c ,  d >. >.  { <. ,  >.  |  X.  X.  1st `  R 1st `  1st `  1st `  2nd `  S 2nd `  }
41, 3bitri 173 . 2  <. a ,  b >. T <. c ,  d >.  <. <. a ,  b >. ,  <. c ,  d >. >.  { <. ,  >.  |  X.  X.  1st `  R 1st `  1st `  1st `  2nd `  S 2nd `  }
5 vex 2554 . . . 4  a 
_V
6 vex 2554 . . . 4  b 
_V
75, 6opex 3957 . . 3  <. a ,  b >.  _V
8 vex 2554 . . . 4  c 
_V
9 vex 2554 . . . 4  d 
_V
108, 9opex 3957 . . 3  <. c ,  d >.  _V
11 eleq1 2097 . . . . . 6  <. a ,  b
>.  X. 
<. a ,  b >.  X.
12 opelxp 4317 . . . . . 6  <. a ,  b >.  X.  a  b
1311, 12syl6bb 185 . . . . 5  <. a ,  b
>.  X.  a  b
1413anbi1d 438 . . . 4  <. a ,  b
>.  X.  X. 
a  b  X.
155, 6op1std 5717 . . . . . 6  <. a ,  b
>.  1st `  a
1615breq1d 3765 . . . . 5  <. a ,  b
>.  1st `  R 1st `  a R 1st `
1715eqeq1d 2045 . . . . . 6  <. a ,  b
>.  1st `  1st `  a  1st `
185, 6op2ndd 5718 . . . . . . 7  <. a ,  b
>.  2nd `  b
1918breq1d 3765 . . . . . 6  <. a ,  b
>.  2nd `  S 2nd `  b S 2nd `
2017, 19anbi12d 442 . . . . 5  <. a ,  b
>.  1st `  1st `  2nd `  S 2nd `  a  1st `  b S 2nd `
2116, 20orbi12d 706 . . . 4  <. a ,  b
>.  1st `  R 1st `  1st `  1st `  2nd `  S 2nd `  a R 1st `  a  1st `  b S 2nd `
2214, 21anbi12d 442 . . 3  <. a ,  b
>.  X.  X.  1st `  R 1st `  1st `  1st `  2nd `  S 2nd `  a  b  X.  a R 1st `  a  1st `  b S 2nd `
23 eleq1 2097 . . . . . 6  <. c ,  d
>.  X. 
<. c ,  d >.  X.
24 opelxp 4317 . . . . . 6  <. c ,  d >.  X.  c  d
2523, 24syl6bb 185 . . . . 5  <. c ,  d
>.  X.  c  d
2625anbi2d 437 . . . 4  <. c ,  d
>.  a  b  X.  a  b 
c  d
278, 9op1std 5717 . . . . . 6  <. c ,  d
>.  1st `  c
2827breq2d 3767 . . . . 5  <. c ,  d
>.  a R 1st `  a R c
2927eqeq2d 2048 . . . . . 6  <. c ,  d
>.  a  1st `  a  c
308, 9op2ndd 5718 . . . . . . 7  <. c ,  d
>.  2nd `  d
3130breq2d 3767 . . . . . 6  <. c ,  d
>.  b S 2nd `  b S d
3229, 31anbi12d 442 . . . . 5  <. c ,  d
>.  a  1st `  b S 2nd `  a  c  b S d
3328, 32orbi12d 706 . . . 4  <. c ,  d
>.  a R 1st `  a  1st `  b S 2nd `  a R c 
a  c  b S d
3426, 33anbi12d 442 . . 3  <. c ,  d
>.  a  b  X.  a R 1st `  a  1st `  b S 2nd `  a  b  c  d  a R c  a  c  b S d
357, 10, 22, 34opelopab 3999 . 2  <. <.
a ,  b >. ,  <. c ,  d
>. >.  { <. ,  >.  |  X.  X.  1st `  R 1st `  1st `  1st `  2nd `  S 2nd `  }  a  b 
c  d  a R c  a  c  b S d
36 an4 520 . . 3  a  b  c  d  a  c  b  d
3736anbi1i 431 . 2  a  b 
c  d  a R c  a  c  b S d  a  c  b  d 
a R c  a  c  b S d
384, 35, 373bitri 195 1  <. a ,  b >. T <. c ,  d >.  a  c  b  d  a R c  a  c  b S d
Colors of variables: wff set class
Syntax hints:   wa 97   wb 98   wo 628   wceq 1242   wcel 1390   <.cop 3370   class class class wbr 3755   {copab 3808    X. cxp 4286   ` cfv 4845   1stc1st 5707   2ndc2nd 5708
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-iota 4810  df-fun 4847  df-fv 4853  df-1st 5709  df-2nd 5710
This theorem is referenced by:  poxp  5794
  Copyright terms: Public domain W3C validator