Metamath Proof Explorer


Theorem 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 ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) < 𝐴 ) )