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

Theorem recexprlemss1u 6608
 Description: The upper cut of A ·P B is a subset of the upper 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
recexprlemss1u (A P → (2nd ‘(A ·P B)) ⊆ (2nd ‘1P))
Distinct variable groups:   x,y,A   x,B,y

Proof of Theorem recexprlemss1u
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, 4genpelvu 6496 . . . . 5 ((A P B P) → (w (2nd ‘(A ·P B)) ↔ z (2ndA)𝑞 (2ndB)w = (z ·Q 𝑞)))
62, 5mpdan 398 . . . 4 (A P → (w (2nd ‘(A ·P B)) ↔ z (2ndA)𝑞 (2ndB)w = (z ·Q 𝑞)))
71recexprlemelu 6595 . . . . . . . 8 (𝑞 (2ndB) ↔ y(y <Q 𝑞 (*Qy) (1stA)))
8 ltrelnq 6349 . . . . . . . . . . . . . 14 <Q ⊆ (Q × Q)
98brel 4335 . . . . . . . . . . . . 13 (y <Q 𝑞 → (y Q 𝑞 Q))
109simpld 105 . . . . . . . . . . . 12 (y <Q 𝑞y Q)
11 prop 6458 . . . . . . . . . . . . . . . . . 18 (A P → ⟨(1stA), (2ndA)⟩ P)
12 elprnqu 6465 . . . . . . . . . . . . . . . . . 18 ((⟨(1stA), (2ndA)⟩ P z (2ndA)) → z Q)
1311, 12sylan 267 . . . . . . . . . . . . . . . . 17 ((A P z (2ndA)) → z Q)
14 ltmnqi 6387 . . . . . . . . . . . . . . . . . 18 ((y <Q 𝑞 z Q) → (z ·Q y) <Q (z ·Q 𝑞))
1514expcom 109 . . . . . . . . . . . . . . . . 17 (z Q → (y <Q 𝑞 → (z ·Q y) <Q (z ·Q 𝑞)))
1613, 15syl 14 . . . . . . . . . . . . . . . 16 ((A P z (2ndA)) → (y <Q 𝑞 → (z ·Q y) <Q (z ·Q 𝑞)))
1716adantr 261 . . . . . . . . . . . . . . 15 (((A P z (2ndA)) y Q) → (y <Q 𝑞 → (z ·Q y) <Q (z ·Q 𝑞)))
18 prltlu 6470 . . . . . . . . . . . . . . . . . . . 20 ((⟨(1stA), (2ndA)⟩ P (*Qy) (1stA) z (2ndA)) → (*Qy) <Q z)
1911, 18syl3an1 1167 . . . . . . . . . . . . . . . . . . 19 ((A P (*Qy) (1stA) z (2ndA)) → (*Qy) <Q z)
20193com23 1109 . . . . . . . . . . . . . . . . . 18 ((A P z (2ndA) (*Qy) (1stA)) → (*Qy) <Q z)
21203expia 1105 . . . . . . . . . . . . . . . . 17 ((A P z (2ndA)) → ((*Qy) (1stA) → (*Qy) <Q z))
2221adantr 261 . . . . . . . . . . . . . . . 16 (((A P z (2ndA)) y Q) → ((*Qy) (1stA) → (*Qy) <Q z))
23 ltmnqi 6387 . . . . . . . . . . . . . . . . . . . . 21 (((*Qy) <Q z y Q) → (y ·Q (*Qy)) <Q (y ·Q z))
2423expcom 109 . . . . . . . . . . . . . . . . . . . 20 (y Q → ((*Qy) <Q z → (y ·Q (*Qy)) <Q (y ·Q z)))
2524adantr 261 . . . . . . . . . . . . . . . . . . 19 ((y Q z Q) → ((*Qy) <Q z → (y ·Q (*Qy)) <Q (y ·Q z)))
26 recidnq 6377 . . . . . . . . . . . . . . . . . . . . 21 (y Q → (y ·Q (*Qy)) = 1Q)
2726adantr 261 . . . . . . . . . . . . . . . . . . . 20 ((y Q z Q) → (y ·Q (*Qy)) = 1Q)
28 mulcomnqg 6367 . . . . . . . . . . . . . . . . . . . 20 ((y Q z Q) → (y ·Q z) = (z ·Q y))
2927, 28breq12d 3768 . . . . . . . . . . . . . . . . . . 19 ((y Q z Q) → ((y ·Q (*Qy)) <Q (y ·Q z) ↔ 1Q <Q (z ·Q y)))
3025, 29sylibd 138 . . . . . . . . . . . . . . . . . 18 ((y Q z Q) → ((*Qy) <Q z → 1Q <Q (z ·Q y)))
3130ancoms 255 . . . . . . . . . . . . . . . . 17 ((z Q y Q) → ((*Qy) <Q z → 1Q <Q (z ·Q y)))
3213, 31sylan 267 . . . . . . . . . . . . . . . 16 (((A P z (2ndA)) y Q) → ((*Qy) <Q z → 1Q <Q (z ·Q y)))
3322, 32syld 40 . . . . . . . . . . . . . . 15 (((A P z (2ndA)) y Q) → ((*Qy) (1stA) → 1Q <Q (z ·Q y)))
3417, 33anim12d 318 . . . . . . . . . . . . . 14 (((A P z (2ndA)) y Q) → ((y <Q 𝑞 (*Qy) (1stA)) → ((z ·Q y) <Q (z ·Q 𝑞) 1Q <Q (z ·Q y))))
35 ltsonq 6382 . . . . . . . . . . . . . . . 16 <Q Or Q
3635, 8sotri 4663 . . . . . . . . . . . . . . 15 ((1Q <Q (z ·Q y) (z ·Q y) <Q (z ·Q 𝑞)) → 1Q <Q (z ·Q 𝑞))
3736ancoms 255 . . . . . . . . . . . . . 14 (((z ·Q y) <Q (z ·Q 𝑞) 1Q <Q (z ·Q y)) → 1Q <Q (z ·Q 𝑞))
3834, 37syl6 29 . . . . . . . . . . . . 13 (((A P z (2ndA)) y Q) → ((y <Q 𝑞 (*Qy) (1stA)) → 1Q <Q (z ·Q 𝑞)))
3938exp4b 349 . . . . . . . . . . . 12 ((A P z (2ndA)) → (y Q → (y <Q 𝑞 → ((*Qy) (1stA) → 1Q <Q (z ·Q 𝑞)))))
4010, 39syl5 28 . . . . . . . . . . 11 ((A P z (2ndA)) → (y <Q 𝑞 → (y <Q 𝑞 → ((*Qy) (1stA) → 1Q <Q (z ·Q 𝑞)))))
4140pm2.43d 44 . . . . . . . . . 10 ((A P z (2ndA)) → (y <Q 𝑞 → ((*Qy) (1stA) → 1Q <Q (z ·Q 𝑞))))
4241impd 242 . . . . . . . . 9 ((A P z (2ndA)) → ((y <Q 𝑞 (*Qy) (1stA)) → 1Q <Q (z ·Q 𝑞)))
4342exlimdv 1697 . . . . . . . 8 ((A P z (2ndA)) → (y(y <Q 𝑞 (*Qy) (1stA)) → 1Q <Q (z ·Q 𝑞)))
447, 43syl5bi 141 . . . . . . 7 ((A P z (2ndA)) → (𝑞 (2ndB) → 1Q <Q (z ·Q 𝑞)))
45 breq2 3759 . . . . . . . 8 (w = (z ·Q 𝑞) → (1Q <Q w ↔ 1Q <Q (z ·Q 𝑞)))
4645biimprcd 149 . . . . . . 7 (1Q <Q (z ·Q 𝑞) → (w = (z ·Q 𝑞) → 1Q <Q w))
4744, 46syl6 29 . . . . . 6 ((A P z (2ndA)) → (𝑞 (2ndB) → (w = (z ·Q 𝑞) → 1Q <Q w)))
4847expimpd 345 . . . . 5 (A P → ((z (2ndA) 𝑞 (2ndB)) → (w = (z ·Q 𝑞) → 1Q <Q w)))
4948rexlimdvv 2433 . . . 4 (A P → (z (2ndA)𝑞 (2ndB)w = (z ·Q 𝑞) → 1Q <Q w))
506, 49sylbid 139 . . 3 (A P → (w (2nd ‘(A ·P B)) → 1Q <Q w))
51 1pru 6537 . . . 4 (2nd ‘1P) = {w ∣ 1Q <Q w}
5251abeq2i 2145 . . 3 (w (2nd ‘1P) ↔ 1Q <Q w)
5350, 52syl6ibr 151 . 2 (A P → (w (2nd ‘(A ·P B)) → w (2nd ‘1P)))
5453ssrdv 2945 1 (A P → (2nd ‘(A ·P B)) ⊆ (2nd ‘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