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

Theorem recexprlemss1l 6459
Description: The lower cut of A ·P B is a subset of the lower cut of one. Lemma for recexpr 6462. (Contributed by Jim Kingdon, 27-Dec-2019.)
Hypothesis
Ref Expression
recexpr.1 B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩
Assertion
Ref Expression
recexprlemss1l (A P → (1st ‘(A ·P B)) ⊆ (1st ‘1P))
Distinct variable groups:   x,y,A   x,B,y

Proof of Theorem recexprlemss1l
Dummy variables 𝑞 z w u f g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 recexpr.1 . . . . . 6 B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩
21recexprlempr 6456 . . . . 5 (A PB P)
3 df-imp 6312 . . . . . 6 ·P = (y P, w P ↦ ⟨{u Qf Q g Q (f (1sty) g (1stw) u = (f ·Q g))}, {u Qf Q g Q (f (2ndy) g (2ndw) u = (f ·Q g))}⟩)
4 mulclnq 6224 . . . . . 6 ((f Q g Q) → (f ·Q g) Q)
53, 4genpelvl 6355 . . . . 5 ((A P B P) → (w (1st ‘(A ·P B)) ↔ z (1stA)𝑞 (1stB)w = (z ·Q 𝑞)))
62, 5mpdan 398 . . . 4 (A P → (w (1st ‘(A ·P B)) ↔ z (1stA)𝑞 (1stB)w = (z ·Q 𝑞)))
71recexprlemell 6446 . . . . . . . 8 (𝑞 (1stB) ↔ y(𝑞 <Q y (*Qy) (2ndA)))
8 ltrelnq 6213 . . . . . . . . . . . . . 14 <Q ⊆ (Q × Q)
98brel 4310 . . . . . . . . . . . . 13 (𝑞 <Q y → (𝑞 Q y Q))
109simprd 107 . . . . . . . . . . . 12 (𝑞 <Q yy Q)
11 prop 6318 . . . . . . . . . . . . . . . . . 18 (A P → ⟨(1stA), (2ndA)⟩ P)
12 elprnql 6324 . . . . . . . . . . . . . . . . . 18 ((⟨(1stA), (2ndA)⟩ P z (1stA)) → z Q)
1311, 12sylan 267 . . . . . . . . . . . . . . . . 17 ((A P z (1stA)) → z Q)
14 ltmnqi 6251 . . . . . . . . . . . . . . . . . 18 ((𝑞 <Q y z Q) → (z ·Q 𝑞) <Q (z ·Q y))
1514expcom 109 . . . . . . . . . . . . . . . . 17 (z Q → (𝑞 <Q y → (z ·Q 𝑞) <Q (z ·Q y)))
1613, 15syl 14 . . . . . . . . . . . . . . . 16 ((A P z (1stA)) → (𝑞 <Q y → (z ·Q 𝑞) <Q (z ·Q y)))
1716adantr 261 . . . . . . . . . . . . . . 15 (((A P z (1stA)) y Q) → (𝑞 <Q y → (z ·Q 𝑞) <Q (z ·Q y)))
18 prltlu 6330 . . . . . . . . . . . . . . . . . . 19 ((⟨(1stA), (2ndA)⟩ P z (1stA) (*Qy) (2ndA)) → z <Q (*Qy))
1911, 18syl3an1 1151 . . . . . . . . . . . . . . . . . 18 ((A P z (1stA) (*Qy) (2ndA)) → z <Q (*Qy))
20193expia 1089 . . . . . . . . . . . . . . . . 17 ((A P z (1stA)) → ((*Qy) (2ndA) → z <Q (*Qy)))
2120adantr 261 . . . . . . . . . . . . . . . 16 (((A P z (1stA)) y Q) → ((*Qy) (2ndA) → z <Q (*Qy)))
22 ltmnqi 6251 . . . . . . . . . . . . . . . . . . . . 21 ((z <Q (*Qy) y Q) → (y ·Q z) <Q (y ·Q (*Qy)))
2322expcom 109 . . . . . . . . . . . . . . . . . . . 20 (y Q → (z <Q (*Qy) → (y ·Q z) <Q (y ·Q (*Qy))))
2423adantr 261 . . . . . . . . . . . . . . . . . . 19 ((y Q z Q) → (z <Q (*Qy) → (y ·Q z) <Q (y ·Q (*Qy))))
25 mulcomnqg 6231 . . . . . . . . . . . . . . . . . . . 20 ((y Q z Q) → (y ·Q z) = (z ·Q y))
26 recidnq 6241 . . . . . . . . . . . . . . . . . . . . 21 (y Q → (y ·Q (*Qy)) = 1Q)
2726adantr 261 . . . . . . . . . . . . . . . . . . . 20 ((y Q z Q) → (y ·Q (*Qy)) = 1Q)
2825, 27breq12d 3743 . . . . . . . . . . . . . . . . . . 19 ((y Q z Q) → ((y ·Q z) <Q (y ·Q (*Qy)) ↔ (z ·Q y) <Q 1Q))
2924, 28sylibd 138 . . . . . . . . . . . . . . . . . 18 ((y Q z Q) → (z <Q (*Qy) → (z ·Q y) <Q 1Q))
3029ancoms 255 . . . . . . . . . . . . . . . . 17 ((z Q y Q) → (z <Q (*Qy) → (z ·Q y) <Q 1Q))
3113, 30sylan 267 . . . . . . . . . . . . . . . 16 (((A P z (1stA)) y Q) → (z <Q (*Qy) → (z ·Q y) <Q 1Q))
3221, 31syld 40 . . . . . . . . . . . . . . 15 (((A P z (1stA)) y Q) → ((*Qy) (2ndA) → (z ·Q y) <Q 1Q))
3317, 32anim12d 318 . . . . . . . . . . . . . 14 (((A P z (1stA)) y Q) → ((𝑞 <Q y (*Qy) (2ndA)) → ((z ·Q 𝑞) <Q (z ·Q y) (z ·Q y) <Q 1Q)))
34 ltsonq 6246 . . . . . . . . . . . . . . 15 <Q Or Q
3534, 8sotri 4638 . . . . . . . . . . . . . 14 (((z ·Q 𝑞) <Q (z ·Q y) (z ·Q y) <Q 1Q) → (z ·Q 𝑞) <Q 1Q)
3633, 35syl6 29 . . . . . . . . . . . . 13 (((A P z (1stA)) y Q) → ((𝑞 <Q y (*Qy) (2ndA)) → (z ·Q 𝑞) <Q 1Q))
3736exp4b 349 . . . . . . . . . . . 12 ((A P z (1stA)) → (y Q → (𝑞 <Q y → ((*Qy) (2ndA) → (z ·Q 𝑞) <Q 1Q))))
3810, 37syl5 28 . . . . . . . . . . 11 ((A P z (1stA)) → (𝑞 <Q y → (𝑞 <Q y → ((*Qy) (2ndA) → (z ·Q 𝑞) <Q 1Q))))
3938pm2.43d 44 . . . . . . . . . 10 ((A P z (1stA)) → (𝑞 <Q y → ((*Qy) (2ndA) → (z ·Q 𝑞) <Q 1Q)))
4039impd 242 . . . . . . . . 9 ((A P z (1stA)) → ((𝑞 <Q y (*Qy) (2ndA)) → (z ·Q 𝑞) <Q 1Q))
4140exlimdv 1676 . . . . . . . 8 ((A P z (1stA)) → (y(𝑞 <Q y (*Qy) (2ndA)) → (z ·Q 𝑞) <Q 1Q))
427, 41syl5bi 141 . . . . . . 7 ((A P z (1stA)) → (𝑞 (1stB) → (z ·Q 𝑞) <Q 1Q))
43 breq1 3733 . . . . . . . 8 (w = (z ·Q 𝑞) → (w <Q 1Q ↔ (z ·Q 𝑞) <Q 1Q))
4443biimprcd 149 . . . . . . 7 ((z ·Q 𝑞) <Q 1Q → (w = (z ·Q 𝑞) → w <Q 1Q))
4542, 44syl6 29 . . . . . 6 ((A P z (1stA)) → (𝑞 (1stB) → (w = (z ·Q 𝑞) → w <Q 1Q)))
4645expimpd 345 . . . . 5 (A P → ((z (1stA) 𝑞 (1stB)) → (w = (z ·Q 𝑞) → w <Q 1Q)))
4746rexlimdvv 2411 . . . 4 (A P → (z (1stA)𝑞 (1stB)w = (z ·Q 𝑞) → w <Q 1Q))
486, 47sylbid 139 . . 3 (A P → (w (1st ‘(A ·P B)) → w <Q 1Q))
49 1prl 6394 . . . 4 (1st ‘1P) = {ww <Q 1Q}
5049abeq2i 2124 . . 3 (w (1st ‘1P) ↔ w <Q 1Q)
5148, 50syl6ibr 151 . 2 (A P → (w (1st ‘(A ·P B)) → w (1st ‘1P)))
5251ssrdv 2922 1 (A P → (1st ‘(A ·P B)) ⊆ (1st ‘1P))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1226  wex 1357   wcel 1369  {cab 2002  wrex 2279  wss 2888  cop 3345   class class class wbr 3730  cfv 4820  (class class class)co 5427  1st c1st 5679  2nd c2nd 5680  Qcnq 6129  1Qc1q 6130   ·Q cmq 6132  *Qcrq 6133   <Q cltq 6134  Pcnp 6140  1Pc1p 6141   ·P cmp 6143
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 529  ax-in2 530  ax-io 614  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1358  ax-ie2 1359  ax-8 1371  ax-10 1372  ax-11 1373  ax-i12 1374  ax-bnd 1375  ax-4 1376  ax-13 1380  ax-14 1381  ax-17 1395  ax-i9 1399  ax-ial 1403  ax-i5r 1404  ax-ext 1998  ax-coll 3838  ax-sep 3841  ax-nul 3849  ax-pow 3893  ax-pr 3910  ax-un 4111  ax-setind 4195  ax-iinf 4229
This theorem depends on definitions:  df-bi 110  df-dc 727  df-3or 870  df-3an 871  df-tru 1229  df-fal 1232  df-nf 1326  df-sb 1622  df-eu 1879  df-mo 1880  df-clab 2003  df-cleq 2009  df-clel 2012  df-nfc 2143  df-ne 2182  df-ral 2283  df-rex 2284  df-reu 2285  df-rab 2287  df-v 2531  df-sbc 2736  df-csb 2824  df-dif 2891  df-un 2893  df-in 2895  df-ss 2902  df-nul 3196  df-pw 3328  df-sn 3348  df-pr 3349  df-op 3351  df-uni 3547  df-int 3582  df-iun 3625  df-br 3731  df-opab 3785  df-mpt 3786  df-tr 3821  df-eprel 3992  df-id 3996  df-po 3999  df-iso 4000  df-iord 4044  df-on 4046  df-suc 4049  df-iom 4232  df-xp 4269  df-rel 4270  df-cnv 4271  df-co 4272  df-dm 4273  df-rn 4274  df-res 4275  df-ima 4276  df-iota 4785  df-fun 4822  df-fn 4823  df-f 4824  df-f1 4825  df-fo 4826  df-f1o 4827  df-fv 4828  df-ov 5430  df-oprab 5431  df-mpt2 5432  df-1st 5681  df-2nd 5682  df-recs 5833  df-irdg 5869  df-1o 5907  df-oadd 5911  df-omul 5912  df-er 6008  df-ec 6010  df-qs 6014  df-ni 6153  df-pli 6154  df-mi 6155  df-lti 6156  df-plpq 6192  df-mpq 6193  df-enq 6195  df-nqqs 6196  df-plqqs 6197  df-mqqs 6198  df-1nqqs 6199  df-rq 6200  df-ltnqqs 6201  df-inp 6309  df-i1p 6310  df-imp 6312
This theorem is referenced by:  recexprlemex  6461
  Copyright terms: Public domain W3C validator