Theorem limsupge

Description: The defining property of the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	limsupge.b	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
	limsupge.f	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ* )
	limsupge.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
Assertion	limsupge	⊢ ( 𝜑 → ( 𝐴 ≤ ( lim sup ‘ 𝐹 ) ↔ ∀ 𝑘 ∈ ℝ 𝐴 ≤ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )

Proof

Step	Hyp	Ref	Expression
1		limsupge.b	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
2		limsupge.f	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ* )
3		limsupge.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
4		eqid	⊢ ( 𝑗 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑗 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
5	4	limsuple	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐴 ≤ ( lim sup ‘ 𝐹 ) ↔ ∀ 𝑖 ∈ ℝ 𝐴 ≤ ( ( 𝑗 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑖 ) ) )
6	1 2 3 5	syl3anc	⊢ ( 𝜑 → ( 𝐴 ≤ ( lim sup ‘ 𝐹 ) ↔ ∀ 𝑖 ∈ ℝ 𝐴 ≤ ( ( 𝑗 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑖 ) ) )
7		oveq1	⊢ ( 𝑗 = 𝑖 → ( 𝑗 [,) +∞ ) = ( 𝑖 [,) +∞ ) )
8	7	imaeq2d	⊢ ( 𝑗 = 𝑖 → ( 𝐹 “ ( 𝑗 [,) +∞ ) ) = ( 𝐹 “ ( 𝑖 [,) +∞ ) ) )
9	8	ineq1d	⊢ ( 𝑗 = 𝑖 → ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) = ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) )
10	9	supeq1d	⊢ ( 𝑗 = 𝑖 → sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → 𝑖 ∈ ℝ )
12		xrltso	⊢ < Or ℝ*
13	12	supex	⊢ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ V
14	13	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ V )
15	4 10 11 14	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → ( ( 𝑗 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑖 ) = sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
16	15	breq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → ( 𝐴 ≤ ( ( 𝑗 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑖 ) ↔ 𝐴 ≤ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
17	16	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ℝ 𝐴 ≤ ( ( 𝑗 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ℝ 𝐴 ≤ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
18	6 17	bitrd	⊢ ( 𝜑 → ( 𝐴 ≤ ( lim sup ‘ 𝐹 ) ↔ ∀ 𝑖 ∈ ℝ 𝐴 ≤ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
19		oveq1	⊢ ( 𝑖 = 𝑘 → ( 𝑖 [,) +∞ ) = ( 𝑘 [,) +∞ ) )
20	19	imaeq2d	⊢ ( 𝑖 = 𝑘 → ( 𝐹 “ ( 𝑖 [,) +∞ ) ) = ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
21	20	ineq1d	⊢ ( 𝑖 = 𝑘 → ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) = ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
22	21	supeq1d	⊢ ( 𝑖 = 𝑘 → sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
23	22	breq2d	⊢ ( 𝑖 = 𝑘 → ( 𝐴 ≤ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ↔ 𝐴 ≤ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
24	23	cbvralvw	⊢ ( ∀ 𝑖 ∈ ℝ 𝐴 ≤ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ↔ ∀ 𝑘 ∈ ℝ 𝐴 ≤ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
25	24	a1i	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ ℝ 𝐴 ≤ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ↔ ∀ 𝑘 ∈ ℝ 𝐴 ≤ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
26	18 25	bitrd	⊢ ( 𝜑 → ( 𝐴 ≤ ( lim sup ‘ 𝐹 ) ↔ ∀ 𝑘 ∈ ℝ 𝐴 ≤ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )