Step | Hyp | Ref
| Expression |
1 | | nfcv 2899 |
. . 3
⊢
Ⅎ𝑙𝐹 |
2 | | limsupre2.2 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
3 | | limsupre2.3 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) |
4 | 1, 2, 3 | limsupre2lem 42807 |
. 2
⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔
(∃𝑦 ∈ ℝ
∀𝑖 ∈ ℝ
∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑦 < (𝐹‘𝑙)) ∧ ∃𝑦 ∈ ℝ ∃𝑖 ∈ ℝ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑦)))) |
5 | | breq1 5033 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑦 < (𝐹‘𝑙) ↔ 𝑥 < (𝐹‘𝑙))) |
6 | 5 | anbi2d 632 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → ((𝑖 ≤ 𝑙 ∧ 𝑦 < (𝐹‘𝑙)) ↔ (𝑖 ≤ 𝑙 ∧ 𝑥 < (𝐹‘𝑙)))) |
7 | 6 | rexbidv 3207 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑦 < (𝐹‘𝑙)) ↔ ∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑥 < (𝐹‘𝑙)))) |
8 | 7 | ralbidv 3109 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (∀𝑖 ∈ ℝ ∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑦 < (𝐹‘𝑙)) ↔ ∀𝑖 ∈ ℝ ∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑥 < (𝐹‘𝑙)))) |
9 | | breq1 5033 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → (𝑖 ≤ 𝑙 ↔ 𝑘 ≤ 𝑙)) |
10 | 9 | anbi1d 633 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → ((𝑖 ≤ 𝑙 ∧ 𝑥 < (𝐹‘𝑙)) ↔ (𝑘 ≤ 𝑙 ∧ 𝑥 < (𝐹‘𝑙)))) |
11 | 10 | rexbidv 3207 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑥 < (𝐹‘𝑙)) ↔ ∃𝑙 ∈ 𝐴 (𝑘 ≤ 𝑙 ∧ 𝑥 < (𝐹‘𝑙)))) |
12 | | nfv 1921 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝑘 ≤ 𝑙 |
13 | | nfcv 2899 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗𝑥 |
14 | | nfcv 2899 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗
< |
15 | | limsupre2.1 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗𝐹 |
16 | | nfcv 2899 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗𝑙 |
17 | 15, 16 | nffv 6684 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗(𝐹‘𝑙) |
18 | 13, 14, 17 | nfbr 5077 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝑥 < (𝐹‘𝑙) |
19 | 12, 18 | nfan 1906 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗(𝑘 ≤ 𝑙 ∧ 𝑥 < (𝐹‘𝑙)) |
20 | | nfv 1921 |
. . . . . . . . . . 11
⊢
Ⅎ𝑙(𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)) |
21 | | breq2 5034 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑗 → (𝑘 ≤ 𝑙 ↔ 𝑘 ≤ 𝑗)) |
22 | | fveq2 6674 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑗 → (𝐹‘𝑙) = (𝐹‘𝑗)) |
23 | 22 | breq2d 5042 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑗 → (𝑥 < (𝐹‘𝑙) ↔ 𝑥 < (𝐹‘𝑗))) |
24 | 21, 23 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑗 → ((𝑘 ≤ 𝑙 ∧ 𝑥 < (𝐹‘𝑙)) ↔ (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)))) |
25 | 19, 20, 24 | cbvrexw 3341 |
. . . . . . . . . 10
⊢
(∃𝑙 ∈
𝐴 (𝑘 ≤ 𝑙 ∧ 𝑥 < (𝐹‘𝑙)) ↔ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) |
26 | 25 | a1i 11 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (∃𝑙 ∈ 𝐴 (𝑘 ≤ 𝑙 ∧ 𝑥 < (𝐹‘𝑙)) ↔ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)))) |
27 | 11, 26 | bitrd 282 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → (∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑥 < (𝐹‘𝑙)) ↔ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)))) |
28 | 27 | cbvralvw 3349 |
. . . . . . 7
⊢
(∀𝑖 ∈
ℝ ∃𝑙 ∈
𝐴 (𝑖 ≤ 𝑙 ∧ 𝑥 < (𝐹‘𝑙)) ↔ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) |
29 | 28 | a1i 11 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (∀𝑖 ∈ ℝ ∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑥 < (𝐹‘𝑙)) ↔ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)))) |
30 | 8, 29 | bitrd 282 |
. . . . 5
⊢ (𝑦 = 𝑥 → (∀𝑖 ∈ ℝ ∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑦 < (𝐹‘𝑙)) ↔ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)))) |
31 | 30 | cbvrexvw 3350 |
. . . 4
⊢
(∃𝑦 ∈
ℝ ∀𝑖 ∈
ℝ ∃𝑙 ∈
𝐴 (𝑖 ≤ 𝑙 ∧ 𝑦 < (𝐹‘𝑙)) ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) |
32 | 31 | a1i 11 |
. . 3
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑖 ∈ ℝ ∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑦 < (𝐹‘𝑙)) ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)))) |
33 | | breq2 5034 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝐹‘𝑙) < 𝑦 ↔ (𝐹‘𝑙) < 𝑥)) |
34 | 33 | imbi2d 344 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → ((𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑦) ↔ (𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑥))) |
35 | 34 | ralbidv 3109 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑦) ↔ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑥))) |
36 | 35 | rexbidv 3207 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ ℝ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑦) ↔ ∃𝑖 ∈ ℝ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑥))) |
37 | 9 | imbi1d 345 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → ((𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑥) ↔ (𝑘 ≤ 𝑙 → (𝐹‘𝑙) < 𝑥))) |
38 | 37 | ralbidv 3109 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑥) ↔ ∀𝑙 ∈ 𝐴 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) < 𝑥))) |
39 | 17, 14, 13 | nfbr 5077 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗(𝐹‘𝑙) < 𝑥 |
40 | 12, 39 | nfim 1903 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗(𝑘 ≤ 𝑙 → (𝐹‘𝑙) < 𝑥) |
41 | | nfv 1921 |
. . . . . . . . . . 11
⊢
Ⅎ𝑙(𝑘 ≤ 𝑗 → (𝐹‘𝑗) < 𝑥) |
42 | 22 | breq1d 5040 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑗 → ((𝐹‘𝑙) < 𝑥 ↔ (𝐹‘𝑗) < 𝑥)) |
43 | 21, 42 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑗 → ((𝑘 ≤ 𝑙 → (𝐹‘𝑙) < 𝑥) ↔ (𝑘 ≤ 𝑗 → (𝐹‘𝑗) < 𝑥))) |
44 | 40, 41, 43 | cbvralw 3340 |
. . . . . . . . . 10
⊢
(∀𝑙 ∈
𝐴 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) < 𝑥) ↔ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) < 𝑥)) |
45 | 44 | a1i 11 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (∀𝑙 ∈ 𝐴 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) < 𝑥) ↔ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) < 𝑥))) |
46 | 38, 45 | bitrd 282 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → (∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑥) ↔ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) < 𝑥))) |
47 | 46 | cbvrexvw 3350 |
. . . . . . 7
⊢
(∃𝑖 ∈
ℝ ∀𝑙 ∈
𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑥) ↔ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) < 𝑥)) |
48 | 47 | a1i 11 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ ℝ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑥) ↔ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) < 𝑥))) |
49 | 36, 48 | bitrd 282 |
. . . . 5
⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ ℝ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑦) ↔ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) < 𝑥))) |
50 | 49 | cbvrexvw 3350 |
. . . 4
⊢
(∃𝑦 ∈
ℝ ∃𝑖 ∈
ℝ ∀𝑙 ∈
𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑦) ↔ ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) < 𝑥)) |
51 | 50 | a1i 11 |
. . 3
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∃𝑖 ∈ ℝ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑦) ↔ ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) < 𝑥))) |
52 | 32, 51 | anbi12d 634 |
. 2
⊢ (𝜑 → ((∃𝑦 ∈ ℝ ∀𝑖 ∈ ℝ ∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑦 < (𝐹‘𝑙)) ∧ ∃𝑦 ∈ ℝ ∃𝑖 ∈ ℝ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) < 𝑦)) ↔ (∃𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)) ∧ ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) < 𝑥)))) |
53 | 4, 52 | bitrd 282 |
1
⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔
(∃𝑥 ∈ ℝ
∀𝑘 ∈ ℝ
∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)) ∧ ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) < 𝑥)))) |