supxrss

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

		Ref	Expression
	Assertion	supxrss	$⊢ (A \subseteq B \land B \subseteq ℝ^{}) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <)$

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((A \subseteq B \land B \subseteq ℝ^{}) \land x \in A) \to B \subseteq ℝ^{}$
2		simpl	$⊢ (A \subseteq B \land B \subseteq ℝ^{*}) \to A \subseteq B$
3	2	sselda	$⊢ ((A \subseteq B \land B \subseteq ℝ^{*}) \land x \in A) \to x \in B$
4		supxrub	$⊢ (B \subseteq ℝ^{} \land x \in B) \to x \leq sup (B ℝ^{} <)$
5	1 3 4	syl2anc	$⊢ ((A \subseteq B \land B \subseteq ℝ^{}) \land x \in A) \to x \leq sup (B ℝ^{} <)$
6	5	ralrimiva	$⊢ (A \subseteq B \land B \subseteq ℝ^{}) \to \forall x \in A x \leq sup (B ℝ^{} <)$
7		sstr	$⊢ (A \subseteq B \land B \subseteq ℝ^{}) \to A \subseteq ℝ^{}$
8		supxrcl	$⊢ B \subseteq ℝ^{} \to sup (B ℝ^{} <) \in ℝ^{*}$
9	8	adantl	$⊢ (A \subseteq B \land B \subseteq ℝ^{}) \to sup (B ℝ^{} <) \in ℝ^{*}$
10		supxrleub	$⊢ (A \subseteq ℝ^{} \land sup (B ℝ^{} <) \in ℝ^{}) \to (sup (A ℝ^{} <) \leq sup (B ℝ^{} <) \leftrightarrow \forall x \in A x \leq sup (B ℝ^{} <))$
11	7 9 10	syl2anc	$⊢ (A \subseteq B \land B \subseteq ℝ^{}) \to (sup (A ℝ^{} <) \leq sup (B ℝ^{} <) \leftrightarrow \forall x \in A x \leq sup (B ℝ^{} <))$
12	6 11	mpbird	$⊢ (A \subseteq B \land B \subseteq ℝ^{}) \to sup (A ℝ^{} <) \leq sup (B ℝ^{*} <)$

Metamath Proof Explorer