Step |
Hyp |
Ref |
Expression |
1 |
|
limsupre2mpt.p |
⊢ Ⅎ 𝑥 𝜑 |
2 |
|
limsupre2mpt.a |
⊢ ( 𝜑 → 𝐴 ⊆ ℝ ) |
3 |
|
limsupre2mpt.b |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* ) |
4 |
|
nfmpt1 |
⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
5 |
1 3
|
fmptd2f |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ* ) |
6 |
4 2 5
|
limsupre2 |
⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ↔ ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑤 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∧ ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑤 ) ) ) ) |
7 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
8 |
7
|
a1i |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) |
9 |
8 3
|
fvmpt2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 ) |
10 |
9
|
breq2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑤 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ 𝑤 < 𝐵 ) ) |
11 |
10
|
anbi2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑗 ≤ 𝑥 ∧ 𝑤 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ↔ ( 𝑗 ≤ 𝑥 ∧ 𝑤 < 𝐵 ) ) ) |
12 |
1 11
|
rexbida |
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑤 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑤 < 𝐵 ) ) ) |
13 |
12
|
ralbidv |
⊢ ( 𝜑 → ( ∀ 𝑗 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑤 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ↔ ∀ 𝑗 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑤 < 𝐵 ) ) ) |
14 |
13
|
rexbidv |
⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑤 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑤 < 𝐵 ) ) ) |
15 |
9
|
breq1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑤 ↔ 𝐵 < 𝑤 ) ) |
16 |
15
|
imbi2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑗 ≤ 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑤 ) ↔ ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑤 ) ) ) |
17 |
1 16
|
ralbida |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑤 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑤 ) ) ) |
18 |
17
|
rexbidv |
⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑤 ) ↔ ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑤 ) ) ) |
19 |
18
|
rexbidv |
⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑤 ) ↔ ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑤 ) ) ) |
20 |
14 19
|
anbi12d |
⊢ ( 𝜑 → ( ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑤 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ) ∧ ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑤 ) ) ↔ ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑤 < 𝐵 ) ∧ ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑤 ) ) ) ) |
21 |
|
breq1 |
⊢ ( 𝑤 = 𝑦 → ( 𝑤 < 𝐵 ↔ 𝑦 < 𝐵 ) ) |
22 |
21
|
anbi2d |
⊢ ( 𝑤 = 𝑦 → ( ( 𝑗 ≤ 𝑥 ∧ 𝑤 < 𝐵 ) ↔ ( 𝑗 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ) ) |
23 |
22
|
rexbidv |
⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑤 < 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ) ) |
24 |
23
|
ralbidv |
⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑗 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑤 < 𝐵 ) ↔ ∀ 𝑗 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ) ) |
25 |
|
breq1 |
⊢ ( 𝑗 = 𝑘 → ( 𝑗 ≤ 𝑥 ↔ 𝑘 ≤ 𝑥 ) ) |
26 |
25
|
anbi1d |
⊢ ( 𝑗 = 𝑘 → ( ( 𝑗 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ↔ ( 𝑘 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ) ) |
27 |
26
|
rexbidv |
⊢ ( 𝑗 = 𝑘 → ( ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ) ) |
28 |
27
|
cbvralvw |
⊢ ( ∀ 𝑗 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ) |
29 |
28
|
a1i |
⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑗 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ) ) |
30 |
24 29
|
bitrd |
⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑗 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑤 < 𝐵 ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ) ) |
31 |
30
|
cbvrexvw |
⊢ ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑤 < 𝐵 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ) |
32 |
|
breq2 |
⊢ ( 𝑤 = 𝑦 → ( 𝐵 < 𝑤 ↔ 𝐵 < 𝑦 ) ) |
33 |
32
|
imbi2d |
⊢ ( 𝑤 = 𝑦 → ( ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑤 ) ↔ ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑦 ) ) ) |
34 |
33
|
ralbidv |
⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑤 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑦 ) ) ) |
35 |
34
|
rexbidv |
⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑤 ) ↔ ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑦 ) ) ) |
36 |
25
|
imbi1d |
⊢ ( 𝑗 = 𝑘 → ( ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑦 ) ↔ ( 𝑘 ≤ 𝑥 → 𝐵 < 𝑦 ) ) ) |
37 |
36
|
ralbidv |
⊢ ( 𝑗 = 𝑘 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 → 𝐵 < 𝑦 ) ) ) |
38 |
37
|
cbvrexvw |
⊢ ( ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑦 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 → 𝐵 < 𝑦 ) ) |
39 |
38
|
a1i |
⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑦 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 → 𝐵 < 𝑦 ) ) ) |
40 |
35 39
|
bitrd |
⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑤 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 → 𝐵 < 𝑦 ) ) ) |
41 |
40
|
cbvrexvw |
⊢ ( ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑤 ) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 → 𝐵 < 𝑦 ) ) |
42 |
31 41
|
anbi12i |
⊢ ( ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑤 < 𝐵 ) ∧ ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑤 ) ) ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 → 𝐵 < 𝑦 ) ) ) |
43 |
42
|
a1i |
⊢ ( 𝜑 → ( ( ∃ 𝑤 ∈ ℝ ∀ 𝑗 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 ∧ 𝑤 < 𝐵 ) ∧ ∃ 𝑤 ∈ ℝ ∃ 𝑗 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑗 ≤ 𝑥 → 𝐵 < 𝑤 ) ) ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 → 𝐵 < 𝑦 ) ) ) ) |
44 |
6 20 43
|
3bitrd |
⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 ∧ 𝑦 < 𝐵 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑘 ≤ 𝑥 → 𝐵 < 𝑦 ) ) ) ) |