limsupres

Description: The superior limit of a restriction is less than or equal to the original superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

		Ref	Expression
	Hypothesis	limsupres.1	$⊢ φ \to F \in V$
	Assertion	limsupres	$⊢ φ \to lim sup ({F ↾}_{C}) \leq lim sup (F)$

Proof

Step	Hyp	Ref	Expression
1		limsupres.1	$⊢ φ \to F \in V$
2		nfv	$⊢ Ⅎ k φ$
3		resimass	$⊢ ({F ↾}_{C}) [[k, +∞)] \subseteq F [[k, +∞)]$
4	3	a1i	$⊢ k \in ℝ \to ({F ↾}_{C}) [[k, +∞)] \subseteq F [[k, +∞)]$
5	4	ssrind	$⊢ k \in ℝ \to ({F ↾}_{C}) [[k, +∞)] \cap ℝ^{} \subseteq F [[k, +∞)] \cap ℝ^{}$
6	5	adantl	$⊢ (φ \land k \in ℝ) \to ({F ↾}_{C}) [[k, +∞)] \cap ℝ^{} \subseteq F [[k, +∞)] \cap ℝ^{}$
7		inss2	$⊢ F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
8	7	a1i	$⊢ (φ \land k \in ℝ) \to F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
9	6 8	sstrd	$⊢ (φ \land k \in ℝ) \to ({F ↾}_{C}) [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
10	9	supxrcld	$⊢ (φ \land k \in ℝ) \to sup (({F ↾}_{C}) [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
11	8	supxrcld	$⊢ (φ \land k \in ℝ) \to sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
12		supxrss	$⊢ (({F ↾}_{C}) [[k, +∞)] \cap ℝ^{} \subseteq F [[k, +∞)] \cap ℝ^{} \land F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}) \to sup (({F ↾}_{C}) [[k, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)$
13	6 8 12	syl2anc	$⊢ (φ \land k \in ℝ) \to sup (({F ↾}_{C}) [[k, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)$
14	2 10 11 13	infrnmptle	$⊢ φ \to inf (ran (k \in ℝ ⟼ sup (({F ↾}_{C}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \leq inf (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
15	1	resexd	$⊢ φ \to {F ↾}_{C} \in V$
16		eqid	$⊢ (k \in ℝ ⟼ sup (({F ↾}_{C}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup (({F ↾}_{C}) [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
17	16	limsupval	$⊢ {F ↾}_{C} \in V \to lim sup ({F ↾}_{C}) = inf (ran (k \in ℝ ⟼ sup (({F ↾}_{C}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
18	15 17	syl	$⊢ φ \to lim sup ({F ↾}_{C}) = inf (ran (k \in ℝ ⟼ sup (({F ↾}_{C}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
19		eqid	$⊢ (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
20	19	limsupval	$⊢ F \in V \to lim sup (F) = inf (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
21	1 20	syl	$⊢ φ \to lim sup (F) = inf (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
22	18 21	breq12d	$⊢ φ \to (lim sup ({F ↾}_{C}) \leq lim sup (F) \leftrightarrow inf (ran (k \in ℝ ⟼ sup (({F ↾}_{C}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \leq inf (ran (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <))$
23	14 22	mpbird	$⊢ φ \to lim sup ({F ↾}_{C}) \leq lim sup (F)$

Metamath Proof Explorer

Theorem limsupres

Proof