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

Theorem recexprlemss1u 7451
 Description: The upper cut of 𝐴 ·P 𝐵 is a subset of the upper cut of one. Lemma for recexpr 7453. (Contributed by Jim Kingdon, 27-Dec-2019.)
Hypothesis
Ref Expression
recexpr.1 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
Assertion
Ref Expression
recexprlemss1u (𝐴P → (2nd ‘(𝐴 ·P 𝐵)) ⊆ (2nd ‘1P))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Proof of Theorem recexprlemss1u
Dummy variables 𝑞 𝑧 𝑤 𝑢 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 recexpr.1 . . . . . 6 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
21recexprlempr 7447 . . . . 5 (𝐴P𝐵P)
3 df-imp 7284 . . . . . 6 ·P = (𝑦P, 𝑤P ↦ ⟨{𝑢Q ∣ ∃𝑓Q𝑔Q (𝑓 ∈ (1st𝑦) ∧ 𝑔 ∈ (1st𝑤) ∧ 𝑢 = (𝑓 ·Q 𝑔))}, {𝑢Q ∣ ∃𝑓Q𝑔Q (𝑓 ∈ (2nd𝑦) ∧ 𝑔 ∈ (2nd𝑤) ∧ 𝑢 = (𝑓 ·Q 𝑔))}⟩)
4 mulclnq 7191 . . . . . 6 ((𝑓Q𝑔Q) → (𝑓 ·Q 𝑔) ∈ Q)
53, 4genpelvu 7328 . . . . 5 ((𝐴P𝐵P) → (𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (2nd𝐴)∃𝑞 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑞)))
62, 5mpdan 417 . . . 4 (𝐴P → (𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (2nd𝐴)∃𝑞 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑞)))
71recexprlemelu 7438 . . . . . . . 8 (𝑞 ∈ (2nd𝐵) ↔ ∃𝑦(𝑦 <Q 𝑞 ∧ (*Q𝑦) ∈ (1st𝐴)))
8 ltrelnq 7180 . . . . . . . . . . . . . 14 <Q ⊆ (Q × Q)
98brel 4591 . . . . . . . . . . . . 13 (𝑦 <Q 𝑞 → (𝑦Q𝑞Q))
109simpld 111 . . . . . . . . . . . 12 (𝑦 <Q 𝑞𝑦Q)
11 prop 7290 . . . . . . . . . . . . . . . . . 18 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
12 elprnqu 7297 . . . . . . . . . . . . . . . . . 18 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑧 ∈ (2nd𝐴)) → 𝑧Q)
1311, 12sylan 281 . . . . . . . . . . . . . . . . 17 ((𝐴P𝑧 ∈ (2nd𝐴)) → 𝑧Q)
14 ltmnqi 7218 . . . . . . . . . . . . . . . . . 18 ((𝑦 <Q 𝑞𝑧Q) → (𝑧 ·Q 𝑦) <Q (𝑧 ·Q 𝑞))
1514expcom 115 . . . . . . . . . . . . . . . . 17 (𝑧Q → (𝑦 <Q 𝑞 → (𝑧 ·Q 𝑦) <Q (𝑧 ·Q 𝑞)))
1613, 15syl 14 . . . . . . . . . . . . . . . 16 ((𝐴P𝑧 ∈ (2nd𝐴)) → (𝑦 <Q 𝑞 → (𝑧 ·Q 𝑦) <Q (𝑧 ·Q 𝑞)))
1716adantr 274 . . . . . . . . . . . . . . 15 (((𝐴P𝑧 ∈ (2nd𝐴)) ∧ 𝑦Q) → (𝑦 <Q 𝑞 → (𝑧 ·Q 𝑦) <Q (𝑧 ·Q 𝑞)))
18 prltlu 7302 . . . . . . . . . . . . . . . . . . . 20 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P ∧ (*Q𝑦) ∈ (1st𝐴) ∧ 𝑧 ∈ (2nd𝐴)) → (*Q𝑦) <Q 𝑧)
1911, 18syl3an1 1249 . . . . . . . . . . . . . . . . . . 19 ((𝐴P ∧ (*Q𝑦) ∈ (1st𝐴) ∧ 𝑧 ∈ (2nd𝐴)) → (*Q𝑦) <Q 𝑧)
20193com23 1187 . . . . . . . . . . . . . . . . . 18 ((𝐴P𝑧 ∈ (2nd𝐴) ∧ (*Q𝑦) ∈ (1st𝐴)) → (*Q𝑦) <Q 𝑧)
21203expia 1183 . . . . . . . . . . . . . . . . 17 ((𝐴P𝑧 ∈ (2nd𝐴)) → ((*Q𝑦) ∈ (1st𝐴) → (*Q𝑦) <Q 𝑧))
2221adantr 274 . . . . . . . . . . . . . . . 16 (((𝐴P𝑧 ∈ (2nd𝐴)) ∧ 𝑦Q) → ((*Q𝑦) ∈ (1st𝐴) → (*Q𝑦) <Q 𝑧))
23 ltmnqi 7218 . . . . . . . . . . . . . . . . . . . . 21 (((*Q𝑦) <Q 𝑧𝑦Q) → (𝑦 ·Q (*Q𝑦)) <Q (𝑦 ·Q 𝑧))
2423expcom 115 . . . . . . . . . . . . . . . . . . . 20 (𝑦Q → ((*Q𝑦) <Q 𝑧 → (𝑦 ·Q (*Q𝑦)) <Q (𝑦 ·Q 𝑧)))
2524adantr 274 . . . . . . . . . . . . . . . . . . 19 ((𝑦Q𝑧Q) → ((*Q𝑦) <Q 𝑧 → (𝑦 ·Q (*Q𝑦)) <Q (𝑦 ·Q 𝑧)))
26 recidnq 7208 . . . . . . . . . . . . . . . . . . . . 21 (𝑦Q → (𝑦 ·Q (*Q𝑦)) = 1Q)
2726adantr 274 . . . . . . . . . . . . . . . . . . . 20 ((𝑦Q𝑧Q) → (𝑦 ·Q (*Q𝑦)) = 1Q)
28 mulcomnqg 7198 . . . . . . . . . . . . . . . . . . . 20 ((𝑦Q𝑧Q) → (𝑦 ·Q 𝑧) = (𝑧 ·Q 𝑦))
2927, 28breq12d 3942 . . . . . . . . . . . . . . . . . . 19 ((𝑦Q𝑧Q) → ((𝑦 ·Q (*Q𝑦)) <Q (𝑦 ·Q 𝑧) ↔ 1Q <Q (𝑧 ·Q 𝑦)))
3025, 29sylibd 148 . . . . . . . . . . . . . . . . . 18 ((𝑦Q𝑧Q) → ((*Q𝑦) <Q 𝑧 → 1Q <Q (𝑧 ·Q 𝑦)))
3130ancoms 266 . . . . . . . . . . . . . . . . 17 ((𝑧Q𝑦Q) → ((*Q𝑦) <Q 𝑧 → 1Q <Q (𝑧 ·Q 𝑦)))
3213, 31sylan 281 . . . . . . . . . . . . . . . 16 (((𝐴P𝑧 ∈ (2nd𝐴)) ∧ 𝑦Q) → ((*Q𝑦) <Q 𝑧 → 1Q <Q (𝑧 ·Q 𝑦)))
3322, 32syld 45 . . . . . . . . . . . . . . 15 (((𝐴P𝑧 ∈ (2nd𝐴)) ∧ 𝑦Q) → ((*Q𝑦) ∈ (1st𝐴) → 1Q <Q (𝑧 ·Q 𝑦)))
3417, 33anim12d 333 . . . . . . . . . . . . . 14 (((𝐴P𝑧 ∈ (2nd𝐴)) ∧ 𝑦Q) → ((𝑦 <Q 𝑞 ∧ (*Q𝑦) ∈ (1st𝐴)) → ((𝑧 ·Q 𝑦) <Q (𝑧 ·Q 𝑞) ∧ 1Q <Q (𝑧 ·Q 𝑦))))
35 ltsonq 7213 . . . . . . . . . . . . . . . 16 <Q Or Q
3635, 8sotri 4934 . . . . . . . . . . . . . . 15 ((1Q <Q (𝑧 ·Q 𝑦) ∧ (𝑧 ·Q 𝑦) <Q (𝑧 ·Q 𝑞)) → 1Q <Q (𝑧 ·Q 𝑞))
3736ancoms 266 . . . . . . . . . . . . . 14 (((𝑧 ·Q 𝑦) <Q (𝑧 ·Q 𝑞) ∧ 1Q <Q (𝑧 ·Q 𝑦)) → 1Q <Q (𝑧 ·Q 𝑞))
3834, 37syl6 33 . . . . . . . . . . . . 13 (((𝐴P𝑧 ∈ (2nd𝐴)) ∧ 𝑦Q) → ((𝑦 <Q 𝑞 ∧ (*Q𝑦) ∈ (1st𝐴)) → 1Q <Q (𝑧 ·Q 𝑞)))
3938exp4b 364 . . . . . . . . . . . 12 ((𝐴P𝑧 ∈ (2nd𝐴)) → (𝑦Q → (𝑦 <Q 𝑞 → ((*Q𝑦) ∈ (1st𝐴) → 1Q <Q (𝑧 ·Q 𝑞)))))
4010, 39syl5 32 . . . . . . . . . . 11 ((𝐴P𝑧 ∈ (2nd𝐴)) → (𝑦 <Q 𝑞 → (𝑦 <Q 𝑞 → ((*Q𝑦) ∈ (1st𝐴) → 1Q <Q (𝑧 ·Q 𝑞)))))
4140pm2.43d 50 . . . . . . . . . 10 ((𝐴P𝑧 ∈ (2nd𝐴)) → (𝑦 <Q 𝑞 → ((*Q𝑦) ∈ (1st𝐴) → 1Q <Q (𝑧 ·Q 𝑞))))
4241impd 252 . . . . . . . . 9 ((𝐴P𝑧 ∈ (2nd𝐴)) → ((𝑦 <Q 𝑞 ∧ (*Q𝑦) ∈ (1st𝐴)) → 1Q <Q (𝑧 ·Q 𝑞)))
4342exlimdv 1791 . . . . . . . 8 ((𝐴P𝑧 ∈ (2nd𝐴)) → (∃𝑦(𝑦 <Q 𝑞 ∧ (*Q𝑦) ∈ (1st𝐴)) → 1Q <Q (𝑧 ·Q 𝑞)))
447, 43syl5bi 151 . . . . . . 7 ((𝐴P𝑧 ∈ (2nd𝐴)) → (𝑞 ∈ (2nd𝐵) → 1Q <Q (𝑧 ·Q 𝑞)))
45 breq2 3933 . . . . . . . 8 (𝑤 = (𝑧 ·Q 𝑞) → (1Q <Q 𝑤 ↔ 1Q <Q (𝑧 ·Q 𝑞)))
4645biimprcd 159 . . . . . . 7 (1Q <Q (𝑧 ·Q 𝑞) → (𝑤 = (𝑧 ·Q 𝑞) → 1Q <Q 𝑤))
4744, 46syl6 33 . . . . . 6 ((𝐴P𝑧 ∈ (2nd𝐴)) → (𝑞 ∈ (2nd𝐵) → (𝑤 = (𝑧 ·Q 𝑞) → 1Q <Q 𝑤)))
4847expimpd 360 . . . . 5 (𝐴P → ((𝑧 ∈ (2nd𝐴) ∧ 𝑞 ∈ (2nd𝐵)) → (𝑤 = (𝑧 ·Q 𝑞) → 1Q <Q 𝑤)))
4948rexlimdvv 2556 . . . 4 (𝐴P → (∃𝑧 ∈ (2nd𝐴)∃𝑞 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑞) → 1Q <Q 𝑤))
506, 49sylbid 149 . . 3 (𝐴P → (𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵)) → 1Q <Q 𝑤))
51 1pru 7371 . . . 4 (2nd ‘1P) = {𝑤 ∣ 1Q <Q 𝑤}
5251abeq2i 2250 . . 3 (𝑤 ∈ (2nd ‘1P) ↔ 1Q <Q 𝑤)
5350, 52syl6ibr 161 . 2 (𝐴P → (𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵)) → 𝑤 ∈ (2nd ‘1P)))
5453ssrdv 3103 1 (𝐴P → (2nd ‘(𝐴 ·P 𝐵)) ⊆ (2nd ‘1P))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1331  ∃wex 1468   ∈ wcel 1480  {cab 2125  ∃wrex 2417   ⊆ wss 3071  ⟨cop 3530   class class class wbr 3929  ‘cfv 5123  (class class class)co 5774  1st c1st 6036  2nd c2nd 6037  Qcnq 7095  1Qc1q 7096   ·Q cmq 7098  *Qcrq 7099
 Copyright terms: Public domain W3C validator