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

Theorem recexprlemrnd 6727
 Description: 𝐵 is rounded. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.)
Hypothesis
Ref Expression
recexpr.1 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
Assertion
Ref Expression
recexprlemrnd (𝐴P → (∀𝑞Q (𝑞 ∈ (1st𝐵) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵))) ∧ ∀𝑟Q (𝑟 ∈ (2nd𝐵) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)))))
Distinct variable groups:   𝑟,𝑞,𝑥,𝑦,𝐴   𝐵,𝑞,𝑟,𝑥,𝑦

Proof of Theorem recexprlemrnd
StepHypRef Expression
1 recexpr.1 . . . . . 6 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
21recexprlemopl 6723 . . . . 5 ((𝐴P𝑞Q𝑞 ∈ (1st𝐵)) → ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵)))
323expia 1106 . . . 4 ((𝐴P𝑞Q) → (𝑞 ∈ (1st𝐵) → ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵))))
41recexprlemlol 6724 . . . 4 ((𝐴P𝑞Q) → (∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵)) → 𝑞 ∈ (1st𝐵)))
53, 4impbid 120 . . 3 ((𝐴P𝑞Q) → (𝑞 ∈ (1st𝐵) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵))))
65ralrimiva 2392 . 2 (𝐴P → ∀𝑞Q (𝑞 ∈ (1st𝐵) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵))))
71recexprlemopu 6725 . . . . 5 ((𝐴P𝑟Q𝑟 ∈ (2nd𝐵)) → ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)))
873expia 1106 . . . 4 ((𝐴P𝑟Q) → (𝑟 ∈ (2nd𝐵) → ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))))
91recexprlemupu 6726 . . . 4 ((𝐴P𝑟Q) → (∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)) → 𝑟 ∈ (2nd𝐵)))
108, 9impbid 120 . . 3 ((𝐴P𝑟Q) → (𝑟 ∈ (2nd𝐵) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))))
1110ralrimiva 2392 . 2 (𝐴P → ∀𝑟Q (𝑟 ∈ (2nd𝐵) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵))))
126, 11jca 290 1 (𝐴P → (∀𝑞Q (𝑞 ∈ (1st𝐵) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵))) ∧ ∀𝑟Q (𝑟 ∈ (2nd𝐵) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1243  ∃wex 1381   ∈ wcel 1393  {cab 2026  ∀wral 2306  ∃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