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

Theorem recexprlemlol 6724
 Description: The lower cut of 𝐵 is lower. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 28-Dec-2019.)
Hypothesis
Ref Expression
recexpr.1 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
Assertion
Ref Expression
recexprlemlol ((𝐴P𝑞Q) → (∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵)) → 𝑞 ∈ (1st𝐵)))
Distinct variable groups:   𝑟,𝑞,𝑥,𝑦,𝐴   𝐵,𝑞,𝑟,𝑥,𝑦

Proof of Theorem recexprlemlol
StepHypRef Expression
1 ltsonq 6496 . . . . . . . . 9 <Q Or Q
2 ltrelnq 6463 . . . . . . . . 9 <Q ⊆ (Q × Q)
31, 2sotri 4720 . . . . . . . 8 ((𝑞 <Q 𝑟𝑟 <Q 𝑦) → 𝑞 <Q 𝑦)
43ex 108 . . . . . . 7 (𝑞 <Q 𝑟 → (𝑟 <Q 𝑦𝑞 <Q 𝑦))
54anim1d 319 . . . . . 6 (𝑞 <Q 𝑟 → ((𝑟 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → (𝑞 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))))
65eximdv 1760 . . . . 5 (𝑞 <Q 𝑟 → (∃𝑦(𝑟 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → ∃𝑦(𝑞 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))))
7 recexpr.1 . . . . . 6 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
87recexprlemell 6720 . . . . 5 (𝑟 ∈ (1st𝐵) ↔ ∃𝑦(𝑟 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)))
97recexprlemell 6720 . . . . 5 (𝑞 ∈ (1st𝐵) ↔ ∃𝑦(𝑞 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)))
106, 8, 93imtr4g 194 . . . 4 (𝑞 <Q 𝑟 → (𝑟 ∈ (1st𝐵) → 𝑞 ∈ (1st𝐵)))
1110imp 115 . . 3 ((𝑞 <Q 𝑟𝑟 ∈ (1st𝐵)) → 𝑞 ∈ (1st𝐵))
1211rexlimivw 2429 . 2 (∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵)) → 𝑞 ∈ (1st𝐵))
1312a1i 9 1 ((𝐴P𝑞Q) → (∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵)) → 𝑞 ∈ (1st𝐵)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   = wceq 1243  ∃wex 1381   ∈ wcel 1393  {cab 2026  ∃wrex 2307  ⟨cop 3378   class class class wbr 3764  ‘cfv 4902  1st c1st 5765  2nd c2nd 5766  Qcnq 6378  *Qcrq 6382
 Copyright terms: Public domain W3C validator