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

Theorem genpassu 6508
Description: Associativity of upper cuts. Lemma for genpassg 6509. (Contributed by Jim Kingdon, 11-Dec-2019.)
Hypotheses
Ref Expression
genpelvl.1  F  P. ,  P.  |->  <. {  Q.  |  Q.  Q.  1st `  1st `  G } ,  {  Q.  |  Q.  Q.  2nd `  2nd `  G } >.
genpelvl.2  Q.  Q.  G  Q.
genpassg.4  dom  F  P.  X.  P.
genpassg.5  P.  P.  F  P.
genpassg.6  Q.  Q.  h  Q.  G G h  G G h
Assertion
Ref Expression
genpassu  P.  P.  C  P.  2nd `  F F C  2nd `  F F C
Distinct variable groups:   ,,,,, h,,,   ,,,,,, h,,   , G,,,,, h,,   , F,    C,,, h,,,,,    h, F,,,,,

Proof of Theorem genpassu
Dummy variable  t is distinct from all other variables.
StepHypRef Expression
1 prop 6458 . . . . . . . . 9  P.  <. 1st `  ,  2nd `  >.  P.
2 elprnqu 6465 . . . . . . . . 9 
<. 1st `  ,  2nd `  >.  P.  2nd `  Q.
31, 2sylan 267 . . . . . . . 8  P.  2nd `  Q.
4 prop 6458 . . . . . . . . . . . . . . . 16  P.  <. 1st `  ,  2nd `  >.  P.
5 elprnqu 6465 . . . . . . . . . . . . . . . 16 
<. 1st `  ,  2nd `  >.  P.  2nd `  Q.
64, 5sylan 267 . . . . . . . . . . . . . . 15  P.  2nd `  Q.
7 r19.41v 2460 . . . . . . . . . . . . . . . . 17  h  2nd `  C t  G h  G t  h  2nd `  C t  G h  G t
8 prop 6458 . . . . . . . . . . . . . . . . . . . . 21  C  P.  <. 1st `  C ,  2nd `  C >.  P.
9 elprnqu 6465 . . . . . . . . . . . . . . . . . . . . 21 
<. 1st `  C ,  2nd `  C >.  P.  h  2nd `  C 
h  Q.
108, 9sylan 267 . . . . . . . . . . . . . . . . . . . 20  C  P.  h  2nd `  C 
h  Q.
11 oveq2 5463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  t  G h  G t  G G h
1211adantr 261 . . . . . . . . . . . . . . . . . . . . . . . . 25  t  G h  Q.  Q.  h  Q.  G t  G G h
13 genpassg.6 . . . . . . . . . . . . . . . . . . . . . . . . . 26  Q.  Q.  h  Q.  G G h  G G h
1413adantl 262 . . . . . . . . . . . . . . . . . . . . . . . . 25  t  G h  Q.  Q.  h  Q.  G G h  G G h
1512, 14eqtr4d 2072 . . . . . . . . . . . . . . . . . . . . . . . 24  t  G h  Q.  Q.  h  Q.  G t  G G h
1615eqeq2d 2048 . . . . . . . . . . . . . . . . . . . . . . 23  t  G h  Q.  Q.  h  Q.  G t  G G h
1716expcom 109 . . . . . . . . . . . . . . . . . . . . . 22  Q.  Q.  h  Q. 
t  G h  G t  G G h
1817pm5.32d 423 . . . . . . . . . . . . . . . . . . . . 21  Q.  Q.  h  Q.  t  G h  G t  t  G h  G G h
19183expa 1103 . . . . . . . . . . . . . . . . . . . 20  Q.  Q.  h  Q.  t  G h  G t  t  G h  G G h
2010, 19sylan2 270 . . . . . . . . . . . . . . . . . . 19  Q.  Q.  C  P.  h  2nd `  C  t  G h  G t  t  G h  G G h
2120anassrs 380 . . . . . . . . . . . . . . . . . 18 
Q.  Q.  C 
P.  h  2nd `  C  t  G h  G t  t  G h  G G h
2221rexbidva 2317 . . . . . . . . . . . . . . . . 17  Q.  Q.  C  P.  h  2nd `  C t  G h  G t  h  2nd `  C t  G h  G G h
237, 22syl5rbbr 184 . . . . . . . . . . . . . . . 16  Q.  Q.  C  P.  h  2nd `  C t  G h  G G h  h  2nd `  C t  G h  G t
2423an32s 502 . . . . . . . . . . . . . . 15  Q.  C  P.  Q.  h  2nd `  C t  G h  G G h  h  2nd `  C t  G h  G t
256, 24sylan2 270 . . . . . . . . . . . . . 14  Q.  C  P.  P.  2nd `  h  2nd `  C t  G h  G G h  h  2nd `  C t  G h  G t
2625anassrs 380 . . . . . . . . . . . . 13 
Q.  C  P.  P.  2nd `  h  2nd `  C t  G h  G G h  h  2nd `  C t  G h  G t
2726rexbidva 2317 . . . . . . . . . . . 12  Q.  C  P.  P.  2nd `  h  2nd `  C t  G h  G G h  2nd `  h  2nd `  C t  G h  G t
28 r19.41v 2460 . . . . . . . . . . . 12  2nd `  h  2nd `  C t  G h  G t  2nd `  h  2nd `  C t  G h  G t
2927, 28syl6bb 185 . . . . . . . . . . 11  Q.  C  P.  P.  2nd `  h  2nd `  C t  G h  G G h  2nd `  h  2nd `  C t  G h  G t
3029an31s 504 . . . . . . . . . 10  P.  C  P.  Q.  2nd `  h  2nd `  C t  G h  G G h  2nd `  h  2nd `  C t  G h  G t
3130exbidv 1703 . . . . . . . . 9  P.  C  P.  Q.  t  2nd `  h  2nd `  C t  G h  G G h  t  2nd `  h  2nd `  C t  G h  G t
32 genpelvl.2 . . . . . . . . . . . . . . . . . . . . . . . 24  Q.  Q.  G  Q.
3332caovcl 5597 . . . . . . . . . . . . . . . . . . . . . . 23  Q.  h  Q.  G h  Q.
34 elisset 2562 . . . . . . . . . . . . . . . . . . . . . . 23  G h  Q.  t  t  G h
3533, 34syl 14 . . . . . . . . . . . . . . . . . . . . . 22  Q.  h  Q.  t  t  G h
3635biantrurd 289 . . . . . . . . . . . . . . . . . . . . 21  Q.  h  Q.  G G h  t  t  G h  G G h
37 19.41v 1779 . . . . . . . . . . . . . . . . . . . . 21  t t  G h  G G h  t  t  G h  G G h
3836, 37syl6bbr 187 . . . . . . . . . . . . . . . . . . . 20  Q.  h  Q.  G G h  t t  G h  G G h
3910, 38sylan2 270 . . . . . . . . . . . . . . . . . . 19  Q.  C  P.  h  2nd `  C  G G h  t t  G h  G G h
4039anassrs 380 . . . . . . . . . . . . . . . . . 18  Q.  C  P.  h  2nd `  C  G G h  t t  G h  G G h
4140rexbidva 2317 . . . . . . . . . . . . . . . . 17  Q.  C  P.  h  2nd `  C  G G h  h  2nd `  C t t  G h  G G h
42 rexcom4 2571 . . . . . . . . . . . . . . . . 17  h  2nd `  C t t  G h  G G h  t h  2nd `  C t  G h  G G h
4341, 42syl6bb 185 . . . . . . . . . . . . . . . 16  Q.  C  P.  h  2nd `  C  G G h  t h  2nd `  C t  G h  G G h
4443ancoms 255 . . . . . . . . . . . . . . 15  C  P.  Q.  h  2nd `  C  G G h  t h  2nd `  C t  G h  G G h
456, 44sylan2 270 . . . . . . . . . . . . . 14  C  P.  P.  2nd `  h  2nd `  C  G G h  t h  2nd `  C t  G h  G G h
4645anassrs 380 . . . . . . . . . . . . 13  C  P.  P.  2nd `  h  2nd `  C  G G h  t h  2nd `  C t  G h  G G h
4746rexbidva 2317 . . . . . . . . . . . 12  C  P.  P.  2nd `  h  2nd `  C  G G h  2nd `  t h  2nd `  C t  G h  G G h
4847ancoms 255 . . . . . . . . . . 11  P.  C  P.  2nd `  h  2nd `  C  G G h  2nd `  t h  2nd `  C t  G h  G G h
49 rexcom4 2571 . . . . . . . . . . 11  2nd `  t h  2nd `  C t  G h  G G h  t  2nd `  h  2nd `  C t  G h  G G h
5048, 49syl6bb 185 . . . . . . . . . 10  P.  C  P.  2nd `  h  2nd `  C  G G h  t  2nd `  h  2nd `  C t  G h  G G h
5150adantr 261 . . . . . . . . 9  P.  C  P.  Q.  2nd `  h  2nd `  C  G G h  t  2nd `  h  2nd `  C t  G h  G G h
52 df-rex 2306 . . . . . . . . . . 11  t  2nd `  F C  G t  t t  2nd `  F C  G t
53 genpelvl.1 . . . . . . . . . . . . . 14  F  P. ,  P.  |->  <. {  Q.  |  Q.  Q.  1st `  1st `  G } ,  {  Q.  |  Q.  Q.  2nd `  2nd `  G } >.
5453, 32genpelvu 6496 . . . . . . . . . . . . 13  P.  C  P.  t  2nd `  F C  2nd `  h  2nd `  C t  G h
5554anbi1d 438 . . . . . . . . . . . 12  P.  C  P.  t  2nd `  F C  G t  2nd `  h  2nd `  C t  G h  G t
5655exbidv 1703 . . . . . . . . . . 11  P.  C  P.  t t  2nd `  F C  G t  t  2nd `  h  2nd `  C t  G h  G t
5752, 56syl5bb 181 . . . . . . . . . 10  P.  C  P.  t  2nd `  F C  G t  t  2nd `  h  2nd `  C t  G h  G t
5857adantr 261 . . . . . . . . 9  P.  C  P.  Q.  t  2nd `  F C  G t  t  2nd `  h  2nd `  C t  G h  G t
5931, 51, 583bitr4rd 210 . . . . . . . 8  P.  C  P.  Q.  t  2nd `  F C  G t  2nd `  h  2nd `  C  G G h
603, 59sylan2 270 . . . . . . 7  P.  C  P.  P.  2nd `  t  2nd `  F C  G t  2nd `  h  2nd `  C  G G h
6160anassrs 380 . . . . . 6  P.  C  P.  P.  2nd `  t  2nd `  F C  G t  2nd `  h  2nd `  C  G G h
6261rexbidva 2317 . . . . 5  P.  C  P.  P.  2nd `  t  2nd `  F C  G t  2nd `  2nd `  h  2nd `  C  G G h
6362ancoms 255 . . . 4  P.  P.  C  P.  2nd `  t  2nd `  F C  G t  2nd `  2nd `  h  2nd `  C  G G h
64633impb 1099 . . 3  P.  P.  C  P.  2nd `  t  2nd `  F C  G t  2nd `  2nd `  h  2nd `  C  G G h
65 genpassg.5 . . . . . 6  P.  P.  F  P.
6665caovcl 5597 . . . . 5  P.  C  P.  F C  P.
6753, 32genpelvu 6496 . . . . 5  P.  F C  P.  2nd `  F F C  2nd `  t  2nd `  F C  G t
6866, 67sylan2 270 . . . 4  P.  P.  C  P.  2nd `  F F C  2nd `  t  2nd `  F C  G t
69683impb 1099 . . 3  P.  P.  C  P.  2nd `  F F C  2nd `  t  2nd `  F C  G t
70 df-rex 2306 . . . . 5  t  2nd `  F h  2nd `  C 
t G h  t t  2nd `  F  h  2nd `  C  t G h
7153, 32genpelvu 6496 . . . . . . . 8  P.  P.  t  2nd `  F  2nd `  2nd `  t  G
72713adant3 923 . . . . . . 7  P.  P.  C  P. 
t  2nd `  F  2nd `  2nd `  t  G
7372anbi1d 438 . . . . . 6  P.  P.  C  P.  t  2nd `  F  h  2nd `  C  t G h  2nd `  2nd `  t  G  h  2nd `  C  t G h
7473exbidv 1703 . . . . 5  P.  P.  C  P.  t t  2nd `  F  h  2nd `  C  t G h  t  2nd `  2nd `  t  G  h  2nd `  C  t G h
7570, 74syl5bb 181 . . . 4  P.  P.  C  P.  t  2nd `  F h  2nd `  C 
t G h  t  2nd `  2nd `  t  G  h  2nd `  C  t G h
7665caovcl 5597 . . . . . 6  P.  P.  F  P.
7753, 32genpelvu 6496 . . . . . 6  F  P.  C  P.  2nd `  F F C  t  2nd `  F h  2nd `  C  t G h
7876, 77sylan 267 . . . . 5  P.  P.  C  P.  2nd `  F F C  t  2nd `  F h  2nd `  C  t G h
79783impa 1098 . . . 4  P.  P.  C  P.  2nd `  F F C  t  2nd `  F h  2nd `  C  t G h
8032caovcl 5597 . . . . . . . . . . . . . . . . . . 19  Q.  Q.  G  Q.
81 elisset 2562 . . . . . . . . . . . . . . . . . . 19  G  Q.  t  t  G
8280, 81syl 14 . . . . . . . . . . . . . . . . . 18  Q.  Q.  t  t  G
8382biantrurd 289 . . . . . . . . . . . . . . . . 17  Q.  Q.  h  2nd `  C  G G h  t  t  G  h  2nd `  C  G G h
84 oveq1 5462 . . . . . . . . . . . . . . . . . . . . . 22  t  G 
t G h  G G h
8584eqeq2d 2048 . . . . . . . . . . . . . . . . . . . . 21  t  G  t G h  G G h
8685rexbidv 2321 . . . . . . . . . . . . . . . . . . . 20  t  G  h  2nd `  C  t G h  h  2nd `  C  G G h
8786pm5.32i 427 . . . . . . . . . . . . . . . . . . 19  t  G  h  2nd `  C  t G h  t  G  h  2nd `  C  G G h
8887exbii 1493 . . . . . . . . . . . . . . . . . 18  t t  G  h  2nd `  C 
t G h  t t  G  h  2nd `  C  G G h
89 19.41v 1779 . . . . . . . . . . . . . . . . . 18  t t  G  h  2nd `  C  G G h  t  t  G  h  2nd `  C  G G h
9088, 89bitri 173 . . . . . . . . . . . . . . . . 17  t t  G  h  2nd `  C 
t G h  t 
t  G  h  2nd `  C  G G h
9183, 90syl6bbr 187 . . . . . . . . . . . . . . . 16  Q.  Q.  h  2nd `  C  G G h  t t  G  h  2nd `  C  t G h
926, 91sylan2 270 . . . . . . . . . . . . . . 15  Q.  P.  2nd `  h  2nd `  C  G G h  t t  G  h  2nd `  C  t G h
9392anassrs 380 . . . . . . . . . . . . . 14  Q.  P.  2nd `  h  2nd `  C  G G h  t t  G  h  2nd `  C  t G h
9493rexbidva 2317 . . . . . . . . . . . . 13  Q.  P.  2nd `  h  2nd `  C  G G h  2nd `  t t  G  h  2nd `  C  t G h
95 rexcom4 2571 . . . . . . . . . . . . 13  2nd `  t t  G  h  2nd `  C  t G h  t  2nd `  t  G  h  2nd `  C  t G h
9694, 95syl6bb 185 . . . . . . . . . . . 12  Q.  P.  2nd `  h  2nd `  C  G G h  t  2nd `  t  G  h  2nd `  C  t G h
9796ancoms 255 . . . . . . . . . . 11  P.  Q.  2nd `  h  2nd `  C  G G h  t  2nd `  t  G  h  2nd `  C  t G h
983, 97sylan2 270 . . . . . . . . . 10  P.  P.  2nd `  2nd `  h  2nd `  C  G G h  t  2nd `  t  G  h  2nd `  C  t G h
9998anassrs 380 . . . . . . . . 9  P.  P.  2nd `  2nd `  h  2nd `  C  G G h  t  2nd `  t  G  h  2nd `  C  t G h
10099rexbidva 2317 . . . . . . . 8  P.  P.  2nd `  2nd `  h  2nd `  C  G G h  2nd `  t  2nd `  t  G  h  2nd `  C  t G h
101 rexcom4 2571 . . . . . . . 8  2nd `  t  2nd `  t  G  h  2nd `  C  t G h  t  2nd `  2nd `  t  G  h  2nd `  C  t G h
102100, 101syl6bb 185 . . . . . . 7  P.  P.  2nd `  2nd `  h  2nd `  C  G G h  t  2nd `  2nd `  t  G  h  2nd `  C  t G h
103 r19.41v 2460 . . . . . . . . . 10  2nd `  t  G  h  2nd `  C  t G h  2nd `  t  G  h  2nd `  C 
t G h
104103rexbii 2325 . . . . . . . . 9  2nd `  2nd `  t  G  h  2nd `  C  t G h  2nd `  2nd `  t  G  h  2nd `  C  t G h
105 r19.41v 2460 . . . . . . . . 9  2nd `  2nd `  t  G  h  2nd `  C 
t G h  2nd `  2nd `  t  G  h  2nd `  C  t G h
106104, 105bitri 173 . . . . . . . 8  2nd `  2nd `  t  G  h  2nd `  C  t G h  2nd `  2nd `  t  G  h  2nd `  C  t G h
107106exbii 1493 . . . . . . 7  t  2nd `  2nd `  t  G  h  2nd `  C  t G h  t  2nd `  2nd `  t  G  h  2nd `  C  t G h
108102, 107syl6bb 185 . . . . . 6  P.  P.  2nd `  2nd `  h  2nd `  C  G G h  t  2nd `  2nd `  t  G  h  2nd `  C  t G h
109108ancoms 255 . . . . 5  P.  P.  2nd `  2nd `  h  2nd `  C  G G h  t  2nd `  2nd `  t  G  h  2nd `  C  t G h
1101093adant3 923 . . . 4  P.  P.  C  P.  2nd `  2nd `  h  2nd `  C  G G h  t  2nd `  2nd `  t  G  h  2nd `  C  t G h
11175, 79, 1103bitr4d 209 . . 3  P.  P.  C  P.  2nd `  F F C  2nd `  2nd `  h  2nd `  C  G G h
11264, 69, 1113bitr4rd 210 . 2  P.  P.  C  P.  2nd `  F F C  2nd `  F F C
113112eqrdv 2035 1  P.  P.  C  P.  2nd `  F F C  2nd `  F F C
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98   w3a 884   wceq 1242  wex 1378   wcel 1390  wrex 2301   {crab 2304   <.cop 3370    X. cxp 4286   dom cdm 4288   ` cfv 4845  (class class class)co 5455    |-> cmpt2 5457   1stc1st 5707   2ndc2nd 5708   Q.cnq 6264   P.cnp 6275
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-coll 3863  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  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-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  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-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-qs 6048  df-ni 6288  df-nqqs 6332  df-inp 6449
This theorem is referenced by:  genpassg  6509
  Copyright terms: Public domain W3C validator