Step |
Hyp |
Ref |
Expression |
1 |
|
limsuppnfd.j |
⊢ Ⅎ 𝑗 𝐹 |
2 |
|
limsuppnfd.a |
⊢ ( 𝜑 → 𝐴 ⊆ ℝ ) |
3 |
|
limsuppnfd.f |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* ) |
4 |
|
limsuppnfd.u |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) |
5 |
|
breq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) |
6 |
5
|
anbi2d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) |
7 |
6
|
rexbidv |
⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) |
8 |
|
breq1 |
⊢ ( 𝑘 = 𝑖 → ( 𝑘 ≤ 𝑗 ↔ 𝑖 ≤ 𝑗 ) ) |
9 |
8
|
anbi1d |
⊢ ( 𝑘 = 𝑖 → ( ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ( 𝑖 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) |
10 |
9
|
rexbidv |
⊢ ( 𝑘 = 𝑖 → ( ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑗 ∈ 𝐴 ( 𝑖 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) |
11 |
|
nfv |
⊢ Ⅎ 𝑙 ( 𝑖 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) |
12 |
|
nfv |
⊢ Ⅎ 𝑗 𝑖 ≤ 𝑙 |
13 |
|
nfcv |
⊢ Ⅎ 𝑗 𝑦 |
14 |
|
nfcv |
⊢ Ⅎ 𝑗 ≤ |
15 |
|
nfcv |
⊢ Ⅎ 𝑗 𝑙 |
16 |
1 15
|
nffv |
⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) |
17 |
13 14 16
|
nfbr |
⊢ Ⅎ 𝑗 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) |
18 |
12 17
|
nfan |
⊢ Ⅎ 𝑗 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) |
19 |
|
breq2 |
⊢ ( 𝑗 = 𝑙 → ( 𝑖 ≤ 𝑗 ↔ 𝑖 ≤ 𝑙 ) ) |
20 |
|
fveq2 |
⊢ ( 𝑗 = 𝑙 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑙 ) ) |
21 |
20
|
breq2d |
⊢ ( 𝑗 = 𝑙 → ( 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ↔ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ) |
22 |
19 21
|
anbi12d |
⊢ ( 𝑗 = 𝑙 → ( ( 𝑖 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ) ) |
23 |
11 18 22
|
cbvrexw |
⊢ ( ∃ 𝑗 ∈ 𝐴 ( 𝑖 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ) |
24 |
23
|
a1i |
⊢ ( 𝑘 = 𝑖 → ( ∃ 𝑗 ∈ 𝐴 ( 𝑖 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ) ) |
25 |
10 24
|
bitrd |
⊢ ( 𝑘 = 𝑖 → ( ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ) ) |
26 |
7 25
|
cbvral2vw |
⊢ ( ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ↔ ∀ 𝑦 ∈ ℝ ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ) |
27 |
4 26
|
sylib |
⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ) |
28 |
|
eqid |
⊢ ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑖 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑖 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) |
29 |
2 3 27 28
|
limsuppnfdlem |
⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = +∞ ) |