Step | Hyp | Ref
| Expression |
1 | | rlim2.1 |
. . . 4
⊢ (𝜑 → ∀𝑧 ∈ 𝐴 𝐵 ∈ ℂ) |
2 | | eqid 2771 |
. . . . 5
⊢ (𝑧 ∈ 𝐴 ↦ 𝐵) = (𝑧 ∈ 𝐴 ↦ 𝐵) |
3 | 2 | fmpt 6521 |
. . . 4
⊢
(∀𝑧 ∈
𝐴 𝐵 ∈ ℂ ↔ (𝑧 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
4 | 1, 3 | sylib 208 |
. . 3
⊢ (𝜑 → (𝑧 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
5 | | rlim2.2 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
6 | | eqidd 2772 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) = ((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤)) |
7 | 4, 5, 6 | rlim 14427 |
. 2
⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑤 ∈ 𝐴 (𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥)))) |
8 | | rlim2.3 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ℂ) |
9 | 8 | biantrurd 522 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑤 ∈ 𝐴 (𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑤 ∈ 𝐴 (𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥)))) |
10 | | nfv 1995 |
. . . . . . 7
⊢
Ⅎ𝑧 𝑦 ≤ 𝑤 |
11 | | nfcv 2913 |
. . . . . . . . 9
⊢
Ⅎ𝑧abs |
12 | | nffvmpt1 6338 |
. . . . . . . . . 10
⊢
Ⅎ𝑧((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) |
13 | | nfcv 2913 |
. . . . . . . . . 10
⊢
Ⅎ𝑧
− |
14 | | nfcv 2913 |
. . . . . . . . . 10
⊢
Ⅎ𝑧𝐶 |
15 | 12, 13, 14 | nfov 6819 |
. . . . . . . . 9
⊢
Ⅎ𝑧(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶) |
16 | 11, 15 | nffv 6337 |
. . . . . . . 8
⊢
Ⅎ𝑧(abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) |
17 | | nfcv 2913 |
. . . . . . . 8
⊢
Ⅎ𝑧
< |
18 | | nfcv 2913 |
. . . . . . . 8
⊢
Ⅎ𝑧𝑥 |
19 | 16, 17, 18 | nfbr 4833 |
. . . . . . 7
⊢
Ⅎ𝑧(abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥 |
20 | 10, 19 | nfim 1977 |
. . . . . 6
⊢
Ⅎ𝑧(𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥) |
21 | | nfv 1995 |
. . . . . 6
⊢
Ⅎ𝑤(𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥) |
22 | | breq2 4790 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → (𝑦 ≤ 𝑤 ↔ 𝑦 ≤ 𝑧)) |
23 | | fveq2 6330 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → ((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) = ((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧)) |
24 | 23 | fvoveq1d 6813 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) = (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶))) |
25 | 24 | breq1d 4796 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → ((abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥 ↔ (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥)) |
26 | 22, 25 | imbi12d 333 |
. . . . . 6
⊢ (𝑤 = 𝑧 → ((𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥) ↔ (𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥))) |
27 | 20, 21, 26 | cbvral 3316 |
. . . . 5
⊢
(∀𝑤 ∈
𝐴 (𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥) ↔ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥)) |
28 | 2 | fvmpt2 6431 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → ((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) = 𝐵) |
29 | 28 | fvoveq1d 6813 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) = (abs‘(𝐵 − 𝐶))) |
30 | 29 | breq1d 4796 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → ((abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥 ↔ (abs‘(𝐵 − 𝐶)) < 𝑥)) |
31 | 30 | imbi2d 329 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → ((𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥) ↔ (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
32 | 31 | ralimiaa 3100 |
. . . . . 6
⊢
(∀𝑧 ∈
𝐴 𝐵 ∈ ℂ → ∀𝑧 ∈ 𝐴 ((𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥) ↔ (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
33 | | ralbi 3216 |
. . . . . 6
⊢
(∀𝑧 ∈
𝐴 ((𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥) ↔ (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥)) → (∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
34 | 1, 32, 33 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
35 | 27, 34 | syl5bb 272 |
. . . 4
⊢ (𝜑 → (∀𝑤 ∈ 𝐴 (𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥) ↔ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
36 | 35 | rexbidv 3200 |
. . 3
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝐴 (𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥) ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
37 | 36 | ralbidv 3135 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑤 ∈ 𝐴 (𝑦 ≤ 𝑤 → (abs‘(((𝑧 ∈ 𝐴 ↦ 𝐵)‘𝑤) − 𝐶)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |
38 | 7, 9, 37 | 3bitr2d 296 |
1
⊢ (𝜑 → ((𝑧 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 ↔ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ ℝ
∀𝑧 ∈ 𝐴 (𝑦 ≤ 𝑧 → (abs‘(𝐵 − 𝐶)) < 𝑥))) |