Theorem 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	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
Assertion	limsupres	⊢ ( 𝜑 → ( lim sup ‘ ( 𝐹 ↾ 𝐶 ) ) ≤ ( lim sup ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		limsupres.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		nfv	⊢ Ⅎ 𝑘 𝜑
3		resimass	⊢ ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑘 [,) +∞ ) ) ⊆ ( 𝐹 “ ( 𝑘 [,) +∞ ) )
4	3	a1i	⊢ ( 𝑘 ∈ ℝ → ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑘 [,) +∞ ) ) ⊆ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
5	4	ssrind	⊢ ( 𝑘 ∈ ℝ → ( ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
6	5	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
7		inss2	⊢ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ*
8	7	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* )
9	6 8	sstrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → ( ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* )
10	9	supxrcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → sup ( ( ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
11	8	supxrcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ* )
12		supxrss	⊢ ( ( ( ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ∧ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* ) → sup ( ( ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
13	6 8 12	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → sup ( ( ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
14	2 10 11 13	infrnmptle	⊢ ( 𝜑 → inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) ≤ inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
15	1	resexd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) ∈ V )
16		eqid	⊢ ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
17	16	limsupval	⊢ ( ( 𝐹 ↾ 𝐶 ) ∈ V → ( lim sup ‘ ( 𝐹 ↾ 𝐶 ) ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
18	15 17	syl	⊢ ( 𝜑 → ( lim sup ‘ ( 𝐹 ↾ 𝐶 ) ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
19		eqid	⊢ ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
20	19	limsupval	⊢ ( 𝐹 ∈ 𝑉 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
21	1 20	syl	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
22	18 21	breq12d	⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝐹 ↾ 𝐶 ) ) ≤ ( lim sup ‘ 𝐹 ) ↔ inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) ≤ inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) ) )
23	14 22	mpbird	⊢ ( 𝜑 → ( lim sup ‘ ( 𝐹 ↾ 𝐶 ) ) ≤ ( lim sup ‘ 𝐹 ) )