# Metamath Proof Explorer

Description: Smaller sets of extended reals have smaller suprema. (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion supxrss ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\to sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)$

### Proof

Step Hyp Ref Expression
1 simplr ${⊢}\left(\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\wedge {x}\in {A}\right)\to {B}\subseteq {ℝ}^{*}$
2 simpl ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\to {A}\subseteq {B}$
3 2 sselda ${⊢}\left(\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\wedge {x}\in {A}\right)\to {x}\in {B}$
4 supxrub ${⊢}\left({B}\subseteq {ℝ}^{*}\wedge {x}\in {B}\right)\to {x}\le sup\left({B},{ℝ}^{*},<\right)$
5 1 3 4 syl2anc ${⊢}\left(\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\wedge {x}\in {A}\right)\to {x}\le sup\left({B},{ℝ}^{*},<\right)$
6 5 ralrimiva ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le sup\left({B},{ℝ}^{*},<\right)$
7 sstr ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\to {A}\subseteq {ℝ}^{*}$
8 supxrcl ${⊢}{B}\subseteq {ℝ}^{*}\to sup\left({B},{ℝ}^{*},<\right)\in {ℝ}^{*}$
9 8 adantl ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\to sup\left({B},{ℝ}^{*},<\right)\in {ℝ}^{*}$
10 supxrleub ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge sup\left({B},{ℝ}^{*},<\right)\in {ℝ}^{*}\right)\to \left(sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le sup\left({B},{ℝ}^{*},<\right)\right)$
11 7 9 10 syl2anc ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\to \left(sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le sup\left({B},{ℝ}^{*},<\right)\right)$
12 6 11 mpbird ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\to sup\left({A},{ℝ}^{*},<\right)\le sup\left({B},{ℝ}^{*},<\right)$