Theorem limsupubuzmpt

Description: If the limsup is not +oo , then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupubuzmpt.j	⊢ Ⅎ 𝑗 𝜑
	limsupubuzmpt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	limsupubuzmpt.b	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
	limsupubuzmpt.n	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) ≠ +∞ )
Assertion	limsupubuzmpt	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		limsupubuzmpt.j	⊢ Ⅎ 𝑗 𝜑
2		limsupubuzmpt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		limsupubuzmpt.b	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
4		limsupubuzmpt.n	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) ≠ +∞ )
5		nfmpt1	⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝑍 ↦ 𝐵 )
6		eqid	⊢ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑗 ∈ 𝑍 ↦ 𝐵 )
7	1 3 6	fmptdf	⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ )
8	5 2 7 4	limsupubuz	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ≤ 𝑦 )
9	6	a1i	⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) )
10	9 3	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) = 𝐵 )
11	10	breq1d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ≤ 𝑦 ↔ 𝐵 ≤ 𝑦 ) )
12	1 11	ralbida	⊢ ( 𝜑 → ( ∀ 𝑗 ∈ 𝑍 ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ≤ 𝑦 ↔ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑦 ) )
13	12	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑦 ) )
14	8 13	mpbid	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑦 )
15		breq2	⊢ ( 𝑦 = 𝑥 → ( 𝐵 ≤ 𝑦 ↔ 𝐵 ≤ 𝑥 ) )
16	15	ralbidv	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑦 ↔ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 ) )
17	16	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 )
18	14 17	sylib	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 )