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

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

Proof of Theorem recexprlemupu
StepHypRef Expression
1 ltsonq 7213 . . . . . . . . 9 <Q Or Q
2 ltrelnq 7180 . . . . . . . . 9 <Q ⊆ (Q × Q)
31, 2sotri 4934 . . . . . . . 8 ((𝑦 <Q 𝑞𝑞 <Q 𝑟) → 𝑦 <Q 𝑟)
43expcom 115 . . . . . . 7 (𝑞 <Q 𝑟 → (𝑦 <Q 𝑞𝑦 <Q 𝑟))
54anim1d 334 . . . . . 6 (𝑞 <Q 𝑟 → ((𝑦 <Q 𝑞 ∧ (*Q𝑦) ∈ (1st𝐴)) → (𝑦 <Q 𝑟 ∧ (*Q𝑦) ∈ (1st𝐴))))
65eximdv 1852 . . . . 5 (𝑞 <Q 𝑟 → (∃𝑦(𝑦 <Q 𝑞 ∧ (*Q𝑦) ∈ (1st𝐴)) → ∃𝑦(𝑦 <Q 𝑟 ∧ (*Q𝑦) ∈ (1st𝐴))))
7 recexpr.1 . . . . . 6 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
87recexprlemelu 7438 . . . . 5 (𝑞 ∈ (2nd𝐵) ↔ ∃𝑦(𝑦 <Q 𝑞 ∧ (*Q𝑦) ∈ (1st𝐴)))
97recexprlemelu 7438 . . . . 5 (𝑟 ∈ (2nd𝐵) ↔ ∃𝑦(𝑦 <Q 𝑟 ∧ (*Q𝑦) ∈ (1st𝐴)))
106, 8, 93imtr4g 204 . . . 4 (𝑞 <Q 𝑟 → (𝑞 ∈ (2nd𝐵) → 𝑟 ∈ (2nd𝐵)))
1110imp 123 . . 3 ((𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)) → 𝑟 ∈ (2nd𝐵))
1211rexlimivw 2545 . 2 (∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)) → 𝑟 ∈ (2nd𝐵))
1312a1i 9 1 ((𝐴P𝑟Q) → (∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)) → 𝑟 ∈ (2nd𝐵)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1331  ∃wex 1468   ∈ wcel 1480  {cab 2125  ∃wrex 2417  ⟨cop 3530   class class class wbr 3929  ‘cfv 5123  1st c1st 6036  2nd c2nd 6037  Qcnq 7095  *Qcrq 7099
 Copyright terms: Public domain W3C validator