limsupgord

Description: Ordering property of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by Mario Carneiro, 7-May-2016)

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

Proof

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

Metamath Proof Explorer

Theorem limsupgord

Proof