Step | Hyp | Ref
| Expression |
1 | | ellimc3.f |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
2 | | ellimc3.a |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
3 | | ellimc3.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℂ) |
4 | | eqid 2738 |
. . 3
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
5 | 1, 2, 3, 4 | ellimc2 24629 |
. 2
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))) |
6 | | cnxmet 23526 |
. . . . . . . . 9
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
7 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈
ℂ) |
8 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
9 | | blcntr 23167 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) |
10 | 6, 7, 8, 9 | mp3an2i 1467 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) |
11 | | rpxr 12482 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ*) |
12 | 11 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ*) |
13 | 4 | cnfldtopn 23535 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
14 | 13 | blopn 23254 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ*) → (𝐶(ball‘(abs ∘ −
))𝑥) ∈
(TopOpen‘ℂfld)) |
15 | 6, 7, 12, 14 | mp3an2i 1467 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (𝐶(ball‘(abs ∘ −
))𝑥) ∈
(TopOpen‘ℂfld)) |
16 | | eleq2 2821 |
. . . . . . . . . . 11
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐶 ∈ 𝑢 ↔ 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) |
17 | | sseq2 3904 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢 ↔ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
18 | 17 | anbi2d 632 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ (𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
19 | 18 | rexbidv 3207 |
. . . . . . . . . . 11
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → (∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
20 | 16, 19 | imbi12d 348 |
. . . . . . . . . 10
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ (𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))) |
21 | 20 | rspcv 3522 |
. . . . . . . . 9
⊢ ((𝐶(ball‘(abs ∘ −
))𝑥) ∈
(TopOpen‘ℂfld) → (∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → (𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))) |
22 | 15, 21 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) →
(∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → (𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))) |
23 | 10, 22 | mpid 44 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) →
(∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
24 | 13 | mopni2 23247 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐵 ∈ 𝑣) → ∃𝑦 ∈ ℝ+
(𝐵(ball‘(abs ∘
− ))𝑦) ⊆ 𝑣) |
25 | 6, 24 | mp3an1 1449 |
. . . . . . . . . 10
⊢ ((𝑣 ∈
(TopOpen‘ℂfld) ∧ 𝐵 ∈ 𝑣) → ∃𝑦 ∈ ℝ+ (𝐵(ball‘(abs ∘ −
))𝑦) ⊆ 𝑣) |
26 | | ssrin 4125 |
. . . . . . . . . . . . 13
⊢ ((𝐵(ball‘(abs ∘ −
))𝑦) ⊆ 𝑣 → ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑣 ∩ (𝐴 ∖ {𝐵}))) |
27 | | imass2 5940 |
. . . . . . . . . . . . 13
⊢ (((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑣 ∩ (𝐴 ∖ {𝐵})) → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵})))) |
28 | | sstr2 3885 |
. . . . . . . . . . . . 13
⊢ ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
29 | 26, 27, 28 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝐵(ball‘(abs ∘ −
))𝑦) ⊆ 𝑣 → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
30 | 29 | com12 32 |
. . . . . . . . . . 11
⊢ ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐵(ball‘(abs ∘ − ))𝑦) ⊆ 𝑣 → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
31 | 30 | reximdv 3183 |
. . . . . . . . . 10
⊢ ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (∃𝑦 ∈ ℝ+
(𝐵(ball‘(abs ∘
− ))𝑦) ⊆ 𝑣 → ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
32 | 25, 31 | syl5com 31 |
. . . . . . . . 9
⊢ ((𝑣 ∈
(TopOpen‘ℂfld) ∧ 𝐵 ∈ 𝑣) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
33 | 32 | impr 458 |
. . . . . . . 8
⊢ ((𝑣 ∈
(TopOpen‘ℂfld) ∧ (𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) → ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) |
34 | 33 | rexlimiva 3191 |
. . . . . . 7
⊢
(∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) |
35 | 23, 34 | syl6 35 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) →
(∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
36 | 35 | ralrimdva 3101 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
37 | 13 | mopni2 23247 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝐶 ∈ 𝑢) → ∃𝑥 ∈ ℝ+
(𝐶(ball‘(abs ∘
− ))𝑥) ⊆ 𝑢) |
38 | 6, 37 | mp3an1 1449 |
. . . . . . . . 9
⊢ ((𝑢 ∈
(TopOpen‘ℂfld) ∧ 𝐶 ∈ 𝑢) → ∃𝑥 ∈ ℝ+ (𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢) |
39 | | r19.29r 3168 |
. . . . . . . . . . 11
⊢
((∃𝑥 ∈
ℝ+ (𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑥 ∈ ℝ+
((𝐶(ball‘(abs ∘
− ))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
40 | 3 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝐵 ∈
ℂ) |
41 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝑦 ∈
ℝ+) |
42 | 41 | rpxrd 12516 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝑦 ∈
ℝ*) |
43 | 13 | blopn 23254 |
. . . . . . . . . . . . . . . . 17
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ*) → (𝐵(ball‘(abs ∘ −
))𝑦) ∈
(TopOpen‘ℂfld)) |
44 | 6, 40, 42, 43 | mp3an2i 1467 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ (𝐵(ball‘(abs
∘ − ))𝑦) ∈
(TopOpen‘ℂfld)) |
45 | | blcntr 23167 |
. . . . . . . . . . . . . . . . 17
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ+) → 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) |
46 | 6, 40, 41, 45 | mp3an2i 1467 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝐵 ∈ (𝐵(ball‘(abs ∘ −
))𝑦)) |
47 | | eleq2 2821 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐵 ∈ 𝑣 ↔ 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) |
48 | | ineq1 4097 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝑣 ∩ (𝐴 ∖ {𝐵})) = ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) |
49 | 48 | imaeq2d 5904 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) = (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})))) |
50 | 49 | sseq1d 3909 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
51 | 47, 50 | anbi12d 634 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → ((𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ (𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
52 | 51 | rspcev 3527 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵(ball‘(abs ∘ −
))𝑦) ∈
(TopOpen‘ℂfld) ∧ (𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
53 | 52 | expr 460 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵(ball‘(abs ∘ −
))𝑦) ∈
(TopOpen‘ℂfld) ∧ 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
54 | 44, 46, 53 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ ((𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
55 | 54 | rexlimdva 3194 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) →
(∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
56 | | sstr2 3885 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) |
57 | 56 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢 → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) |
58 | 57 | anim2d 615 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢 → ((𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → (𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
59 | 58 | reximdv 3183 |
. . . . . . . . . . . . . 14
⊢ ((𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢 → (∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
60 | 55, 59 | syl9 77 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → ((𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢 → (∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
61 | 60 | impd 414 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (((𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
62 | 61 | rexlimdva 3194 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∃𝑥 ∈ ℝ+
((𝐶(ball‘(abs ∘
− ))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
63 | 39, 62 | syl5 34 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((∃𝑥 ∈ ℝ+
(𝐶(ball‘(abs ∘
− ))𝑥) ⊆ 𝑢 ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
64 | 63 | expd 419 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∃𝑥 ∈ ℝ+
(𝐶(ball‘(abs ∘
− ))𝑥) ⊆ 𝑢 → (∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
65 | 38, 64 | syl5 34 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝐶 ∈ 𝑢) → (∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
66 | 65 | expdimp 456 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑢 ∈
(TopOpen‘ℂfld)) → (𝐶 ∈ 𝑢 → (∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
67 | 66 | com23 86 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑢 ∈
(TopOpen‘ℂfld)) → (∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
68 | 67 | ralrimdva 3101 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
69 | 36, 68 | impbid 215 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
70 | 1 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ 𝐹:𝐴⟶ℂ) |
71 | 70 | ffund 6509 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ Fun 𝐹) |
72 | | inss2 4121 |
. . . . . . . . . 10
⊢ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝐴 ∖ {𝐵}) |
73 | | difss 4023 |
. . . . . . . . . . 11
⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴 |
74 | 70 | fdmd 6516 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ dom 𝐹 = 𝐴) |
75 | 73, 74 | sseqtrrid 3931 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝐴 ∖ {𝐵}) ⊆ dom 𝐹) |
76 | 72, 75 | sstrid 3889 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵})) ⊆ dom 𝐹) |
77 | | funimass4 6735 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ dom 𝐹) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) |
78 | 71, 76, 77 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) |
79 | 6 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
80 | | simplrr 778 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℝ+) |
81 | 80 | rpxrd 12516 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℝ*) |
82 | 3 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ) |
83 | 73, 2 | sstrid 3889 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ) |
84 | 83 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝐴 ∖ {𝐵}) ⊆
ℂ) |
85 | 84 | sselda 3878 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ∈ ℂ) |
86 | | elbl3 23146 |
. . . . . . . . . . . . 13
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ ℝ*) ∧ (𝐵 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (𝑧(abs ∘ − )𝐵) < 𝑦)) |
87 | 79, 81, 82, 85, 86 | syl22anc 838 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (𝑧(abs ∘ − )𝐵) < 𝑦)) |
88 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (abs
∘ − ) = (abs ∘ − ) |
89 | 88 | cnmetdval 23524 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑧(abs ∘ − )𝐵) = (abs‘(𝑧 − 𝐵))) |
90 | 85, 82, 89 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧(abs ∘ − )𝐵) = (abs‘(𝑧 − 𝐵))) |
91 | 90 | breq1d 5041 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝑧(abs ∘ − )𝐵) < 𝑦 ↔ (abs‘(𝑧 − 𝐵)) < 𝑦)) |
92 | 87, 91 | bitrd 282 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (abs‘(𝑧 − 𝐵)) < 𝑦)) |
93 | | simplrl 777 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ+) |
94 | 93 | rpxrd 12516 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ*) |
95 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐶 ∈ ℂ) |
96 | | eldifi 4018 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧 ∈ 𝐴) |
97 | | ffvelrn 6860 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ) |
98 | 70, 96, 97 | syl2an 599 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ ℂ) |
99 | | elbl3 23146 |
. . . . . . . . . . . . 13
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℝ*) ∧ (𝐶 ∈ ℂ ∧ (𝐹‘𝑧) ∈ ℂ)) → ((𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ((𝐹‘𝑧)(abs ∘ − )𝐶) < 𝑥)) |
100 | 79, 94, 95, 98, 99 | syl22anc 838 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ((𝐹‘𝑧)(abs ∘ − )𝐶) < 𝑥)) |
101 | 88 | cnmetdval 23524 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑧) ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐹‘𝑧)(abs ∘ − )𝐶) = (abs‘((𝐹‘𝑧) − 𝐶))) |
102 | 98, 95, 101 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧)(abs ∘ − )𝐶) = (abs‘((𝐹‘𝑧) − 𝐶))) |
103 | 102 | breq1d 5041 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (((𝐹‘𝑧)(abs ∘ − )𝐶) < 𝑥 ↔ (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) |
104 | 100, 103 | bitrd 282 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) |
105 | 92, 104 | imbi12d 348 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
106 | 105 | ralbidva 3108 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (∀𝑧 ∈
(𝐴 ∖ {𝐵})(𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ∀𝑧 ∈ (𝐴 ∖ {𝐵})((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
107 | | elin 3860 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ↔ (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵}))) |
108 | 107 | biancomi 466 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ↔ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) |
109 | 108 | imbi1i 353 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) |
110 | | impexp 454 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ (𝑧 ∈ (𝐴 ∖ {𝐵}) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
111 | 109, 110 | bitr2i 279 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) ↔ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) |
112 | 111 | ralbii2 3078 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝐴 ∖ {𝐵})(𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) |
113 | | impexp 454 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧 ∈ 𝐴 → (𝑧 ≠ 𝐵 → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) |
114 | | eldifsn 4676 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵)) |
115 | 114 | imbi1i 353 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
116 | | impexp 454 |
. . . . . . . . . . . 12
⊢ (((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥) ↔ (𝑧 ≠ 𝐵 → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
117 | 116 | imbi2i 339 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧 ∈ 𝐴 → (𝑧 ≠ 𝐵 → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) |
118 | 113, 115,
117 | 3bitr4i 306 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
119 | 118 | ralbii2 3078 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝐴 ∖ {𝐵})((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) |
120 | 106, 112,
119 | 3bitr3g 316 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (∀𝑧 ∈
((𝐵(ball‘(abs ∘
− ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
121 | 78, 120 | bitrd 282 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
122 | 121 | anassrs 471 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ ((𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
123 | 122 | rexbidva 3206 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) →
(∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
124 | 123 | ralbidva 3108 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
125 | 69, 124 | bitrd 282 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
126 | 125 | pm5.32da 582 |
. 2
⊢ (𝜑 → ((𝐶 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) |
127 | 5, 126 | bitrd 282 |
1
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) |