This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem supxrss

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

Ref Expression
Assertion supxrss ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ* ) → sup ( 𝐴 , ℝ* , < ) ≤ sup ( 𝐵 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 simplr ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ ℝ* )
2 simpl ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ* ) → 𝐴 ⊆ 𝐵 )
3 2 sselda ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
4 supxrub ⊢ ( ( 𝐵 ⊆ ℝ* ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ≤ sup ( 𝐵 , ℝ* , < ) )
5 1 3 4 syl2anc ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ* ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ sup ( 𝐵 , ℝ* , < ) )
6 5 ralrimiva ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ* ) → ∀ 𝑥 ∈ 𝐴 𝑥 ≤ sup ( 𝐵 , ℝ* , < ) )
7 sstr ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ* ) → 𝐴 ⊆ ℝ* )
8 supxrcl ⊢ ( 𝐵 ⊆ ℝ* → sup ( 𝐵 , ℝ* , < ) ∈ ℝ* )
9 8 adantl ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ* ) → sup ( 𝐵 , ℝ* , < ) ∈ ℝ* )
10 supxrleub ⊢ ( ( 𝐴 ⊆ ℝ* ∧ sup ( 𝐵 , ℝ* , < ) ∈ ℝ* ) → ( sup ( 𝐴 , ℝ* , < ) ≤ sup ( 𝐵 , ℝ* , < ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ sup ( 𝐵 , ℝ* , < ) ) )
11 7 9 10 syl2anc ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ* ) → ( sup ( 𝐴 , ℝ* , < ) ≤ sup ( 𝐵 , ℝ* , < ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ sup ( 𝐵 , ℝ* , < ) ) )
12 6 11 mpbird ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ* ) → sup ( 𝐴 , ℝ* , < ) ≤ sup ( 𝐵 , ℝ* , < ) )