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

Theorem ltexprlemfu 7072
Description: Lemma for ltexpri 7074. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
Hypothesis
Ref Expression
ltexprlem.1 𝐶 = ⟨{𝑥Q ∣ ∃𝑦(𝑦 ∈ (2nd𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st𝐵))}, {𝑥Q ∣ ∃𝑦(𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd𝐵))}⟩
Assertion
Ref Expression
ltexprlemfu (𝐴<P 𝐵 → (2nd ‘(𝐴 +P 𝐶)) ⊆ (2nd𝐵))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦

Proof of Theorem ltexprlemfu
Dummy variables 𝑧 𝑤 𝑢 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelpr 6966 . . . . . 6 <P ⊆ (P × P)
21brel 4447 . . . . 5 (𝐴<P 𝐵 → (𝐴P𝐵P))
32simpld 110 . . . 4 (𝐴<P 𝐵𝐴P)
4 ltexprlem.1 . . . . 5 𝐶 = ⟨{𝑥Q ∣ ∃𝑦(𝑦 ∈ (2nd𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st𝐵))}, {𝑥Q ∣ ∃𝑦(𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd𝐵))}⟩
54ltexprlempr 7069 . . . 4 (𝐴<P 𝐵𝐶P)
6 df-iplp 6929 . . . . 5 +P = (𝑧P, 𝑦P ↦ ⟨{𝑓Q ∣ ∃𝑔QQ (𝑔 ∈ (1st𝑧) ∧ ∈ (1st𝑦) ∧ 𝑓 = (𝑔 +Q ))}, {𝑓Q ∣ ∃𝑔QQ (𝑔 ∈ (2nd𝑧) ∧ ∈ (2nd𝑦) ∧ 𝑓 = (𝑔 +Q ))}⟩)
7 addclnq 6836 . . . . 5 ((𝑔QQ) → (𝑔 +Q ) ∈ Q)
86, 7genpelvu 6974 . . . 4 ((𝐴P𝐶P) → (𝑧 ∈ (2nd ‘(𝐴 +P 𝐶)) ↔ ∃𝑤 ∈ (2nd𝐴)∃𝑢 ∈ (2nd𝐶)𝑧 = (𝑤 +Q 𝑢)))
93, 5, 8syl2anc 403 . . 3 (𝐴<P 𝐵 → (𝑧 ∈ (2nd ‘(𝐴 +P 𝐶)) ↔ ∃𝑤 ∈ (2nd𝐴)∃𝑢 ∈ (2nd𝐶)𝑧 = (𝑤 +Q 𝑢)))
10 simprr 499 . . . . . 6 ((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢))) → 𝑧 = (𝑤 +Q 𝑢))
114ltexprlemelu 7060 . . . . . . . . . . 11 (𝑢 ∈ (2nd𝐶) ↔ (𝑢Q ∧ ∃𝑦(𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))))
1211biimpi 118 . . . . . . . . . 10 (𝑢 ∈ (2nd𝐶) → (𝑢Q ∧ ∃𝑦(𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))))
1312ad2antlr 473 . . . . . . . . 9 (((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) → (𝑢Q ∧ ∃𝑦(𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))))
1413simprd 112 . . . . . . . 8 (((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) → ∃𝑦(𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵)))
1514adantl 271 . . . . . . 7 ((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢))) → ∃𝑦(𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵)))
16 prop 6936 . . . . . . . . . . . . . . 15 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
173, 16syl 14 . . . . . . . . . . . . . 14 (𝐴<P 𝐵 → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
18 prltlu 6948 . . . . . . . . . . . . . 14 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑦 ∈ (1st𝐴) ∧ 𝑤 ∈ (2nd𝐴)) → 𝑦 <Q 𝑤)
1917, 18syl3an1 1203 . . . . . . . . . . . . 13 ((𝐴<P 𝐵𝑦 ∈ (1st𝐴) ∧ 𝑤 ∈ (2nd𝐴)) → 𝑦 <Q 𝑤)
20193com23 1145 . . . . . . . . . . . 12 ((𝐴<P 𝐵𝑤 ∈ (2nd𝐴) ∧ 𝑦 ∈ (1st𝐴)) → 𝑦 <Q 𝑤)
21203adant2r 1165 . . . . . . . . . . 11 ((𝐴<P 𝐵 ∧ (𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑦 ∈ (1st𝐴)) → 𝑦 <Q 𝑤)
22213adant2r 1165 . . . . . . . . . 10 ((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ 𝑦 ∈ (1st𝐴)) → 𝑦 <Q 𝑤)
23223adant3r 1167 . . . . . . . . 9 ((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))) → 𝑦 <Q 𝑤)
24 ltanqg 6861 . . . . . . . . . . . 12 ((𝑓Q𝑔QQ) → (𝑓 <Q 𝑔 ↔ ( +Q 𝑓) <Q ( +Q 𝑔)))
2524adantl 271 . . . . . . . . . . 11 (((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))) ∧ (𝑓Q𝑔QQ)) → (𝑓 <Q 𝑔 ↔ ( +Q 𝑓) <Q ( +Q 𝑔)))
26 elprnql 6942 . . . . . . . . . . . . . 14 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑦 ∈ (1st𝐴)) → 𝑦Q)
2717, 26sylan 277 . . . . . . . . . . . . 13 ((𝐴<P 𝐵𝑦 ∈ (1st𝐴)) → 𝑦Q)
2827adantrr 463 . . . . . . . . . . . 12 ((𝐴<P 𝐵 ∧ (𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))) → 𝑦Q)
29283adant2 958 . . . . . . . . . . 11 ((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))) → 𝑦Q)
30 elprnqu 6943 . . . . . . . . . . . . . . 15 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑤 ∈ (2nd𝐴)) → 𝑤Q)
3117, 30sylan 277 . . . . . . . . . . . . . 14 ((𝐴<P 𝐵𝑤 ∈ (2nd𝐴)) → 𝑤Q)
3231adantrr 463 . . . . . . . . . . . . 13 ((𝐴<P 𝐵 ∧ (𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶))) → 𝑤Q)
3332adantrr 463 . . . . . . . . . . . 12 ((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢))) → 𝑤Q)
34333adant3 959 . . . . . . . . . . 11 ((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))) → 𝑤Q)
35 prop 6936 . . . . . . . . . . . . . . . 16 (𝐶P → ⟨(1st𝐶), (2nd𝐶)⟩ ∈ P)
365, 35syl 14 . . . . . . . . . . . . . . 15 (𝐴<P 𝐵 → ⟨(1st𝐶), (2nd𝐶)⟩ ∈ P)
37 elprnqu 6943 . . . . . . . . . . . . . . 15 ((⟨(1st𝐶), (2nd𝐶)⟩ ∈ P𝑢 ∈ (2nd𝐶)) → 𝑢Q)
3836, 37sylan 277 . . . . . . . . . . . . . 14 ((𝐴<P 𝐵𝑢 ∈ (2nd𝐶)) → 𝑢Q)
3938adantrl 462 . . . . . . . . . . . . 13 ((𝐴<P 𝐵 ∧ (𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶))) → 𝑢Q)
4039adantrr 463 . . . . . . . . . . . 12 ((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢))) → 𝑢Q)
41403adant3 959 . . . . . . . . . . 11 ((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))) → 𝑢Q)
42 addcomnqg 6842 . . . . . . . . . . . 12 ((𝑓Q𝑔Q) → (𝑓 +Q 𝑔) = (𝑔 +Q 𝑓))
4342adantl 271 . . . . . . . . . . 11 (((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))) ∧ (𝑓Q𝑔Q)) → (𝑓 +Q 𝑔) = (𝑔 +Q 𝑓))
4425, 29, 34, 41, 43caovord2d 5748 . . . . . . . . . 10 ((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))) → (𝑦 <Q 𝑤 ↔ (𝑦 +Q 𝑢) <Q (𝑤 +Q 𝑢)))
452simprd 112 . . . . . . . . . . . . . 14 (𝐴<P 𝐵𝐵P)
46 prop 6936 . . . . . . . . . . . . . 14 (𝐵P → ⟨(1st𝐵), (2nd𝐵)⟩ ∈ P)
4745, 46syl 14 . . . . . . . . . . . . 13 (𝐴<P 𝐵 → ⟨(1st𝐵), (2nd𝐵)⟩ ∈ P)
48 prcunqu 6946 . . . . . . . . . . . . 13 ((⟨(1st𝐵), (2nd𝐵)⟩ ∈ P ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵)) → ((𝑦 +Q 𝑢) <Q (𝑤 +Q 𝑢) → (𝑤 +Q 𝑢) ∈ (2nd𝐵)))
4947, 48sylan 277 . . . . . . . . . . . 12 ((𝐴<P 𝐵 ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵)) → ((𝑦 +Q 𝑢) <Q (𝑤 +Q 𝑢) → (𝑤 +Q 𝑢) ∈ (2nd𝐵)))
5049adantrl 462 . . . . . . . . . . 11 ((𝐴<P 𝐵 ∧ (𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))) → ((𝑦 +Q 𝑢) <Q (𝑤 +Q 𝑢) → (𝑤 +Q 𝑢) ∈ (2nd𝐵)))
51503adant2 958 . . . . . . . . . 10 ((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))) → ((𝑦 +Q 𝑢) <Q (𝑤 +Q 𝑢) → (𝑤 +Q 𝑢) ∈ (2nd𝐵)))
5244, 51sylbid 148 . . . . . . . . 9 ((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))) → (𝑦 <Q 𝑤 → (𝑤 +Q 𝑢) ∈ (2nd𝐵)))
5323, 52mpd 13 . . . . . . . 8 ((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢)) ∧ (𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))) → (𝑤 +Q 𝑢) ∈ (2nd𝐵))
54533expa 1139 . . . . . . 7 (((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢))) ∧ (𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑢) ∈ (2nd𝐵))) → (𝑤 +Q 𝑢) ∈ (2nd𝐵))
5515, 54exlimddv 1821 . . . . . 6 ((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢))) → (𝑤 +Q 𝑢) ∈ (2nd𝐵))
5610, 55eqeltrd 2159 . . . . 5 ((𝐴<P 𝐵 ∧ ((𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑢))) → 𝑧 ∈ (2nd𝐵))
5756expr 367 . . . 4 ((𝐴<P 𝐵 ∧ (𝑤 ∈ (2nd𝐴) ∧ 𝑢 ∈ (2nd𝐶))) → (𝑧 = (𝑤 +Q 𝑢) → 𝑧 ∈ (2nd𝐵)))
5857rexlimdvva 2490 . . 3 (𝐴<P 𝐵 → (∃𝑤 ∈ (2nd𝐴)∃𝑢 ∈ (2nd𝐶)𝑧 = (𝑤 +Q 𝑢) → 𝑧 ∈ (2nd𝐵)))
599, 58sylbid 148 . 2 (𝐴<P 𝐵 → (𝑧 ∈ (2nd ‘(𝐴 +P 𝐶)) → 𝑧 ∈ (2nd𝐵)))
6059ssrdv 3016 1 (𝐴<P 𝐵 → (2nd ‘(𝐴 +P 𝐶)) ⊆ (2nd𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  w3a 920   = wceq 1285  wex 1422  wcel 1434  wrex 2354  {crab 2357  wss 2984  cop 3425   class class class wbr 3811  cfv 4968  (class class class)co 5590  1st c1st 5843  2nd c2nd 5844  Qcnq 6741   +Q cplq 6743   <Q cltq 6746  Pcnp 6752   +P cpp 6754  <P cltp 6756
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-coll 3919  ax-sep 3922  ax-nul 3930  ax-pow 3974  ax-pr 3999  ax-un 4223  ax-setind 4315  ax-iinf 4365
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2614  df-sbc 2827  df-csb 2920  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-nul 3270  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-int 3663  df-iun 3706  df-br 3812  df-opab 3866  df-mpt 3867  df-tr 3902  df-eprel 4079  df-id 4083  df-po 4086  df-iso 4087  df-iord 4156  df-on 4158  df-suc 4161  df-iom 4368  df-xp 4406  df-rel 4407  df-cnv 4408  df-co 4409  df-dm 4410  df-rn 4411  df-res 4412  df-ima 4413  df-iota 4933  df-fun 4970  df-fn 4971  df-f 4972  df-f1 4973  df-fo 4974  df-f1o 4975  df-fv 4976  df-ov 5593  df-oprab 5594  df-mpt2 5595  df-1st 5845  df-2nd 5846  df-recs 6001  df-irdg 6066  df-1o 6112  df-2o 6113  df-oadd 6116  df-omul 6117  df-er 6221  df-ec 6223  df-qs 6227  df-ni 6765  df-pli 6766  df-mi 6767  df-lti 6768  df-plpq 6805  df-mpq 6806  df-enq 6808  df-nqqs 6809  df-plqqs 6810  df-mqqs 6811  df-1nqqs 6812  df-rq 6813  df-ltnqqs 6814  df-enq0 6885  df-nq0 6886  df-0nq0 6887  df-plq0 6888  df-mq0 6889  df-inp 6927  df-iplp 6929  df-iltp 6931
This theorem is referenced by:  ltexpri  7074
  Copyright terms: Public domain W3C validator