Step |
Hyp |
Ref |
Expression |
1 |
|
limsupmnf.j |
⊢ Ⅎ 𝑗 𝐹 |
2 |
|
limsupmnf.a |
⊢ ( 𝜑 → 𝐴 ⊆ ℝ ) |
3 |
|
limsupmnf.f |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* ) |
4 |
|
eqid |
⊢ ( 𝑖 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) , ℝ* , < ) ) = ( 𝑖 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) , ℝ* , < ) ) |
5 |
2 3 4
|
limsupmnflem |
⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) ) |
6 |
|
breq2 |
⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) |
7 |
6
|
imbi2d |
⊢ ( 𝑦 = 𝑥 → ( ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) ) |
8 |
7
|
ralbidv |
⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) ) |
9 |
8
|
rexbidv |
⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) ) |
10 |
|
breq1 |
⊢ ( 𝑖 = 𝑘 → ( 𝑖 ≤ 𝑙 ↔ 𝑘 ≤ 𝑙 ) ) |
11 |
10
|
imbi1d |
⊢ ( 𝑖 = 𝑘 → ( ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) ) |
12 |
11
|
ralbidv |
⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) ) |
13 |
|
nfv |
⊢ Ⅎ 𝑗 𝑘 ≤ 𝑙 |
14 |
|
nfcv |
⊢ Ⅎ 𝑗 𝑙 |
15 |
1 14
|
nffv |
⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) |
16 |
|
nfcv |
⊢ Ⅎ 𝑗 ≤ |
17 |
|
nfcv |
⊢ Ⅎ 𝑗 𝑥 |
18 |
15 16 17
|
nfbr |
⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 |
19 |
13 18
|
nfim |
⊢ Ⅎ 𝑗 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) |
20 |
|
nfv |
⊢ Ⅎ 𝑙 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) |
21 |
|
breq2 |
⊢ ( 𝑙 = 𝑗 → ( 𝑘 ≤ 𝑙 ↔ 𝑘 ≤ 𝑗 ) ) |
22 |
|
fveq2 |
⊢ ( 𝑙 = 𝑗 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑗 ) ) |
23 |
22
|
breq1d |
⊢ ( 𝑙 = 𝑗 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) |
24 |
21 23
|
imbi12d |
⊢ ( 𝑙 = 𝑗 → ( ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ) |
25 |
19 20 24
|
cbvralw |
⊢ ( ∀ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) |
26 |
25
|
a1i |
⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ) |
27 |
12 26
|
bitrd |
⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ) |
28 |
27
|
cbvrexvw |
⊢ ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) |
29 |
28
|
a1i |
⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ) |
30 |
9 29
|
bitrd |
⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ) |
31 |
30
|
cbvralvw |
⊢ ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) |
32 |
31
|
a1i |
⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ) |
33 |
5 32
|
bitrd |
⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ) |