limsuplt2

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

	Ref	Expression
Hypotheses	limsuplt2.1	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
	limsuplt2.2	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ^* )
	limsuplt2.3	⊢ ( 𝜑 → 𝐴 ∈ ℝ^* )
Assertion	limsuplt2	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) < 𝐴 ↔ ∃ 𝑘 ∈ ℝ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) < 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		limsuplt2.1	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
2		limsuplt2.2	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ^* )
3		limsuplt2.3	⊢ ( 𝜑 → 𝐴 ∈ ℝ^* )
4		eqid	⊢ ( 𝑗 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ( 𝑗 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
5	4	limsuplt	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ^* ∧ 𝐴 ∈ ℝ^* ) → ( ( 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	breq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℝ ) → ( ( ( 𝑗 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) ‘ 𝑖 ) < 𝐴 ↔ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) < 𝐴 ) )
17	16	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ℝ ( ( 𝑗 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑗 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) ‘ 𝑖 ) < 𝐴 ↔ ∃ 𝑖 ∈ ℝ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) < 𝐴 ) )
18		oveq1	⊢ ( 𝑖 = 𝑘 → ( 𝑖 [,) +∞ ) = ( 𝑘 [,) +∞ ) )
19	18	imaeq2d	⊢ ( 𝑖 = 𝑘 → ( 𝐹 “ ( 𝑖 [,) +∞ ) ) = ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
20	19	ineq1d	⊢ ( 𝑖 = 𝑘 → ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ^* ) = ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) )
21	20	supeq1d	⊢ ( 𝑖 = 𝑘 → sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) = sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
22	21	breq1d	⊢ ( 𝑖 = 𝑘 → ( sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) < 𝐴 ↔ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) < 𝐴 ) )
23	22	cbvrexvw	⊢ ( ∃ 𝑖 ∈ ℝ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) < 𝐴 ↔ ∃ 𝑘 ∈ ℝ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) < 𝐴 )
24	23	a1i	⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ℝ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) < 𝐴 ↔ ∃ 𝑘 ∈ ℝ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) < 𝐴 ) )
25	6 17 24	3bitrd	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) < 𝐴 ↔ ∃ 𝑘 ∈ ℝ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) < 𝐴 ) )

Metamath Proof Explorer

Theorem limsuplt2

Proof