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

Theorem poxp 5794
Description: A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.)
Hypothesis
Ref Expression
poxp.1  T  { <. , 
>.  |  X.  X.  1st `  R 1st `  1st `  1st `  2nd `  S 2nd `  }
Assertion
Ref Expression
poxp  R  Po  S  Po  T  Po  X.
Distinct variable groups:   ,,   ,,   , R,   , S,
Allowed substitution hints:    T(,)

Proof of Theorem poxp
Dummy variables  a  b  c  d  e  t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxp 4305 . . . . . . . 8  t  X.  a b t 
<. a ,  b >.  a  b
2 elxp 4305 . . . . . . . 8  X.  c d 
<. c ,  d >.  c  d
3 elxp 4305 . . . . . . . 8  X.  e 
<. e ,  >.  e
4 3an6 1216 . . . . . . . . . . . . . . . . 17  t  <. a ,  b >. 
a  b 
<. c ,  d >.  c  d  <. e ,  >. 
e 
t  <. a ,  b >.  <. c ,  d
>.  <. e ,  >.  a  b 
c  d  e
5 poirr 4035 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  R  Po  a  a R a
65ex 108 . . . . . . . . . . . . . . . . . . . . . . . . . 26  R  Po 
a  a R a
7 poirr 4035 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  S  Po  b  b S b
87intnand 839 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  S  Po  b  a  a  b S b
98ex 108 . . . . . . . . . . . . . . . . . . . . . . . . . 26  S  Po 
b  a  a  b S b
106, 9im2anan9 530 . . . . . . . . . . . . . . . . . . . . . . . . 25  R  Po  S  Po  a  b  a R a  a  a  b S b
11 ioran 668 . . . . . . . . . . . . . . . . . . . . . . . . 25  a R a  a  a  b S b  a R a  a  a  b S b
1210, 11syl6ibr 151 . . . . . . . . . . . . . . . . . . . . . . . 24  R  Po  S  Po  a  b  a R a  a  a  b S b
1312imp 115 . . . . . . . . . . . . . . . . . . . . . . 23  R  Po  S  Po  a  b  a R a  a  a  b S b
1413intnand 839 . . . . . . . . . . . . . . . . . . . . . 22  R  Po  S  Po  a  b  a  a 
b  b  a R a  a  a  b S b
15143ad2antr1 1068 . . . . . . . . . . . . . . . . . . . . 21  R  Po  S  Po  a  b 
c  d  e  a  a 
b  b  a R a  a  a  b S b
16 an4 520 . . . . . . . . . . . . . . . . . . . . . 22  a  c 
b  d  a R c  a  c  b S d  c  e  d  c R e  c  e  d S  a  c  b  d  c  e  d  a R c  a  c  b S d  c R e  c  e  d S
17 3an6 1216 . . . . . . . . . . . . . . . . . . . . . . . . 25  a  b  c  d 
e  a  c  e 
b  d
18 potr 4036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  R  Po  a  c  e  a R c  c R e  a R e
19183impia 1100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  R  Po  a  c  e  a R c  c R e  a R e
2019orcd 651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  R  Po  a  c  e  a R c  c R e  a R e  a  e  b S
21203expia 1105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  R  Po  a  c  e  a R c  c R e  a R e  a  e  b S
2221expdimp 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  R  Po  a  c  e  a R c  c R e  a R e  a  e  b S
23 breq2 3759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  c  e 
a R c  a R e
2423biimpa 280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  c  e  a R c  a R e
2524orcd 651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  c  e  a R c  a R e  a  e  b S
2625expcom 109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  a R c 
c  e  a R e  a  e  b S
2726adantrd 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  a R c  c  e  d S  a R e  a  e  b S
2827adantl 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  R  Po  a  c  e  a R c  c  e  d S  a R e  a  e  b S
2922, 28jaod 636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  R  Po  a  c  e  a R c  c R e  c  e  d S  a R e  a  e  b S
3029ex 108 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  R  Po  a  c  e 
a R c  c R e  c  e  d S  a R e  a  e  b S
31 potr 4036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  S  Po  b  d  b S d  d S  b S
3231expdimp 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  S  Po  b  d  b S d  d S  b S
3332anim2d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  S  Po  b  d  b S d  c  e  d S  c  e  b S
3433orim2d 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  S  Po  b  d  b S d  c R e  c  e  d S  c R e  c  e  b S
35 breq1 3758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  a  c 
a R e  c R e
36 equequ1 1595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  a  c 
a  e  c  e
3736anbi1d 438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  a  c  a  e  b S  c  e  b S
3835, 37orbi12d 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  a  c  a R e  a  e  b S  c R e 
c  e  b S
3938imbi2d 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  a  c  c R e  c  e  d S  a R e  a  e  b S  c R e  c  e  d S  c R e  c  e  b S
4034, 39syl5ibr 145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  a  c  S  Po  b  d  b S d  c R e  c  e  d S  a R e  a  e  b S
4140expd 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  a  c  S  Po  b  d 
b S d  c R e  c  e  d S  a R e  a  e  b S
4241com12 27 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  S  Po  b  d 
a  c  b S d  c R e  c  e  d S  a R e  a  e  b S
4342impd 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  S  Po  b  d  a  c  b S d  c R e  c  e  d S  a R e  a  e  b S
4430, 43jaao 638 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  R  Po  a  c  e  S  Po  b  d  a R c  a  c  b S d  c R e  c  e  d S  a R e  a  e  b S
4544impd 242 . . . . . . . . . . . . . . . . . . . . . . . . . 26  R  Po  a  c  e  S  Po  b  d  a R c  a  c  b S d  c R e  c  e  d S  a R e  a  e  b S
4645an4s 522 . . . . . . . . . . . . . . . . . . . . . . . . 25  R  Po  S  Po  a  c  e 
b  d  a R c  a  c  b S d  c R e  c  e  d S  a R e  a  e  b S
4717, 46sylan2b 271 . . . . . . . . . . . . . . . . . . . . . . . 24  R  Po  S  Po  a  b 
c  d  e  a R c  a  c  b S d  c R e  c  e  d S  a R e  a  e  b S
48 an4 520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  a  b  e  a  e  b
4948biimpi 113 . . . . . . . . . . . . . . . . . . . . . . . . . 26  a  b  e  a  e  b
50493adant2 922 . . . . . . . . . . . . . . . . . . . . . . . . 25  a  b  c  d 
e  a  e 
b
5150adantl 262 . . . . . . . . . . . . . . . . . . . . . . . 24  R  Po  S  Po  a  b 
c  d  e  a  e  b
5247, 51jctild 299 . . . . . . . . . . . . . . . . . . . . . . 23  R  Po  S  Po  a  b 
c  d  e  a R c  a  c  b S d  c R e  c  e  d S  a  e 
b  a R e  a  e  b S
5352adantld 263 . . . . . . . . . . . . . . . . . . . . . 22  R  Po  S  Po  a  b 
c  d  e  a  c 
b  d  c  e 
d  a R c  a  c  b S d  c R e  c  e  d S  a  e  b  a R e  a  e  b S
5416, 53syl5bi 141 . . . . . . . . . . . . . . . . . . . . 21  R  Po  S  Po  a  b 
c  d  e  a  c 
b  d  a R c  a  c  b S d  c  e  d  c R e  c  e  d S  a  e  b  a R e  a  e  b S
5515, 54jca 290 . . . . . . . . . . . . . . . . . . . 20  R  Po  S  Po  a  b 
c  d  e  a  a 
b  b  a R a  a  a  b S b  a  c 
b  d  a R c  a  c  b S d  c  e  d  c R e  c  e  d S  a  e  b  a R e  a  e  b S
56 breq12 3760 . . . . . . . . . . . . . . . . . . . . . . . . 25  t  <. a ,  b >.  t  <. a ,  b
>. 
t T t  <. a ,  b >. T <. a ,  b >.
5756anidms 377 . . . . . . . . . . . . . . . . . . . . . . . 24  t  <. a ,  b
>.  t T t  <. a ,  b
>. T <. a ,  b
>.
5857notbid 591 . . . . . . . . . . . . . . . . . . . . . . 23  t  <. a ,  b
>.  t T t  <. a ,  b >. T <. a ,  b >.
59583ad2ant1 924 . . . . . . . . . . . . . . . . . . . . . 22  t  <. a ,  b >.  <. c ,  d
>.  <. e ,  >.  t T t  <. a ,  b >. T <. a ,  b >.
60 breq12 3760 . . . . . . . . . . . . . . . . . . . . . . . . 25  t  <. a ,  b >.  <. c ,  d
>. 
t T  <. a ,  b >. T <. c ,  d >.
61603adant3 923 . . . . . . . . . . . . . . . . . . . . . . . 24  t  <. a ,  b >.  <. c ,  d
>.  <. e ,  >.  t T 
<. a ,  b >. T <. c ,  d
>.
62 breq12 3760 . . . . . . . . . . . . . . . . . . . . . . . . 25  <. c ,  d >.  <. e , 
>.  T  <. c ,  d >. T <. e ,  >.
63623adant1 921 . . . . . . . . . . . . . . . . . . . . . . . 24  t  <. a ,  b >.  <. c ,  d
>.  <. e ,  >.  T 
<. c ,  d >. T <. e , 
>.
6461, 63anbi12d 442 . . . . . . . . . . . . . . . . . . . . . . 23  t  <. a ,  b >.  <. c ,  d
>.  <. e ,  >.  t T  T  <. a ,  b >. T <. c ,  d >.  <. c ,  d >. T <. e ,  >.
65 breq12 3760 . . . . . . . . . . . . . . . . . . . . . . . 24  t  <. a ,  b >.  <. e , 
>. 
t T  <. a ,  b >. T <. e ,  >.
66653adant2 922 . . . . . . . . . . . . . . . . . . . . . . 23  t  <. a ,  b >.  <. c ,  d
>.  <. e ,  >.  t T 
<. a ,  b >. T <. e , 
>.
6764, 66imbi12d 223 . . . . . . . . . . . . . . . . . . . . . 22  t  <. a ,  b >.  <. c ,  d
>.  <. e ,  >.  t T  T  t T  <. a ,  b >. T <. c ,  d >.  <. c ,  d >. T <. e ,  >.  <. a ,  b
>. T <. e , 
>.
6859, 67anbi12d 442 . . . . . . . . . . . . . . . . . . . . 21  t  <. a ,  b >.  <. c ,  d
>.  <. e ,  >.  t T t  t T  T  t T  <. a ,  b >. T <. a ,  b >.  <. a ,  b
>. T <. c ,  d
>.  <. c ,  d
>. T <. e , 
>.  <. a ,  b >. T <. e ,  >.
69 poxp.1 . . . . . . . . . . . . . . . . . . . . . . . 24  T  { <. , 
>.  |  X.  X.  1st `  R 1st `  1st `  1st `  2nd `  S 2nd `  }
7069xporderlem 5793 . . . . . . . . . . . . . . . . . . . . . . 23  <. a ,  b >. T <. a ,  b >.  a  a  b  b  a R a  a  a  b S b
7170notbii 593 . . . . . . . . . . . . . . . . . . . . . 22 
<. a ,  b >. T <. a ,  b
>.  a  a  b  b 
a R a  a  a  b S b
7269xporderlem 5793 . . . . . . . . . . . . . . . . . . . . . . . 24  <. a ,  b >. T <. c ,  d >.  a  c  b  d  a R c  a  c  b S d
7369xporderlem 5793 . . . . . . . . . . . . . . . . . . . . . . . 24  <. c ,  d >. T <. e ,  >.  c  e  d  c R e  c  e  d S
7472, 73anbi12i 433 . . . . . . . . . . . . . . . . . . . . . . 23 
<. a ,  b >. T <. c ,  d
>.  <. c ,  d
>. T <. e , 
>.  a  c  b  d  a R c  a  c  b S d  c  e 
d  c R e  c  e  d S
7569xporderlem 5793 . . . . . . . . . . . . . . . . . . . . . . 23  <. a ,  b >. T <. e ,  >.  a  e  b  a R e  a  e  b S
7674, 75imbi12i 228 . . . . . . . . . . . . . . . . . . . . . 22  <. a ,  b
>. T <. c ,  d
>.  <. c ,  d
>. T <. e , 
>.  <. a ,  b >. T <. e ,  >.  a  c  b  d 
a R c  a  c  b S d  c  e  d  c R e  c  e  d S  a  e  b  a R e  a  e  b S
7771, 76anbi12i 433 . . . . . . . . . . . . . . . . . . . . 21  <. a ,  b
>. T <. a ,  b
>.  <. a ,  b >. T <. c ,  d >.  <. c ,  d >. T <. e ,  >.  <. a ,  b
>. T <. e , 
>.  a  a 
b  b  a R a  a  a  b S b  a  c 
b  d  a R c  a  c  b S d  c  e  d  c R e  c  e  d S  a  e  b  a R e  a  e  b S
7868, 77syl6bb 185 . . . . . . . . . . . . . . . . . . . 20  t  <. a ,  b >.  <. c ,  d
>.  <. e ,  >.  t T t  t T  T  t T  a  a  b  b  a R a  a  a  b S b  a  c  b  d  a R c  a  c  b S d  c  e 
d  c R e  c  e  d S  a  e  b  a R e  a  e  b S
7955, 78syl5ibr 145 . . . . . . . . . . . . . . . . . . 19  t  <. a ,  b >.  <. c ,  d
>.  <. e ,  >.  R  Po  S  Po  a  b  c  d 
e  t T t  t T  T  t T
8079expcomd 1327 . . . . . . . . . . . . . . . . . 18  t  <. a ,  b >.  <. c ,  d
>.  <. e ,  >.  a  b 
c  d  e  R  Po  S  Po  t T t  t T  T  t T
8180imp 115 . . . . . . . . . . . . . . . . 17  t  <. a ,  b >.  <. c ,  d
>.  <. e ,  >.  a  b 
c  d  e  R  Po  S  Po  t T t  t T  T  t T
824, 81sylbi 114 . . . . . . . . . . . . . . . 16  t  <. a ,  b >. 
a  b 
<. c ,  d >.  c  d  <. e ,  >. 
e  R  Po  S  Po  t T t  t T  T  t T
83823exp 1102 . . . . . . . . . . . . . . 15  t  <. a ,  b >. 
a  b  <. c ,  d
>.  c  d  <. e ,  >. 
e  R  Po  S  Po  t T t  t T  T  t T
8483com3l 75 . . . . . . . . . . . . . 14  <. c ,  d >. 
c  d  <. e , 
>.  e  t  <. a ,  b >. 
a  b  R  Po  S  Po  t T t  t T  T  t T
8584exlimivv 1773 . . . . . . . . . . . . 13  c d  <. c ,  d
>.  c  d  <. e ,  >. 
e  t  <. a ,  b
>.  a  b  R  Po  S  Po  t T t  t T  T  t T
8685com3l 75 . . . . . . . . . . . 12  <. e ,  >. 
e  t  <. a ,  b
>.  a  b  c d  <. c ,  d >. 
c  d  R  Po  S  Po  t T t  t T  T  t T
8786exlimivv 1773 . . . . . . . . . . 11  e  <. e , 
>.  e  t  <. a ,  b >. 
a  b  c d 
<. c ,  d >.  c  d  R  Po  S  Po  t T t  t T  T  t T
8887com3l 75 . . . . . . . . . 10  t  <. a ,  b >. 
a  b  c d 
<. c ,  d >.  c  d  e  <. e ,  >. 
e  R  Po  S  Po  t T t  t T  T  t T
8988exlimivv 1773 . . . . . . . . 9  a b t  <. a ,  b
>.  a  b  c d  <. c ,  d >. 
c  d  e 
<. e ,  >.  e  R  Po  S  Po  t T t  t T  T  t T
90893imp 1097 . . . . . . . 8  a b t  <. a ,  b >. 
a  b  c d 
<. c ,  d >.  c  d  e 
<. e ,  >.  e  R  Po  S  Po  t T t  t T  T  t T
911, 2, 3, 90syl3anb 1177 . . . . . . 7  t  X.  X.  X.  R  Po  S  Po  t T t  t T  T  t T
92913expia 1105 . . . . . 6  t  X.  X.  X.  R  Po  S  Po  t T t  t T  T  t T
9392com3r 73 . . . . 5  R  Po  S  Po  t  X.  X.  X.  t T t  t T  T  t T
9493imp 115 . . . 4  R  Po  S  Po  t  X.  X.  X.  t T t  t T  T  t T
9594ralrimiv 2385 . . 3  R  Po  S  Po  t  X.  X.  X.  t T t  t T  T  t T
9695ralrimivva 2395 . 2  R  Po  S  Po  t  X.  X.  X.  t T t  t T  T  t T
97 df-po 4024 . 2  T  Po  X.  t  X.  X.  X.  t T t  t T  T  t T
9896, 97sylibr 137 1  R  Po  S  Po  T  Po  X.
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 97   wb 98   wo 628   w3a 884   wceq 1242  wex 1378   wcel 1390  wral 2300   <.cop 3370   class class class wbr 3755   {copab 3808    Po wpo 4022    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-in1 544  ax-in2 545  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-po 4024  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: (None)
  Copyright terms: Public domain W3C validator