Step | Hyp | Ref
| Expression |
1 | | nfcv 2904 |
. . 3
⊢
Ⅎ𝑙𝐹 |
2 | | limsupre3.2 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
3 | | limsupre3.3 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) |
4 | 1, 2, 3 | limsupre3lem 42948 |
. 2
⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔
(∃𝑦 ∈ ℝ
∀𝑖 ∈ ℝ
∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑦 ≤ (𝐹‘𝑙)) ∧ ∃𝑦 ∈ ℝ ∃𝑖 ∈ ℝ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦)))) |
5 | | breq1 5056 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑦 ≤ (𝐹‘𝑙) ↔ 𝑥 ≤ (𝐹‘𝑙))) |
6 | 5 | anbi2d 632 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → ((𝑖 ≤ 𝑙 ∧ 𝑦 ≤ (𝐹‘𝑙)) ↔ (𝑖 ≤ 𝑙 ∧ 𝑥 ≤ (𝐹‘𝑙)))) |
7 | 6 | rexbidv 3216 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑦 ≤ (𝐹‘𝑙)) ↔ ∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑥 ≤ (𝐹‘𝑙)))) |
8 | 7 | ralbidv 3118 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (∀𝑖 ∈ ℝ ∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑦 ≤ (𝐹‘𝑙)) ↔ ∀𝑖 ∈ ℝ ∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑥 ≤ (𝐹‘𝑙)))) |
9 | | breq1 5056 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → (𝑖 ≤ 𝑙 ↔ 𝑘 ≤ 𝑙)) |
10 | 9 | anbi1d 633 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → ((𝑖 ≤ 𝑙 ∧ 𝑥 ≤ (𝐹‘𝑙)) ↔ (𝑘 ≤ 𝑙 ∧ 𝑥 ≤ (𝐹‘𝑙)))) |
11 | 10 | rexbidv 3216 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑥 ≤ (𝐹‘𝑙)) ↔ ∃𝑙 ∈ 𝐴 (𝑘 ≤ 𝑙 ∧ 𝑥 ≤ (𝐹‘𝑙)))) |
12 | | nfv 1922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝑘 ≤ 𝑙 |
13 | | nfcv 2904 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗𝑥 |
14 | | nfcv 2904 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗
≤ |
15 | | limsupre3.1 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗𝐹 |
16 | | nfcv 2904 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗𝑙 |
17 | 15, 16 | nffv 6727 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗(𝐹‘𝑙) |
18 | 13, 14, 17 | nfbr 5100 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝑥 ≤ (𝐹‘𝑙) |
19 | 12, 18 | nfan 1907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗(𝑘 ≤ 𝑙 ∧ 𝑥 ≤ (𝐹‘𝑙)) |
20 | | nfv 1922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑙(𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)) |
21 | | breq2 5057 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑗 → (𝑘 ≤ 𝑙 ↔ 𝑘 ≤ 𝑗)) |
22 | | fveq2 6717 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑗 → (𝐹‘𝑙) = (𝐹‘𝑗)) |
23 | 22 | breq2d 5065 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑗 → (𝑥 ≤ (𝐹‘𝑙) ↔ 𝑥 ≤ (𝐹‘𝑗))) |
24 | 21, 23 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑗 → ((𝑘 ≤ 𝑙 ∧ 𝑥 ≤ (𝐹‘𝑙)) ↔ (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)))) |
25 | 19, 20, 24 | cbvrexw 3350 |
. . . . . . . . . 10
⊢
(∃𝑙 ∈
𝐴 (𝑘 ≤ 𝑙 ∧ 𝑥 ≤ (𝐹‘𝑙)) ↔ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) |
26 | 25 | a1i 11 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (∃𝑙 ∈ 𝐴 (𝑘 ≤ 𝑙 ∧ 𝑥 ≤ (𝐹‘𝑙)) ↔ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)))) |
27 | 11, 26 | bitrd 282 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → (∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑥 ≤ (𝐹‘𝑙)) ↔ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)))) |
28 | 27 | cbvralvw 3358 |
. . . . . . 7
⊢
(∀𝑖 ∈
ℝ ∃𝑙 ∈
𝐴 (𝑖 ≤ 𝑙 ∧ 𝑥 ≤ (𝐹‘𝑙)) ↔ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) |
29 | 28 | a1i 11 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (∀𝑖 ∈ ℝ ∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑥 ≤ (𝐹‘𝑙)) ↔ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)))) |
30 | 8, 29 | bitrd 282 |
. . . . 5
⊢ (𝑦 = 𝑥 → (∀𝑖 ∈ ℝ ∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑦 ≤ (𝐹‘𝑙)) ↔ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)))) |
31 | 30 | cbvrexvw 3359 |
. . . 4
⊢
(∃𝑦 ∈
ℝ ∀𝑖 ∈
ℝ ∃𝑙 ∈
𝐴 (𝑖 ≤ 𝑙 ∧ 𝑦 ≤ (𝐹‘𝑙)) ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) |
32 | | breq2 5057 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((𝐹‘𝑙) ≤ 𝑦 ↔ (𝐹‘𝑙) ≤ 𝑥)) |
33 | 32 | imbi2d 344 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → ((𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦) ↔ (𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑥))) |
34 | 33 | ralbidv 3118 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦) ↔ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑥))) |
35 | 34 | rexbidv 3216 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ ℝ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦) ↔ ∃𝑖 ∈ ℝ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑥))) |
36 | 9 | imbi1d 345 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → ((𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑥) ↔ (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑥))) |
37 | 36 | ralbidv 3118 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑥) ↔ ∀𝑙 ∈ 𝐴 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑥))) |
38 | 17, 14, 13 | nfbr 5100 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗(𝐹‘𝑙) ≤ 𝑥 |
39 | 12, 38 | nfim 1904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗(𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑥) |
40 | | nfv 1922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑙(𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) |
41 | 22 | breq1d 5063 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑗 → ((𝐹‘𝑙) ≤ 𝑥 ↔ (𝐹‘𝑗) ≤ 𝑥)) |
42 | 21, 41 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑙 = 𝑗 → ((𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑥) ↔ (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) |
43 | 39, 40, 42 | cbvralw 3349 |
. . . . . . . . . 10
⊢
(∀𝑙 ∈
𝐴 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑥) ↔ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) |
44 | 43 | a1i 11 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (∀𝑙 ∈ 𝐴 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑥) ↔ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) |
45 | 37, 44 | bitrd 282 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → (∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑥) ↔ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) |
46 | 45 | cbvrexvw 3359 |
. . . . . . 7
⊢
(∃𝑖 ∈
ℝ ∀𝑙 ∈
𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑥) ↔ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) |
47 | 46 | a1i 11 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ ℝ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑥) ↔ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) |
48 | 35, 47 | bitrd 282 |
. . . . 5
⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ ℝ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦) ↔ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) |
49 | 48 | cbvrexvw 3359 |
. . . 4
⊢
(∃𝑦 ∈
ℝ ∃𝑖 ∈
ℝ ∀𝑙 ∈
𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦) ↔ ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) |
50 | 31, 49 | anbi12i 630 |
. . 3
⊢
((∃𝑦 ∈
ℝ ∀𝑖 ∈
ℝ ∃𝑙 ∈
𝐴 (𝑖 ≤ 𝑙 ∧ 𝑦 ≤ (𝐹‘𝑙)) ∧ ∃𝑦 ∈ ℝ ∃𝑖 ∈ ℝ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦)) ↔ (∃𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)) ∧ ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥))) |
51 | 50 | a1i 11 |
. 2
⊢ (𝜑 → ((∃𝑦 ∈ ℝ ∀𝑖 ∈ ℝ ∃𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 ∧ 𝑦 ≤ (𝐹‘𝑙)) ∧ ∃𝑦 ∈ ℝ ∃𝑖 ∈ ℝ ∀𝑙 ∈ 𝐴 (𝑖 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦)) ↔ (∃𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)) ∧ ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)))) |
52 | 4, 51 | bitrd 282 |
1
⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔
(∃𝑥 ∈ ℝ
∀𝑘 ∈ ℝ
∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)) ∧ ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)))) |