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

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

Proof of Theorem prmu
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 elinp 6457 . 2 (⟨𝐿, 𝑈 P ↔ (((𝐿Q 𝑈Q) (y Q y 𝐿 x Q x 𝑈)) ((y Q (y 𝐿x Q (y <Q x x 𝐿)) x Q (x 𝑈y Q (y <Q x y 𝑈))) y Q ¬ (y 𝐿 y 𝑈) y Q x Q (y <Q x → (y 𝐿 x 𝑈)))))
2 simplrr 488 . 2 ((((𝐿Q 𝑈Q) (y Q y 𝐿 x Q x 𝑈)) ((y Q (y 𝐿x Q (y <Q x x 𝐿)) x Q (x 𝑈y Q (y <Q x y 𝑈))) y Q ¬ (y 𝐿 y 𝑈) y Q x Q (y <Q x → (y 𝐿 x 𝑈)))) → 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