Theorem suprlubrd

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

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

Proof

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