Theorem suprleubrd

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

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

Proof

Step	Hyp	Ref	Expression
1		suprleubrd.1	$$⊢\phi \to A\subseteq ℝ$$
2		suprleubrd.2	$$⊢\phi \to A\ne \varnothing$$
3		suprleubrd.3	$$⊢\phi \to \exists x\in ℝ\forall y\in Ay\le x$$
4		suprleubrd.4	$$⊢\phi \to B\in ℝ$$
5		suprleubrd.5	$$⊢\phi \to \forall z\in Az\le B$$
6		suprleub	$$⊢\left(\left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists x\in ℝ\forall y\in Ay\le x\right)\wedge B\in ℝ\right)\to \left(sup\left(A,ℝ,<\right)\le B\leftrightarrow \forall z\in Az\le B\right)$$
7	1 2 3 4 6	syl31anc	$$⊢\phi \to \left(sup\left(A,ℝ,<\right)\le B\leftrightarrow \forall z\in Az\le B\right)$$
8	7	bicomd	$$⊢\phi \to \left(\forall z\in Az\le B\leftrightarrow sup\left(A,ℝ,<\right)\le B\right)$$
9	8	biimpd	$$⊢\phi \to \left(\forall z\in Az\le B\to sup\left(A,ℝ,<\right)\le B\right)$$
10	9	imp	$$⊢\left(\phi \wedge \forall z\in Az\le B\right)\to sup\left(A,ℝ,<\right)\le B$$
11	5 10	mpdan	$$⊢\phi \to sup\left(A,ℝ,<\right)\le B$$