infxrss

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	$⊢ (A \subseteq B \land B \subseteq ℝ^{}) \to sup (B ℝ^{} <) \leq sup (A ℝ^{*} <)$

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		infxrlb	$⊢ (B \subseteq ℝ^{} \land x \in B) \to sup (B ℝ^{} <) \leq x$
5	1 3 4	syl2anc	$⊢ ((A \subseteq B \land B \subseteq ℝ^{}) \land x \in A) \to sup (B ℝ^{} <) \leq x$
6	5	ralrimiva	$⊢ (A \subseteq B \land B \subseteq ℝ^{}) \to \forall x \in A sup (B ℝ^{} <) \leq x$
7		sstr	$⊢ (A \subseteq B \land B \subseteq ℝ^{}) \to A \subseteq ℝ^{}$
8		infxrcl	$⊢ B \subseteq ℝ^{} \to sup (B ℝ^{} <) \in ℝ^{*}$
9	8	adantl	$⊢ (A \subseteq B \land B \subseteq ℝ^{}) \to sup (B ℝ^{} <) \in ℝ^{*}$
10		infxrgelb	$⊢ (A \subseteq ℝ^{} \land sup (B ℝ^{} <) \in ℝ^{}) \to (sup (B ℝ^{} <) \leq sup (A ℝ^{} <) \leftrightarrow \forall x \in A sup (B ℝ^{} <) \leq x)$
11	7 9 10	syl2anc	$⊢ (A \subseteq B \land B \subseteq ℝ^{}) \to (sup (B ℝ^{} <) \leq sup (A ℝ^{} <) \leftrightarrow \forall x \in A sup (B ℝ^{} <) \leq x)$
12	6 11	mpbird	$⊢ (A \subseteq B \land B \subseteq ℝ^{}) \to sup (B ℝ^{} <) \leq sup (A ℝ^{*} <)$

Metamath Proof Explorer