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

Theorem recexprlemss1l 6607
 Description: The lower cut of A ·P B is a subset of the lower cut of one. Lemma for recexpr 6610. (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 6604 . . . . 5 (A PB P)
3 df-imp 6452 . . . . . 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 6360 . . . . . 6 ((f Q g Q) → (f ·Q g) Q)
53, 4genpelvl 6495 . . . . 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 6594 . . . . . . . 8 (𝑞 (1stB) ↔ y(𝑞 <Q y (*Qy) (2ndA)))
8 ltrelnq 6349 . . . . . . . . . . . . . 14 <Q ⊆ (Q × Q)
98brel 4335 . . . . . . . . . . . . 13 (𝑞 <Q y → (𝑞 Q y Q))
109simprd 107 . . . . . . . . . . . 12 (𝑞 <Q yy Q)
11 prop 6458 . . . . . . . . . . . . . . . . . 18 (A P → ⟨(1stA), (2ndA)⟩ P)
12 elprnql 6464 . . . . . . . . . . . . . . . . . 18 ((⟨(1stA), (2ndA)⟩ P z (1stA)) → z Q)
1311, 12sylan 267 . . . . . . . . . . . . . . . . 17 ((A P z (1stA)) → z Q)
14 ltmnqi 6387 . . . . . . . . . . . . . . . . . 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 6470 . . . . . . . . . . . . . . . . . . 19 ((⟨(1stA), (2ndA)⟩ P z (1stA) (*Qy) (2ndA)) → z <Q (*Qy))
1911, 18syl3an1 1167 . . . . . . . . . . . . . . . . . 18 ((A P z (1stA) (*Qy) (2ndA)) → z <Q (*Qy))
20193expia 1105 . . . . . . . . . . . . . . . . 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 6387 . . . . . . . . . . . . . . . . . . . . 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 6367 . . . . . . . . . . . . . . . . . . . 20 ((y Q z Q) → (y ·Q z) = (z ·Q y))
26 recidnq 6377 . . . . . . . . . . . . . . . . . . . . 21 (y Q → (y ·Q (*Qy)) = 1Q)
2726adantr 261 . . . . . . . . . . . . . . . . . . . 20 ((y Q z Q) → (y ·Q (*Qy)) = 1Q)
2825, 27breq12d 3768 . . . . . . . . . . . . . . . . . . 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 6382 . . . . . . . . . . . . . . 15 <Q Or Q
3534, 8sotri 4663 . . . . . . . . . . . . . 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 1697 . . . . . . . 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 3758 . . . . . . . 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 2433 . . . 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 6536 . . . 4 (1st ‘1P) = {ww <Q 1Q}
5049abeq2i 2145 . . 3 (w (1st ‘1P) ↔ w <Q 1Q)
5148, 50syl6ibr 151 . 2 (A P → (w (1st ‘(A ·P B)) → w (1st ‘1P)))
5251ssrdv 2945 1 (A P → (1st ‘(A ·P B)) ⊆ (1st ‘1P))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1242  ∃wex 1378   ∈ wcel 1390  {cab 2023  ∃wrex 2301   ⊆ wss 2911  ⟨cop 3370   class class class wbr 3755  ‘cfv 4845  (class class class)co 5455  1st c1st 5707  2nd c2nd 5708  Qcnq 6264  1Qc1q 6265   ·Q cmq 6267  *Qcrq 6268
 Copyright terms: Public domain W3C validator