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

Theorem prml 6460
 Description: A positive real's lower cut is inhabited. (Contributed by Jim Kingdon, 27-Sep-2019.)
Assertion
Ref Expression
prml (⟨𝐿, 𝑈 Px Q x 𝐿)
Distinct variable groups:   x,𝐿   x,𝑈

Proof of Theorem prml
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 elinp 6457 . 2 (⟨𝐿, 𝑈 P ↔ (((𝐿Q 𝑈Q) (x Q x 𝐿 y Q y 𝑈)) ((x Q (x 𝐿y Q (x <Q y y 𝐿)) y Q (y 𝑈x Q (x <Q y x 𝑈))) x Q ¬ (x 𝐿 x 𝑈) x Q y Q (x <Q y → (x 𝐿 y 𝑈)))))
2 simplrl 487 . 2 ((((𝐿Q 𝑈Q) (x Q x 𝐿 y Q y 𝑈)) ((x Q (x 𝐿y Q (x <Q y y 𝐿)) y Q (y 𝑈x Q (x <Q y x 𝑈))) x Q ¬ (x 𝐿 x 𝑈) x Q y Q (x <Q y → (x 𝐿 y 𝑈)))) → x Q x 𝐿)
31, 2sylbi 114 1 (⟨𝐿, 𝑈 Px Q x 𝐿)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628   ∧ w3a 884   ∈ wcel 1390  ∀wral 2300  ∃wrex 2301   ⊆ wss 2911  ⟨cop 3370   class class class wbr 3755  Qcnq 6264
 Copyright terms: Public domain W3C validator