Theorem xrsupssd

Description: Inequality deduction for supremum of an extended real subset. (Contributed by Thierry Arnoux, 21-Mar-2017)

	Ref	Expression
Hypotheses	xrsupssd.1	$$⊢\phi \to B\subseteq C$$
	xrsupssd.2	$$⊢\phi \to C\subseteq {ℝ}^{*}$$
Assertion	xrsupssd	$$⊢\phi \to sup\left(B,{ℝ}^{*},<\right)\le sup\left(C,{ℝ}^{*},<\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrsupssd.1	$$⊢\phi \to B\subseteq C$$
2		xrsupssd.2	$$⊢\phi \to C\subseteq {ℝ}^{*}$$
3		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
4	3	a1i	$$⊢\phi \to <\mathrm{Or}{ℝ}^{*}$$
5	1 2	sstrd	$$⊢\phi \to B\subseteq {ℝ}^{*}$$
6		xrsupss	$$⊢B\subseteq {ℝ}^{*}\to \exists x\in {ℝ}^{*}\left(\forall y\in B\neg x<y\wedge \forall y\in {ℝ}^{*}\left(y<x\to \exists z\in By<z\right)\right)$$
7	5 6	syl	$$⊢\phi \to \exists x\in {ℝ}^{*}\left(\forall y\in B\neg x<y\wedge \forall y\in {ℝ}^{*}\left(y<x\to \exists z\in By<z\right)\right)$$
8		xrsupss	$$⊢C\subseteq {ℝ}^{*}\to \exists x\in {ℝ}^{*}\left(\forall y\in C\neg x<y\wedge \forall y\in {ℝ}^{*}\left(y<x\to \exists z\in Cy<z\right)\right)$$
9	2 8	syl	$$⊢\phi \to \exists x\in {ℝ}^{*}\left(\forall y\in C\neg x<y\wedge \forall y\in {ℝ}^{*}\left(y<x\to \exists z\in Cy<z\right)\right)$$
10	4 1 2 7 9	supssd	$$⊢\phi \to \neg sup\left(C,{ℝ}^{*},<\right)<sup\left(B,{ℝ}^{*},<\right)$$
11	4 7	supcl	$$⊢\phi \to sup\left(B,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
12	4 9	supcl	$$⊢\phi \to sup\left(C,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
13		xrlenlt	$$⊢\left(sup\left(B,{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge sup\left(C,{ℝ}^{*},<\right)\in {ℝ}^{*}\right)\to \left(sup\left(B,{ℝ}^{*},<\right)\le sup\left(C,{ℝ}^{*},<\right)\leftrightarrow \neg sup\left(C,{ℝ}^{*},<\right)<sup\left(B,{ℝ}^{*},<\right)\right)$$
14	11 12 13	syl2anc	$$⊢\phi \to \left(sup\left(B,{ℝ}^{*},<\right)\le sup\left(C,{ℝ}^{*},<\right)\leftrightarrow \neg sup\left(C,{ℝ}^{*},<\right)<sup\left(B,{ℝ}^{*},<\right)\right)$$
15	10 14	mpbird	$$⊢\phi \to sup\left(B,{ℝ}^{*},<\right)\le sup\left(C,{ℝ}^{*},<\right)$$