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