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

Theorem prml 6633
 Description: A positive real's lower cut is inhabited. (Contributed by Jim Kingdon, 27-Sep-2019.)
Assertion
Ref Expression
prml (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥Q 𝑥𝐿)
Distinct variable groups:   𝑥,𝐿   𝑥,𝑈

Proof of Theorem prml
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 elinp 6630 . 2 (⟨𝐿, 𝑈⟩ ∈ P ↔ (((𝐿Q𝑈Q) ∧ (∃𝑥Q 𝑥𝐿 ∧ ∃𝑦Q 𝑦𝑈)) ∧ ((∀𝑥Q (𝑥𝐿 ↔ ∃𝑦Q (𝑥 <Q 𝑦𝑦𝐿)) ∧ ∀𝑦Q (𝑦𝑈 ↔ ∃𝑥Q (𝑥 <Q 𝑦𝑥𝑈))) ∧ ∀𝑥Q ¬ (𝑥𝐿𝑥𝑈) ∧ ∀𝑥Q𝑦Q (𝑥 <Q 𝑦 → (𝑥𝐿𝑦𝑈)))))
2 simplrl 495 . 2 ((((𝐿Q𝑈Q) ∧ (∃𝑥Q 𝑥𝐿 ∧ ∃𝑦Q 𝑦𝑈)) ∧ ((∀𝑥Q (𝑥𝐿 ↔ ∃𝑦Q (𝑥 <Q 𝑦𝑦𝐿)) ∧ ∀𝑦Q (𝑦𝑈 ↔ ∃𝑥Q (𝑥 <Q 𝑦𝑥𝑈))) ∧ ∀𝑥Q ¬ (𝑥𝐿𝑥𝑈) ∧ ∀𝑥Q𝑦Q (𝑥 <Q 𝑦 → (𝑥𝐿𝑦𝑈)))) → ∃𝑥Q 𝑥𝐿)
31, 2sylbi 118 1 (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥Q 𝑥𝐿)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 101   ↔ wb 102   ∨ wo 639   ∧ w3a 896   ∈ wcel 1409  ∀wral 2323  ∃wrex 2324   ⊆ wss 2945  ⟨cop 3406   class class class wbr 3792  Qcnq 6436
 Copyright terms: Public domain W3C validator