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 25041 |
. 2
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))) |
6 | | cnxmet 23936 |
. . . . . . . . 9
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
7 | | simplr 766 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈
ℂ) |
8 | | simpr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
9 | | blcntr 23566 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) |
10 | 6, 7, 8, 9 | mp3an2i 1465 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) |
11 | | rpxr 12739 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ*) |
12 | 11 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ*) |
13 | 4 | cnfldtopn 23945 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
14 | 13 | blopn 23656 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ*) → (𝐶(ball‘(abs ∘ −
))𝑥) ∈
(TopOpen‘ℂfld)) |
15 | 6, 7, 12, 14 | mp3an2i 1465 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (𝐶(ball‘(abs ∘ −
))𝑥) ∈
(TopOpen‘ℂfld)) |
16 | | eleq2 2827 |
. . . . . . . . . . 11
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐶 ∈ 𝑢 ↔ 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) |
17 | | sseq2 3947 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢 ↔ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
18 | 17 | anbi2d 629 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ (𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
19 | 18 | rexbidv 3226 |
. . . . . . . . . . 11
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → (∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
20 | 16, 19 | imbi12d 345 |
. . . . . . . . . 10
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ (𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))) |
21 | 20 | rspcv 3557 |
. . . . . . . . 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 23649 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐵 ∈ 𝑣) → ∃𝑦 ∈ ℝ+
(𝐵(ball‘(abs ∘
− ))𝑦) ⊆ 𝑣) |
25 | 6, 24 | mp3an1 1447 |
. . . . . . . . . 10
⊢ ((𝑣 ∈
(TopOpen‘ℂfld) ∧ 𝐵 ∈ 𝑣) → ∃𝑦 ∈ ℝ+ (𝐵(ball‘(abs ∘ −
))𝑦) ⊆ 𝑣) |
26 | | ssrin 4167 |
. . . . . . . . . . . . 13
⊢ ((𝐵(ball‘(abs ∘ −
))𝑦) ⊆ 𝑣 → ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑣 ∩ (𝐴 ∖ {𝐵}))) |
27 | | imass2 6010 |
. . . . . . . . . . . . 13
⊢ (((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑣 ∩ (𝐴 ∖ {𝐵})) → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵})))) |
28 | | sstr2 3928 |
. . . . . . . . . . . . 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 3202 |
. . . . . . . . . 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 455 |
. . . . . . . 8
⊢ ((𝑣 ∈
(TopOpen‘ℂfld) ∧ (𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) → ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) |
34 | 33 | rexlimiva 3210 |
. . . . . . 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 3106 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
37 | 13 | mopni2 23649 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝐶 ∈ 𝑢) → ∃𝑥 ∈ ℝ+
(𝐶(ball‘(abs ∘
− ))𝑥) ⊆ 𝑢) |
38 | 6, 37 | mp3an1 1447 |
. . . . . . . . 9
⊢ ((𝑢 ∈
(TopOpen‘ℂfld) ∧ 𝐶 ∈ 𝑢) → ∃𝑥 ∈ ℝ+ (𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢) |
39 | | r19.29r 3185 |
. . . . . . . . . . 11
⊢
((∃𝑥 ∈
ℝ+ (𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑥 ∈ ℝ+
((𝐶(ball‘(abs ∘
− ))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
40 | 3 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝐵 ∈
ℂ) |
41 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝑦 ∈
ℝ+) |
42 | 41 | rpxrd 12773 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝑦 ∈
ℝ*) |
43 | 13 | blopn 23656 |
. . . . . . . . . . . . . . . . 17
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ*) → (𝐵(ball‘(abs ∘ −
))𝑦) ∈
(TopOpen‘ℂfld)) |
44 | 6, 40, 42, 43 | mp3an2i 1465 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ (𝐵(ball‘(abs
∘ − ))𝑦) ∈
(TopOpen‘ℂfld)) |
45 | | blcntr 23566 |
. . . . . . . . . . . . . . . . 17
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ+) → 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) |
46 | 6, 40, 41, 45 | mp3an2i 1465 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝐵 ∈ (𝐵(ball‘(abs ∘ −
))𝑦)) |
47 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐵 ∈ 𝑣 ↔ 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) |
48 | | ineq1 4139 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝑣 ∩ (𝐴 ∖ {𝐵})) = ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) |
49 | 48 | imaeq2d 5969 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) = (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})))) |
50 | 49 | sseq1d 3952 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
51 | 47, 50 | anbi12d 631 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → ((𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ (𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
52 | 51 | rspcev 3561 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵(ball‘(abs ∘ −
))𝑦) ∈
(TopOpen‘ℂfld) ∧ (𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
53 | 52 | expr 457 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵(ball‘(abs ∘ −
))𝑦) ∈
(TopOpen‘ℂfld) ∧ 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
54 | 44, 46, 53 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ ((𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
55 | 54 | rexlimdva 3213 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) →
(∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
56 | | sstr2 3928 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) |
57 | 56 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢 → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) |
58 | 57 | anim2d 612 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢 → ((𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → (𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
59 | 58 | reximdv 3202 |
. . . . . . . . . . . . . 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 411 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (((𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
62 | 61 | rexlimdva 3213 |
. . . . . . . . . . 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 416 |
. . . . . . . . 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 453 |
. . . . . . 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 3106 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
69 | 36, 68 | impbid 211 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) |
70 | 1 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ 𝐹:𝐴⟶ℂ) |
71 | 70 | ffund 6604 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ Fun 𝐹) |
72 | | inss2 4163 |
. . . . . . . . . 10
⊢ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝐴 ∖ {𝐵}) |
73 | | difss 4066 |
. . . . . . . . . . 11
⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴 |
74 | 70 | fdmd 6611 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ dom 𝐹 = 𝐴) |
75 | 73, 74 | sseqtrrid 3974 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝐴 ∖ {𝐵}) ⊆ dom 𝐹) |
76 | 72, 75 | sstrid 3932 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵})) ⊆ dom 𝐹) |
77 | | funimass4 6834 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ dom 𝐹) → ((𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) |
78 | 71, 76, 77 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) |
79 | 6 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
80 | | simplrr 775 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℝ+) |
81 | 80 | rpxrd 12773 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℝ*) |
82 | 3 | ad3antrrr 727 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ) |
83 | 73, 2 | sstrid 3932 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ) |
84 | 83 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝐴 ∖ {𝐵}) ⊆
ℂ) |
85 | 84 | sselda 3921 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ∈ ℂ) |
86 | | elbl3 23545 |
. . . . . . . . . . . . 13
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ ℝ*) ∧ (𝐵 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (𝑧(abs ∘ − )𝐵) < 𝑦)) |
87 | 79, 81, 82, 85, 86 | syl22anc 836 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (𝑧(abs ∘ − )𝐵) < 𝑦)) |
88 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (abs
∘ − ) = (abs ∘ − ) |
89 | 88 | cnmetdval 23934 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑧(abs ∘ − )𝐵) = (abs‘(𝑧 − 𝐵))) |
90 | 85, 82, 89 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧(abs ∘ − )𝐵) = (abs‘(𝑧 − 𝐵))) |
91 | 90 | breq1d 5084 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝑧(abs ∘ − )𝐵) < 𝑦 ↔ (abs‘(𝑧 − 𝐵)) < 𝑦)) |
92 | 87, 91 | bitrd 278 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (abs‘(𝑧 − 𝐵)) < 𝑦)) |
93 | | simplrl 774 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ+) |
94 | 93 | rpxrd 12773 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ*) |
95 | | simpllr 773 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐶 ∈ ℂ) |
96 | | eldifi 4061 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧 ∈ 𝐴) |
97 | | ffvelrn 6959 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ) |
98 | 70, 96, 97 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ ℂ) |
99 | | elbl3 23545 |
. . . . . . . . . . . . 13
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℝ*) ∧ (𝐶 ∈ ℂ ∧ (𝐹‘𝑧) ∈ ℂ)) → ((𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ((𝐹‘𝑧)(abs ∘ − )𝐶) < 𝑥)) |
100 | 79, 94, 95, 98, 99 | syl22anc 836 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ((𝐹‘𝑧)(abs ∘ − )𝐶) < 𝑥)) |
101 | 88 | cnmetdval 23934 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑧) ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐹‘𝑧)(abs ∘ − )𝐶) = (abs‘((𝐹‘𝑧) − 𝐶))) |
102 | 98, 95, 101 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧)(abs ∘ − )𝐶) = (abs‘((𝐹‘𝑧) − 𝐶))) |
103 | 102 | breq1d 5084 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (((𝐹‘𝑧)(abs ∘ − )𝐶) < 𝑥 ↔ (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) |
104 | 100, 103 | bitrd 278 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) |
105 | 92, 104 | imbi12d 345 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
106 | 105 | ralbidva 3111 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (∀𝑧 ∈
(𝐴 ∖ {𝐵})(𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ∀𝑧 ∈ (𝐴 ∖ {𝐵})((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
107 | | elin 3903 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ↔ (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵}))) |
108 | 107 | biancomi 463 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ↔ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) |
109 | 108 | imbi1i 350 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) |
110 | | impexp 451 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ (𝑧 ∈ (𝐴 ∖ {𝐵}) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)))) |
111 | 109, 110 | bitr2i 275 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) ↔ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) |
112 | 111 | ralbii2 3090 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝐴 ∖ {𝐵})(𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) |
113 | | impexp 451 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧 ∈ 𝐴 → (𝑧 ≠ 𝐵 → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) |
114 | | eldifsn 4720 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵)) |
115 | 114 | imbi1i 350 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
116 | | impexp 451 |
. . . . . . . . . . . 12
⊢ (((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥) ↔ (𝑧 ≠ 𝐵 → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
117 | 116 | imbi2i 336 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧 ∈ 𝐴 → (𝑧 ≠ 𝐵 → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) |
118 | 113, 115,
117 | 3bitr4i 303 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧 ∈ 𝐴 → ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
119 | 118 | ralbii2 3090 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝐴 ∖ {𝐵})((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) |
120 | 106, 112,
119 | 3bitr3g 313 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (∀𝑧 ∈
((𝐵(ball‘(abs ∘
− ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
121 | 78, 120 | bitrd 278 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
122 | 121 | anassrs 468 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ ((𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
123 | 122 | rexbidva 3225 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) →
(∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
124 | 123 | ralbidva 3111 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
125 | 69, 124 | bitrd 278 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) |
126 | 125 | pm5.32da 579 |
. 2
⊢ (𝜑 → ((𝐶 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) |
127 | 5, 126 | bitrd 278 |
1
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) |