Theorem suprcld

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

	Ref	Expression
Hypotheses	suprcld.2	$$⊢\phi \to A\subseteq ℝ$$
	suprcld.1	$$⊢\phi \to A\ne \varnothing$$
	suprcld.4	$$⊢\phi \to \exists x\in ℝ\forall y\in Ay\le x$$
Assertion	suprcld	$$⊢\phi \to sup\left(A,ℝ,<\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		suprcld.2	$$⊢\phi \to A\subseteq ℝ$$
2		suprcld.1	$$⊢\phi \to A\ne \varnothing$$
3		suprcld.4	$$⊢\phi \to \exists x\in ℝ\forall y\in Ay\le x$$
4		suprcl	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists x\in ℝ\forall y\in Ay\le x\right)\to sup\left(A,ℝ,<\right)\in ℝ$$
5	1 2 3 4	syl3anc	$$⊢\phi \to sup\left(A,ℝ,<\right)\in ℝ$$