Theorem suprubd

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

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

Proof

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