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

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

Proof of Theorem recexprlemopu
StepHypRef Expression
1 recexpr.1 . . . 4 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
21recexprlemelu 6778 . . 3 (𝑟 ∈ (2nd𝐵) ↔ ∃𝑦(𝑦 <Q 𝑟 ∧ (*Q𝑦) ∈ (1st𝐴)))
3 ltbtwnnqq 6570 . . . . . 6 (𝑦 <Q 𝑟 ↔ ∃𝑞Q (𝑦 <Q 𝑞𝑞 <Q 𝑟))
43biimpi 117 . . . . 5 (𝑦 <Q 𝑟 → ∃𝑞Q (𝑦 <Q 𝑞𝑞 <Q 𝑟))
5 simplr 490 . . . . . . . 8 (((𝑦 <Q 𝑞𝑞 <Q 𝑟) ∧ (*Q𝑦) ∈ (1st𝐴)) → 𝑞 <Q 𝑟)
6 19.8a 1498 . . . . . . . . . 10 ((𝑦 <Q 𝑞 ∧ (*Q𝑦) ∈ (1st𝐴)) → ∃𝑦(𝑦 <Q 𝑞 ∧ (*Q𝑦) ∈ (1st𝐴)))
71recexprlemelu 6778 . . . . . . . . . 10 (𝑞 ∈ (2nd𝐵) ↔ ∃𝑦(𝑦 <Q 𝑞 ∧ (*Q𝑦) ∈ (1st𝐴)))
86, 7sylibr 141 . . . . . . . . 9 ((𝑦 <Q 𝑞 ∧ (*Q𝑦) ∈ (1st𝐴)) → 𝑞 ∈ (2nd𝐵))
98adantlr 454 . . . . . . . 8 (((𝑦 <Q 𝑞𝑞 <Q 𝑟) ∧ (*Q𝑦) ∈ (1st𝐴)) → 𝑞 ∈ (2nd𝐵))
105, 9jca 294 . . . . . . 7 (((𝑦 <Q 𝑞𝑞 <Q 𝑟) ∧ (*Q𝑦) ∈ (1st𝐴)) → (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)))
1110expcom 113 . . . . . 6 ((*Q𝑦) ∈ (1st𝐴) → ((𝑦 <Q 𝑞𝑞 <Q 𝑟) → (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))))
1211reximdv 2437 . . . . 5 ((*Q𝑦) ∈ (1st𝐴) → (∃𝑞Q (𝑦 <Q 𝑞𝑞 <Q 𝑟) → ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))))
134, 12mpan9 269 . . . 4 ((𝑦 <Q 𝑟 ∧ (*Q𝑦) ∈ (1st𝐴)) → ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)))
1413exlimiv 1505 . . 3 (∃𝑦(𝑦 <Q 𝑟 ∧ (*Q𝑦) ∈ (1st𝐴)) → ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)))
152, 14sylbi 118 . 2 (𝑟 ∈ (2nd𝐵) → ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)))
16153ad2ant3 938 1 ((𝐴P𝑟Q𝑟 ∈ (2nd𝐵)) → ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ∧ w3a 896   = wceq 1259  ∃wex 1397   ∈ wcel 1409  {cab 2042  ∃wrex 2324  ⟨cop 3405   class class class wbr 3791  ‘cfv 4929  1st c1st 5792  2nd c2nd 5793  Qcnq 6435  *Qcrq 6439
 Copyright terms: Public domain W3C validator