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 ( 𝐵 , ℝ* , < ) )