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

Theorem ltexprlemrnd 6761
 Description: Our constructed difference is rounded. Lemma for ltexpri 6769. (Contributed by Jim Kingdon, 17-Dec-2019.)
Hypothesis
Ref Expression
ltexprlem.1 𝐶 = ⟨{𝑥Q ∣ ∃𝑦(𝑦 ∈ (2nd𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st𝐵))}, {𝑥Q ∣ ∃𝑦(𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd𝐵))}⟩
Assertion
Ref Expression
ltexprlemrnd (𝐴<P 𝐵 → (∀𝑞Q (𝑞 ∈ (1st𝐶) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐶))) ∧ ∀𝑟Q (𝑟 ∈ (2nd𝐶) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐶)))))
Distinct variable groups:   𝑥,𝑦,𝑞,𝑟,𝐴   𝑥,𝐵,𝑦,𝑞,𝑟   𝑥,𝐶,𝑦,𝑞,𝑟

Proof of Theorem ltexprlemrnd
StepHypRef Expression
1 ltexprlem.1 . . . . . 6 𝐶 = ⟨{𝑥Q ∣ ∃𝑦(𝑦 ∈ (2nd𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st𝐵))}, {𝑥Q ∣ ∃𝑦(𝑦 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd𝐵))}⟩
21ltexprlemopl 6757 . . . . 5 ((𝐴<P 𝐵𝑞Q𝑞 ∈ (1st𝐶)) → ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐶)))
323expia 1117 . . . 4 ((𝐴<P 𝐵𝑞Q) → (𝑞 ∈ (1st𝐶) → ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐶))))
41ltexprlemlol 6758 . . . 4 ((𝐴<P 𝐵𝑞Q) → (∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐶)) → 𝑞 ∈ (1st𝐶)))
53, 4impbid 124 . . 3 ((𝐴<P 𝐵𝑞Q) → (𝑞 ∈ (1st𝐶) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐶))))
65ralrimiva 2409 . 2 (𝐴<P 𝐵 → ∀𝑞Q (𝑞 ∈ (1st𝐶) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐶))))
71ltexprlemopu 6759 . . . . 5 ((𝐴<P 𝐵𝑟Q𝑟 ∈ (2nd𝐶)) → ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐶)))
873expia 1117 . . . 4 ((𝐴<P 𝐵𝑟Q) → (𝑟 ∈ (2nd𝐶) → ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐶))))
91ltexprlemupu 6760 . . . 4 ((𝐴<P 𝐵𝑟Q) → (∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐶)) → 𝑟 ∈ (2nd𝐶)))
108, 9impbid 124 . . 3 ((𝐴<P 𝐵𝑟Q) → (𝑟 ∈ (2nd𝐶) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐶))))
1110ralrimiva 2409 . 2 (𝐴<P 𝐵 → ∀𝑟Q (𝑟 ∈ (2nd𝐶) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐶))))
126, 11jca 294 1 (𝐴<P 𝐵 → (∀𝑞Q (𝑞 ∈ (1st𝐶) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐶))) ∧ ∀𝑟Q (𝑟 ∈ (2nd𝐶) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐶)))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   = wceq 1259  ∃wex 1397   ∈ wcel 1409  ∀wral 2323  ∃wrex 2324  {crab 2327  ⟨cop 3406   class class class wbr 3792  ‘cfv 4930  (class class class)co 5540  1st c1st 5793  2nd c2nd 5794  Qcnq 6436   +Q cplq 6438
 Copyright terms: Public domain W3C validator