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

Theorem recexprlemopl 6723
 Description: The lower cut of 𝐵 is open. 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
recexprlemopl ((𝐴P𝑞Q𝑞 ∈ (1st𝐵)) → ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵)))
Distinct variable groups:   𝑟,𝑞,𝑥,𝑦,𝐴   𝐵,𝑞,𝑟,𝑥,𝑦

Proof of Theorem recexprlemopl
StepHypRef Expression
1 recexpr.1 . . . 4 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
21recexprlemell 6720 . . 3 (𝑞 ∈ (1st𝐵) ↔ ∃𝑦(𝑞 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)))
3 ltbtwnnqq 6513 . . . . . 6 (𝑞 <Q 𝑦 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 <Q 𝑦))
43biimpi 113 . . . . 5 (𝑞 <Q 𝑦 → ∃𝑟Q (𝑞 <Q 𝑟𝑟 <Q 𝑦))
5 simpll 481 . . . . . . . 8 (((𝑞 <Q 𝑟𝑟 <Q 𝑦) ∧ (*Q𝑦) ∈ (2nd𝐴)) → 𝑞 <Q 𝑟)
6 19.8a 1482 . . . . . . . . . 10 ((𝑟 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → ∃𝑦(𝑟 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)))
71recexprlemell 6720 . . . . . . . . . 10 (𝑟 ∈ (1st𝐵) ↔ ∃𝑦(𝑟 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)))
86, 7sylibr 137 . . . . . . . . 9 ((𝑟 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → 𝑟 ∈ (1st𝐵))
98adantll 445 . . . . . . . 8 (((𝑞 <Q 𝑟𝑟 <Q 𝑦) ∧ (*Q𝑦) ∈ (2nd𝐴)) → 𝑟 ∈ (1st𝐵))
105, 9jca 290 . . . . . . 7 (((𝑞 <Q 𝑟𝑟 <Q 𝑦) ∧ (*Q𝑦) ∈ (2nd𝐴)) → (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵)))
1110expcom 109 . . . . . 6 ((*Q𝑦) ∈ (2nd𝐴) → ((𝑞 <Q 𝑟𝑟 <Q 𝑦) → (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵))))
1211reximdv 2420 . . . . 5 ((*Q𝑦) ∈ (2nd𝐴) → (∃𝑟Q (𝑞 <Q 𝑟𝑟 <Q 𝑦) → ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵))))
134, 12mpan9 265 . . . 4 ((𝑞 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵)))
1413exlimiv 1489 . . 3 (∃𝑦(𝑞 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵)))
152, 14sylbi 114 . 2 (𝑞 ∈ (1st𝐵) → ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵)))
16153ad2ant3 927 1 ((𝐴P𝑞Q𝑞 ∈ (1st𝐵)) → ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885   = 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