liminfgord

Description: Ordering property of the inferior limit function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

		Ref	Expression
	Assertion	liminfgord	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to inf (F [[A, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (F [[B, +∞)] \cap ℝ^{} ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		inss2	$⊢ F [[A, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
2	1	a1i	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land x \in (F [[B, +∞)] \cap ℝ^{})) \to F [[A, +∞)] \cap ℝ^{} \subseteq ℝ^{*}$
3		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
4	3	3ad2ant1	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to A \in ℝ^{*}$
5		simp3	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to A \leq B$
6		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
7		xrletr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land w \in ℝ^{*}) \to ((A \leq B \land B \leq w) \to A \leq w)$
8	6 6 7	ixxss1	$⊢ (A \in ℝ^{*} \land A \leq B) \to [B, +∞) \subseteq [A, +∞)$
9	4 5 8	syl2anc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to [B, +∞) \subseteq [A, +∞)$
10		imass2	$⊢ [B, +∞) \subseteq [A, +∞) \to F [[B, +∞)] \subseteq F [[A, +∞)]$
11		ssrin	$⊢ F [[B, +∞)] \subseteq F [[A, +∞)] \to F [[B, +∞)] \cap ℝ^{} \subseteq F [[A, +∞)] \cap ℝ^{}$
12	9 10 11	3syl	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to F [[B, +∞)] \cap ℝ^{} \subseteq F [[A, +∞)] \cap ℝ^{}$
13	12	sselda	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land x \in (F [[B, +∞)] \cap ℝ^{})) \to x \in (F [[A, +∞)] \cap ℝ^{})$
14		infxrlb	$⊢ (F [[A, +∞)] \cap ℝ^{} \subseteq ℝ^{} \land x \in (F [[A, +∞)] \cap ℝ^{})) \to inf (F [[A, +∞)] \cap ℝ^{} ℝ^{*} <) \leq x$
15	2 13 14	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ \land A \leq B) \land x \in (F [[B, +∞)] \cap ℝ^{})) \to inf (F [[A, +∞)] \cap ℝ^{} ℝ^{*} <) \leq x$
16	15	ralrimiva	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to \forall x \in (F [[B, +∞)] \cap ℝ^{}) inf (F [[A, +∞)] \cap ℝ^{} ℝ^{*} <) \leq x$
17		inss2	$⊢ F [[B, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
18		infxrcl	$⊢ F [[A, +∞)] \cap ℝ^{} \subseteq ℝ^{} \to inf (F [[A, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
19	1 18	ax-mp	$⊢ inf (F [[A, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
20		infxrgelb	$⊢ (F [[B, +∞)] \cap ℝ^{} \subseteq ℝ^{} \land inf (F [[A, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{}) \to (inf (F [[A, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (F [[B, +∞)] \cap ℝ^{} ℝ^{} <) \leftrightarrow \forall x \in (F [[B, +∞)] \cap ℝ^{}) inf (F [[A, +∞)] \cap ℝ^{} ℝ^{} <) \leq x)$
21	17 19 20	mp2an	$⊢ inf (F [[A, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (F [[B, +∞)] \cap ℝ^{} ℝ^{} <) \leftrightarrow \forall x \in (F [[B, +∞)] \cap ℝ^{}) inf (F [[A, +∞)] \cap ℝ^{} ℝ^{*} <) \leq x$
22	16 21	sylibr	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to inf (F [[A, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (F [[B, +∞)] \cap ℝ^{} ℝ^{} <)$

Metamath Proof Explorer

Theorem liminfgord

Proof