# Metamath Proof Explorer

Description: Larger sets of extended reals have smaller infima. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 13-Sep-2020)

Ref Expression
Assertion infxrss ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\to sup\left({B},{ℝ}^{*},<\right)\le sup\left({A},{ℝ}^{*},<\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 infxrlb ${⊢}\left({B}\subseteq {ℝ}^{*}\wedge {x}\in {B}\right)\to sup\left({B},{ℝ}^{*},<\right)\le {x}$
5 1 3 4 syl2anc ${⊢}\left(\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\wedge {x}\in {A}\right)\to sup\left({B},{ℝ}^{*},<\right)\le {x}$
6 5 ralrimiva ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}sup\left({B},{ℝ}^{*},<\right)\le {x}$
7 sstr ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\to {A}\subseteq {ℝ}^{*}$
8 infxrcl ${⊢}{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 infxrgelb ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge sup\left({B},{ℝ}^{*},<\right)\in {ℝ}^{*}\right)\to \left(sup\left({B},{ℝ}^{*},<\right)\le sup\left({A},{ℝ}^{*},<\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}sup\left({B},{ℝ}^{*},<\right)\le {x}\right)$
11 7 9 10 syl2anc ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\to \left(sup\left({B},{ℝ}^{*},<\right)\le sup\left({A},{ℝ}^{*},<\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}sup\left({B},{ℝ}^{*},<\right)\le {x}\right)$
12 6 11 mpbird ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {ℝ}^{*}\right)\to sup\left({B},{ℝ}^{*},<\right)\le sup\left({A},{ℝ}^{*},<\right)$