Step | Hyp | Ref
| Expression |
1 | | ellimc3.f |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
2 | | ellimc3.a |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
3 | | ellimc3.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℂ) |
4 | | eqid 2610 |
. . 3
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
5 | 1, 2, 3, 4 | ellimc2 23447 |
. 2
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))) |
6 | | cnxmet 22386 |
. . . . . . . . . 10
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
7 | 6 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (abs
∘ − ) ∈ (∞Met‘ℂ)) |
8 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈
ℂ) |
9 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
10 | | blcntr 22028 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) |
11 | 7, 8, 9, 10 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) |
12 | | rpxr 11716 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ*) |
13 | 12 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ*) |
14 | 4 | cnfldtopn 22395 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
15 | 14 | blopn 22115 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ*) → (𝐶(ball‘(abs ∘ −
))𝑥) ∈
(TopOpen‘ℂfld)) |
16 | 7, 8, 13, 15 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (𝐶(ball‘(abs ∘ −
))𝑥) ∈
(TopOpen‘ℂfld)) |
17 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐶 ∈ 𝑢 ↔ 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) |
18 | | sseq2 3590 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢 ↔ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
19 | 18 | anbi2d 736 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ (𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
20 | 19 | rexbidv 3034 |
. . . . . . . . . . 11
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → (∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
21 | 17, 20 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ (𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))) |
22 | 21 | rspcv 3278 |
. . . . . . . . 9
⊢ ((𝐶(ball‘(abs ∘ −
))𝑥) ∈
(TopOpen‘ℂfld) → (∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → (𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))) |
23 | 16, 22 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) →
(∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → (𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))) |
24 | 11, 23 | mpid 43 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) →
(∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
25 | 14 | mopni2 22108 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐵 ∈ 𝑣) → ∃𝑦 ∈ ℝ+
(𝐵(ball‘(abs ∘
− ))𝑦) ⊆ 𝑣) |
26 | 6, 25 | mp3an1 1403 |
. . . . . . . . . 10
⊢ ((𝑣 ∈
(TopOpen‘ℂfld) ∧ 𝐵 ∈ 𝑣) → ∃𝑦 ∈ ℝ+ (𝐵(ball‘(abs ∘ −
))𝑦) ⊆ 𝑣) |
27 | | ssrin 3800 |
. . . . . . . . . . . . 13
⊢ ((𝐵(ball‘(abs ∘ −
))𝑦) ⊆ 𝑣 → ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑣 ∩ (𝐴 ∖ {𝐵}))) |
28 | | imass2 5420 |
. . . . . . . . . . . . 13
⊢ (((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑣 ∩ (𝐴 ∖ {𝐵})) → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵})))) |
29 | | sstr2 3575 |
. . . . . . . . . . . . 13
⊢ ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
30 | 27, 28, 29 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝐵(ball‘(abs ∘ −
))𝑦) ⊆ 𝑣 → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
31 | 30 | com12 32 |
. . . . . . . . . . 11
⊢ ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐵(ball‘(abs ∘ − ))𝑦) ⊆ 𝑣 → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
32 | 31 | reximdv 2999 |
. . . . . . . . . 10
⊢ ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (∃𝑦 ∈ ℝ+
(𝐵(ball‘(abs ∘
− ))𝑦) ⊆ 𝑣 → ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
33 | 26, 32 | syl5com 31 |
. . . . . . . . 9
⊢ ((𝑣 ∈
(TopOpen‘ℂfld) ∧ 𝐵 ∈ 𝑣) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
34 | 33 | impr 647 |
. . . . . . . 8
⊢ ((𝑣 ∈
(TopOpen‘ℂfld) ∧ (𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) → ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) |
35 | 34 | rexlimiva 3010 |
. . . . . . 7
⊢
(∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) |
36 | 24, 35 | syl6 34 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) →
(∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
37 | 36 | ralrimdva 2952 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
38 | 14 | mopni2 22108 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝐶 ∈ 𝑢) → ∃𝑥 ∈ ℝ+
(𝐶(ball‘(abs ∘
− ))𝑥) ⊆ 𝑢) |
39 | 6, 38 | mp3an1 1403 |
. . . . . . . . 9
⊢ ((𝑢 ∈
(TopOpen‘ℂfld) ∧ 𝐶 ∈ 𝑢) → ∃𝑥 ∈ ℝ+ (𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢) |
40 | | r19.29r 3055 |
. . . . . . . . . . 11
⊢
((∃𝑥 ∈
ℝ+ (𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑥 ∈ ℝ+
((𝐶(ball‘(abs ∘
− ))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
41 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ (abs ∘ − ) ∈
(∞Met‘ℂ)) |
42 | 3 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝐵 ∈
ℂ) |
43 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝑦 ∈
ℝ+) |
44 | 43 | rpxrd 11749 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝑦 ∈
ℝ*) |
45 | 14 | blopn 22115 |
. . . . . . . . . . . . . . . . 17
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ*) → (𝐵(ball‘(abs ∘ −
))𝑦) ∈
(TopOpen‘ℂfld)) |
46 | 41, 42, 44, 45 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ (𝐵(ball‘(abs
∘ − ))𝑦) ∈
(TopOpen‘ℂfld)) |
47 | | blcntr 22028 |
. . . . . . . . . . . . . . . . 17
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ+) → 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) |
48 | 41, 42, 43, 47 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝐵 ∈ (𝐵(ball‘(abs ∘ −
))𝑦)) |
49 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐵 ∈ 𝑣 ↔ 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) |
50 | | ineq1 3769 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝑣 ∩ (𝐴 ∖ {𝐵})) = ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) |
51 | 50 | imaeq2d 5385 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) = (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})))) |
52 | 51 | sseq1d 3595 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
53 | 49, 52 | anbi12d 743 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → ((𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ (𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
54 | 53 | rspcev 3282 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵(ball‘(abs ∘ −
))𝑦) ∈
(TopOpen‘ℂfld) ∧ (𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
55 | 54 | expr 641 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵(ball‘(abs ∘ −
))𝑦) ∈
(TopOpen‘ℂfld) ∧ 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
56 | 46, 48, 55 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ ((𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
57 | 56 | rexlimdva 3013 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) →
(∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
58 | | sstr2 3575 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) |
59 | 58 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢 → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) |
60 | 59 | anim2d 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢 → ((𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → (𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
61 | 60 | reximdv 2999 |
. . . . . . . . . . . . . 14
⊢ ((𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢 → (∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
62 | 57, 61 | syl9 75 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → ((𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢 → (∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
63 | 62 | impd 446 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (((𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
64 | 63 | rexlimdva 3013 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∃𝑥 ∈ ℝ+
((𝐶(ball‘(abs ∘
− ))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
65 | 40, 64 | syl5 33 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((∃𝑥 ∈ ℝ+
(𝐶(ball‘(abs ∘
− ))𝑥) ⊆ 𝑢 ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
66 | 65 | expd 451 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∃𝑥 ∈ ℝ+
(𝐶(ball‘(abs ∘
− ))𝑥) ⊆ 𝑢 → (∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
67 | 39, 66 | syl5 33 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝐶 ∈ 𝑢) → (∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
68 | 67 | expdimp 452 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑢 ∈
(TopOpen‘ℂfld)) → (𝐶 ∈ 𝑢 → (∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
69 | 68 | com23 84 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑢 ∈
(TopOpen‘ℂfld)) → (∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
70 | 69 | ralrimdva 2952 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
71 | 37, 70 | impbid 201 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
72 | 1 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ 𝐹:𝐴⟶ℂ) |
73 | | ffun 5961 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶ℂ → Fun 𝐹) |
74 | 72, 73 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ Fun 𝐹) |
75 | | inss2 3796 |
. . . . . . . . . 10
⊢ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝐴 ∖ {𝐵}) |
76 | | difss 3699 |
. . . . . . . . . . 11
⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴 |
77 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴) |
78 | 72, 77 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ dom 𝐹 = 𝐴) |
79 | 76, 78 | syl5sseqr 3617 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝐴 ∖ {𝐵}) ⊆ dom 𝐹) |
80 | 75, 79 | syl5ss 3579 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵})) ⊆ dom 𝐹) |
81 | | funimass4 6157 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ dom 𝐹) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) |
82 | 74, 80, 81 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) |
83 | 6 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
84 | | simplrr 797 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℝ+) |
85 | 84 | rpxrd 11749 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℝ*) |
86 | 3 | ad3antrrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ) |
87 | 76, 2 | syl5ss 3579 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ) |
88 | 87 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝐴 ∖ {𝐵}) ⊆
ℂ) |
89 | 88 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ∈ ℂ) |
90 | | elbl3 22007 |
. . . . . . . . . . . . 13
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ ℝ*) ∧ (𝐵 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (𝑧(abs ∘ − )𝐵) < 𝑦)) |
91 | 83, 85, 86, 89, 90 | syl22anc 1319 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (𝑧(abs ∘ − )𝐵) < 𝑦)) |
92 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (abs
∘ − ) = (abs ∘ − ) |
93 | 92 | cnmetdval 22384 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑧(abs ∘ − )𝐵) = (abs‘(𝑧 − 𝐵))) |
94 | 89, 86, 93 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧(abs ∘ − )𝐵) = (abs‘(𝑧 − 𝐵))) |
95 | 94 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝑧(abs ∘ − )𝐵) < 𝑦 ↔ (abs‘(𝑧 − 𝐵)) < 𝑦)) |
96 | 91, 95 | bitrd 267 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (abs‘(𝑧 − 𝐵)) < 𝑦)) |
97 | | simplrl 796 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ+) |
98 | 97 | rpxrd 11749 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ*) |
99 | | simpllr 795 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐶 ∈ ℂ) |
100 | | eldifi 3694 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧 ∈ 𝐴) |
101 | | ffvelrn 6265 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ) |
102 | 72, 100, 101 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ ℂ) |
103 | | elbl3 22007 |
. . . . . . . . . . . . 13
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℝ*) ∧ (𝐶 ∈ ℂ ∧ (𝐹‘𝑧) ∈ ℂ)) → ((𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ((𝐹‘𝑧)(abs ∘ − )𝐶) < 𝑥)) |
104 | 83, 98, 99, 102, 103 | syl22anc 1319 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ((𝐹‘𝑧)(abs ∘ − )𝐶) < 𝑥)) |
105 | 92 | cnmetdval 22384 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑧) ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐹‘𝑧)(abs ∘ − )𝐶) = (abs‘((𝐹‘𝑧) − 𝐶))) |
106 | 102, 99, 105 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧)(abs ∘ − )𝐶) = (abs‘((𝐹‘𝑧) − 𝐶))) |
107 | 106 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (((𝐹‘𝑧)(abs ∘ − )𝐶) < 𝑥 ↔ (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) |
108 | 104, 107 | bitrd 267 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) |
109 | 96, 108 | imbi12d 333 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
110 | 109 | ralbidva 2968 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (∀𝑧 ∈
(𝐴 ∖ {𝐵})(𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ∀𝑧 ∈ (𝐴 ∖ {𝐵})((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
111 | | elin 3758 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ↔ (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵}))) |
112 | | ancom 465 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) ↔ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) |
113 | 111, 112 | bitri 263 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ↔ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) |
114 | 113 | imbi1i 338 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) |
115 | | impexp 461 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ (𝑧 ∈ (𝐴 ∖ {𝐵}) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
116 | 114, 115 | bitr2i 264 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) ↔ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) |
117 | 116 | ralbii2 2961 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝐴 ∖ {𝐵})(𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) |
118 | | impexp 461 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧 ∈ 𝐴 → (𝑧 ≠ 𝐵 → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) |
119 | | eldifsn 4260 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵)) |
120 | 119 | imbi1i 338 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
121 | | impexp 461 |
. . . . . . . . . . . 12
⊢ (((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥) ↔ (𝑧 ≠ 𝐵 → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
122 | 121 | imbi2i 325 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧 ∈ 𝐴 → (𝑧 ≠ 𝐵 → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) |
123 | 118, 120,
122 | 3bitr4i 291 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
124 | 123 | ralbii2 2961 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝐴 ∖ {𝐵})((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) |
125 | 110, 117,
124 | 3bitr3g 301 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (∀𝑧 ∈
((𝐵(ball‘(abs ∘
− ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
126 | 82, 125 | bitrd 267 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
127 | 126 | anassrs 678 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ ((𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
128 | 127 | rexbidva 3031 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) →
(∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
129 | 128 | ralbidva 2968 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
130 | 71, 129 | bitrd 267 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
131 | 130 | pm5.32da 671 |
. 2
⊢ (𝜑 → ((𝐶 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) |
132 | 5, 131 | bitrd 267 |
1
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) |