Metamath Proof Explorer


Theorem suprcld

Description: Natural deduction form of suprcl . (Contributed by Stanislas Polu, 9-Mar-2020)

Ref Expression
Hypotheses suprcld.2
|- ( ph -> A C_ RR )
suprcld.1
|- ( ph -> A =/= (/) )
suprcld.4
|- ( ph -> E. x e. RR A. y e. A y <_ x )
Assertion suprcld
|- ( ph -> sup ( A , RR , < ) e. RR )

Proof

Step Hyp Ref Expression
1 suprcld.2
 |-  ( ph -> A C_ RR )
2 suprcld.1
 |-  ( ph -> A =/= (/) )
3 suprcld.4
 |-  ( ph -> E. x e. RR A. y e. A y <_ x )
4 suprcl
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )
5 1 2 3 4 syl3anc
 |-  ( ph -> sup ( A , RR , < ) e. RR )