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

Theorem prml 6325
 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 6322 . 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 475 . 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 616   ∧ w3a 871   ∈ wcel 1370  ∀wral 2280  ∃wrex 2281   ⊆ wss 2890  ⟨cop 3349   class class class wbr 3734  Qcnq 6134
 Copyright terms: Public domain W3C validator