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

Theorem recexprlempr 7462
 Description: 𝐵 is a positive real. Lemma for recexpr 7468. (Contributed by Jim Kingdon, 27-Dec-2019.)
Hypothesis
Ref Expression
recexpr.1 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
Assertion
Ref Expression
recexprlempr (𝐴P𝐵P)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Proof of Theorem recexprlempr
Dummy variables 𝑟 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 recexpr.1 . . . 4 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
21recexprlemm 7454 . . 3 (𝐴P → (∃𝑞Q 𝑞 ∈ (1st𝐵) ∧ ∃𝑟Q 𝑟 ∈ (2nd𝐵)))
3 ltrelnq 7195 . . . . . . . . . . 11 <Q ⊆ (Q × Q)
43brel 4597 . . . . . . . . . 10 (𝑥 <Q 𝑦 → (𝑥Q𝑦Q))
54simpld 111 . . . . . . . . 9 (𝑥 <Q 𝑦𝑥Q)
65adantr 274 . . . . . . . 8 ((𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → 𝑥Q)
76exlimiv 1578 . . . . . . 7 (∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) → 𝑥Q)
87abssi 3175 . . . . . 6 {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))} ⊆ Q
9 nqex 7193 . . . . . . 7 Q ∈ V
109elpw2 4088 . . . . . 6 ({𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))} ∈ 𝒫 Q ↔ {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))} ⊆ Q)
118, 10mpbir 145 . . . . 5 {𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))} ∈ 𝒫 Q
123brel 4597 . . . . . . . . . 10 (𝑦 <Q 𝑥 → (𝑦Q𝑥Q))
1312simprd 113 . . . . . . . . 9 (𝑦 <Q 𝑥𝑥Q)
1413adantr 274 . . . . . . . 8 ((𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴)) → 𝑥Q)
1514exlimiv 1578 . . . . . . 7 (∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴)) → 𝑥Q)
1615abssi 3175 . . . . . 6 {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))} ⊆ Q
179elpw2 4088 . . . . . 6 ({𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))} ∈ 𝒫 Q ↔ {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))} ⊆ Q)
1816, 17mpbir 145 . . . . 5 {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))} ∈ 𝒫 Q
19 opelxpi 4577 . . . . 5 (({𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))} ∈ 𝒫 Q ∧ {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))} ∈ 𝒫 Q) → ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩ ∈ (𝒫 Q × 𝒫 Q))
2011, 18, 19mp2an 423 . . . 4 ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩ ∈ (𝒫 Q × 𝒫 Q)
211, 20eqeltri 2213 . . 3 𝐵 ∈ (𝒫 Q × 𝒫 Q)
222, 21jctil 310 . 2 (𝐴P → (𝐵 ∈ (𝒫 Q × 𝒫 Q) ∧ (∃𝑞Q 𝑞 ∈ (1st𝐵) ∧ ∃𝑟Q 𝑟 ∈ (2nd𝐵))))
231recexprlemrnd 7459 . . 3 (𝐴P → (∀𝑞Q (𝑞 ∈ (1st𝐵) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵))) ∧ ∀𝑟Q (𝑟 ∈ (2nd𝐵) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)))))
241recexprlemdisj 7460 . . 3 (𝐴P → ∀𝑞Q ¬ (𝑞 ∈ (1st𝐵) ∧ 𝑞 ∈ (2nd𝐵)))
251recexprlemloc 7461 . . 3 (𝐴P → ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st𝐵) ∨ 𝑟 ∈ (2nd𝐵))))
2623, 24, 253jca 1162 . 2 (𝐴P → ((∀𝑞Q (𝑞 ∈ (1st𝐵) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵))) ∧ ∀𝑟Q (𝑟 ∈ (2nd𝐵) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)))) ∧ ∀𝑞Q ¬ (𝑞 ∈ (1st𝐵) ∧ 𝑞 ∈ (2nd𝐵)) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st𝐵) ∨ 𝑟 ∈ (2nd𝐵)))))
27 elnp1st2nd 7306 . 2 (𝐵P ↔ ((𝐵 ∈ (𝒫 Q × 𝒫 Q) ∧ (∃𝑞Q 𝑞 ∈ (1st𝐵) ∧ ∃𝑟Q 𝑟 ∈ (2nd𝐵))) ∧ ((∀𝑞Q (𝑞 ∈ (1st𝐵) ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟 ∈ (1st𝐵))) ∧ ∀𝑟Q (𝑟 ∈ (2nd𝐵) ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞 ∈ (2nd𝐵)))) ∧ ∀𝑞Q ¬ (𝑞 ∈ (1st𝐵) ∧ 𝑞 ∈ (2nd𝐵)) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st𝐵) ∨ 𝑟 ∈ (2nd𝐵))))))
2822, 26, 27sylanbrc 414 1 (𝐴P𝐵P)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698   ∧ w3a 963   = wceq 1332  ∃wex 1469   ∈ wcel 1481  {cab 2126  ∀wral 2417  ∃wrex 2418   ⊆ wss 3074  𝒫 cpw 3513  ⟨cop 3533   class class class wbr 3935   × cxp 4543  ‘cfv 5129  1st c1st 6042  2nd c2nd 6043  Qcnq 7110  *Qcrq 7114
 Copyright terms: Public domain W3C validator