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 ) |
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 ) |