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

Theorem recexprlemss1l 7450
 Description: The lower cut of 𝐴 ·P 𝐵 is a subset of the lower 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
recexprlemss1l (𝐴P → (1st ‘(𝐴 ·P 𝐵)) ⊆ (1st ‘1P))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Proof of Theorem recexprlemss1l
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, 4genpelvl 7327 . . . . 5 ((𝐴P𝐵P) → (𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (1st𝐴)∃𝑞 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑞)))
62, 5mpdan 417 . . . 4 (𝐴P → (𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (1st𝐴)∃𝑞 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑞)))
71recexprlemell 7437 . . . . . . . 8 (𝑞 ∈ (1st𝐵) ↔ ∃𝑦(𝑞 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)))
8 ltrelnq 7180 . . . . . . . . . . . . . 14 <Q ⊆ (Q × Q)
98brel 4591 . . . . . . . . . . . . 13 (𝑞 <Q 𝑦 → (𝑞Q𝑦Q))
109simprd 113 . . . . . . . . . . . 12 (𝑞 <Q 𝑦𝑦Q)
11 prop 7290 . . . . . . . . . . . . . . . . . 18 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
12 elprnql 7296 . . . . . . . . . . . . . . . . . 18 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑧 ∈ (1st𝐴)) → 𝑧Q)
1311, 12sylan 281 . . . . . . . . . . . . . . . . 17 ((𝐴P𝑧 ∈ (1st𝐴)) → 𝑧Q)
14 ltmnqi 7218 . . . . . . . . . . . . . . . . . 18 ((𝑞 <Q 𝑦𝑧Q) → (𝑧 ·Q 𝑞) <Q (𝑧 ·Q 𝑦))
1514expcom 115 . . . . . . . . . . . . . . . . 17 (𝑧Q → (𝑞 <Q 𝑦 → (𝑧 ·Q 𝑞) <Q (𝑧 ·Q 𝑦)))
1613, 15syl 14 . . . . . . . . . . . . . . . 16 ((𝐴P𝑧 ∈ (1st𝐴)) → (𝑞 <Q 𝑦 → (𝑧 ·Q 𝑞) <Q (𝑧 ·Q 𝑦)))
1716adantr 274 . . . . . . . . . . . . . . 15 (((𝐴P𝑧 ∈ (1st𝐴)) ∧ 𝑦Q) → (𝑞 <Q 𝑦 → (𝑧 ·Q 𝑞) <Q (𝑧 ·Q 𝑦)))
18 prltlu 7302 . . . . . . . . . . . . . . . . . . 19 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑧 ∈ (1st𝐴) ∧ (*Q𝑦) ∈ (2nd𝐴)) → 𝑧 <Q (*Q𝑦))
1911, 18syl3an1 1249 . . . . . . . . . . . . . . . . . 18 ((𝐴P𝑧 ∈ (1st𝐴) ∧ (*Q𝑦) ∈ (2nd𝐴)) → 𝑧 <Q (*Q𝑦))
20193expia 1183 . . . . . . . . . . . . . . . . 17 ((𝐴P𝑧 ∈ (1st𝐴)) → ((*Q𝑦) ∈ (2nd𝐴) → 𝑧 <Q (*Q𝑦)))
2120adantr 274 . . . . . . . . . . . . . . . 16 (((𝐴P𝑧 ∈ (1st𝐴)) ∧ 𝑦Q) → ((*Q𝑦) ∈ (2nd𝐴) → 𝑧 <Q (*Q𝑦)))
22 ltmnqi 7218 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 <Q (*Q𝑦) ∧ 𝑦Q) → (𝑦 ·Q 𝑧) <Q (𝑦 ·Q (*Q𝑦)))
2322expcom 115 . . . . . . . . . . . . . . . . . . . 20 (𝑦Q → (𝑧 <Q (*Q𝑦) → (𝑦 ·Q 𝑧) <Q (𝑦 ·Q (*Q𝑦))))
2423adantr 274 . . . . . . . . . . . . . . . . . . 19 ((𝑦Q𝑧Q) → (𝑧 <Q (*Q𝑦) → (𝑦 ·Q 𝑧) <Q (𝑦 ·Q (*Q𝑦))))
25 mulcomnqg 7198 . . . . . . . . . . . . . . . . . . . 20 ((𝑦Q𝑧Q) → (𝑦 ·Q 𝑧) = (𝑧 ·Q 𝑦))
26 recidnq 7208 . . . . . . . . . . . . . . . . . . . . 21 (𝑦Q → (𝑦 ·Q (*Q𝑦)) = 1Q)
2726adantr 274 . . . . . . . . . . . . . . . . . . . 20 ((𝑦Q𝑧Q) → (𝑦 ·Q (*Q𝑦)) = 1Q)
2825, 27breq12d 3942 . . . . . . . . . . . . . . . . . . 19 ((𝑦Q𝑧Q) → ((𝑦 ·Q 𝑧) <Q (𝑦 ·Q (*Q𝑦)) ↔ (𝑧 ·Q 𝑦) <Q 1Q))
2924, 28sylibd 148 . . . . . . . . . . . . . . . . . 18 ((𝑦Q𝑧Q) → (𝑧 <Q (*Q𝑦) → (𝑧 ·Q 𝑦) <Q 1Q))
3029ancoms 266 . . . . . . . . . . . . . . . . 17 ((𝑧Q𝑦Q) → (𝑧 <Q (*Q𝑦) → (𝑧 ·Q 𝑦) <Q 1Q))
3113, 30sylan 281 . . . . . . . . . . . . . . . 16 (((𝐴P𝑧 ∈ (1st𝐴)) ∧ 𝑦Q) → (𝑧 <Q (*Q𝑦) → (𝑧 ·Q 𝑦) <Q 1Q))
3221, 31syld 45 . . . . . . . . . . . . . . 15 (((𝐴P𝑧 ∈ (1st𝐴)) ∧ 𝑦Q) → ((*Q𝑦) ∈ (2nd𝐴) → (𝑧 ·Q 𝑦) <Q 1Q))
3317, 32anim12d 333 . . . . . . . . . . . . . 14 (((𝐴P𝑧 ∈ (1st𝐴)) ∧ 𝑦Q) → ((𝑞 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → ((𝑧 ·Q 𝑞) <Q (𝑧 ·Q 𝑦) ∧ (𝑧 ·Q 𝑦) <Q 1Q)))
34 ltsonq 7213 . . . . . . . . . . . . . . 15 <Q Or Q
3534, 8sotri 4934 . . . . . . . . . . . . . 14 (((𝑧 ·Q 𝑞) <Q (𝑧 ·Q 𝑦) ∧ (𝑧 ·Q 𝑦) <Q 1Q) → (𝑧 ·Q 𝑞) <Q 1Q)
3633, 35syl6 33 . . . . . . . . . . . . 13 (((𝐴P𝑧 ∈ (1st𝐴)) ∧ 𝑦Q) → ((𝑞 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → (𝑧 ·Q 𝑞) <Q 1Q))
3736exp4b 364 . . . . . . . . . . . 12 ((𝐴P𝑧 ∈ (1st𝐴)) → (𝑦Q → (𝑞 <Q 𝑦 → ((*Q𝑦) ∈ (2nd𝐴) → (𝑧 ·Q 𝑞) <Q 1Q))))
3810, 37syl5 32 . . . . . . . . . . 11 ((𝐴P𝑧 ∈ (1st𝐴)) → (𝑞 <Q 𝑦 → (𝑞 <Q 𝑦 → ((*Q𝑦) ∈ (2nd𝐴) → (𝑧 ·Q 𝑞) <Q 1Q))))
3938pm2.43d 50 . . . . . . . . . 10 ((𝐴P𝑧 ∈ (1st𝐴)) → (𝑞 <Q 𝑦 → ((*Q𝑦) ∈ (2nd𝐴) → (𝑧 ·Q 𝑞) <Q 1Q)))
4039impd 252 . . . . . . . . 9 ((𝐴P𝑧 ∈ (1st𝐴)) → ((𝑞 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → (𝑧 ·Q 𝑞) <Q 1Q))
4140exlimdv 1791 . . . . . . . 8 ((𝐴P𝑧 ∈ (1st𝐴)) → (∃𝑦(𝑞 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → (𝑧 ·Q 𝑞) <Q 1Q))
427, 41syl5bi 151 . . . . . . 7 ((𝐴P𝑧 ∈ (1st𝐴)) → (𝑞 ∈ (1st𝐵) → (𝑧 ·Q 𝑞) <Q 1Q))
43 breq1 3932 . . . . . . . 8 (𝑤 = (𝑧 ·Q 𝑞) → (𝑤 <Q 1Q ↔ (𝑧 ·Q 𝑞) <Q 1Q))
4443biimprcd 159 . . . . . . 7 ((𝑧 ·Q 𝑞) <Q 1Q → (𝑤 = (𝑧 ·Q 𝑞) → 𝑤 <Q 1Q))
4542, 44syl6 33 . . . . . 6 ((𝐴P𝑧 ∈ (1st𝐴)) → (𝑞 ∈ (1st𝐵) → (𝑤 = (𝑧 ·Q 𝑞) → 𝑤 <Q 1Q)))
4645expimpd 360 . . . . 5 (𝐴P → ((𝑧 ∈ (1st𝐴) ∧ 𝑞 ∈ (1st𝐵)) → (𝑤 = (𝑧 ·Q 𝑞) → 𝑤 <Q 1Q)))
4746rexlimdvv 2556 . . . 4 (𝐴P → (∃𝑧 ∈ (1st𝐴)∃𝑞 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑞) → 𝑤 <Q 1Q))
486, 47sylbid 149 . . 3 (𝐴P → (𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)) → 𝑤 <Q 1Q))
49 1prl 7370 . . . 4 (1st ‘1P) = {𝑤𝑤 <Q 1Q}
5049abeq2i 2250 . . 3 (𝑤 ∈ (1st ‘1P) ↔ 𝑤 <Q 1Q)
5148, 50syl6ibr 161 . 2 (𝐴P → (𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)) → 𝑤 ∈ (1st ‘1P)))
5251ssrdv 3103 1 (𝐴P → (1st ‘(𝐴 ·P 𝐵)) ⊆ (1st ‘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