Theorem limsupbnd1f

Description: If a sequence is eventually at most A , then the limsup is also at most A . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupbnd1f.1	⊢ Ⅎ 𝑗 𝐹
	limsupbnd1f.2	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
	limsupbnd1f.3	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ* )
	limsupbnd1f.4	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	limsupbnd1f.5	⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) )
Assertion	limsupbnd1f	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≤ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		limsupbnd1f.1	⊢ Ⅎ 𝑗 𝐹
2		limsupbnd1f.2	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
3		limsupbnd1f.3	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ* )
4		limsupbnd1f.4	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
5		limsupbnd1f.5	⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) )
6		breq1	⊢ ( 𝑘 = 𝑖 → ( 𝑘 ≤ 𝑗 ↔ 𝑖 ≤ 𝑗 ) )
7	6	imbi1d	⊢ ( 𝑘 = 𝑖 → ( ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ) )
8	7	ralbidv	⊢ ( 𝑘 = 𝑖 → ( ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ∀ 𝑗 ∈ 𝐵 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ) )
9		nfv	⊢ Ⅎ 𝑙 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 )
10		nfv	⊢ Ⅎ 𝑗 𝑖 ≤ 𝑙
11		nfcv	⊢ Ⅎ 𝑗 𝑙
12	1 11	nffv	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
13		nfcv	⊢ Ⅎ 𝑗 ≤
14		nfcv	⊢ Ⅎ 𝑗 𝐴
15	12 13 14	nfbr	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) ≤ 𝐴
16	10 15	nfim	⊢ Ⅎ 𝑗 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 )
17		breq2	⊢ ( 𝑗 = 𝑙 → ( 𝑖 ≤ 𝑗 ↔ 𝑖 ≤ 𝑙 ) )
18		fveq2	⊢ ( 𝑗 = 𝑙 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑙 ) )
19	18	breq1d	⊢ ( 𝑗 = 𝑙 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ↔ ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 ) )
20	17 19	imbi12d	⊢ ( 𝑗 = 𝑙 → ( ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 ) ) )
21	9 16 20	cbvralw	⊢ ( ∀ 𝑗 ∈ 𝐵 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ∀ 𝑙 ∈ 𝐵 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 ) )
22	21	a1i	⊢ ( 𝑘 = 𝑖 → ( ∀ 𝑗 ∈ 𝐵 ( 𝑖 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ∀ 𝑙 ∈ 𝐵 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 ) ) )
23	8 22	bitrd	⊢ ( 𝑘 = 𝑖 → ( ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ∀ 𝑙 ∈ 𝐵 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 ) ) )
24	23	cbvrexvw	⊢ ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐵 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐵 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 ) )
25	5 24	sylib	⊢ ( 𝜑 → ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐵 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝐴 ) )
26	2 3 4 25	limsupbnd1	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≤ 𝐴 )