| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ellimc3.f | . . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) | 
| 2 |  | ellimc3.a | . . 3
⊢ (𝜑 → 𝐴 ⊆ ℂ) | 
| 3 |  | ellimc3.b | . . 3
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 4 |  | eqid 2736 | . . 3
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 5 | 1, 2, 3, 4 | ellimc2 25913 | . 2
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))) | 
| 6 |  | cnxmet 24794 | . . . . . . . . 9
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) | 
| 7 |  | simplr 768 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈
ℂ) | 
| 8 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) | 
| 9 |  | blcntr 24424 | . . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) | 
| 10 | 6, 7, 8, 9 | mp3an2i 1467 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) | 
| 11 |  | rpxr 13045 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ*) | 
| 12 | 11 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ*) | 
| 13 | 4 | cnfldtopn 24803 | . . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) | 
| 14 | 13 | blopn 24514 | . . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ*) → (𝐶(ball‘(abs ∘ −
))𝑥) ∈
(TopOpen‘ℂfld)) | 
| 15 | 6, 7, 12, 14 | mp3an2i 1467 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (𝐶(ball‘(abs ∘ −
))𝑥) ∈
(TopOpen‘ℂfld)) | 
| 16 |  | eleq2 2829 | . . . . . . . . . . 11
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → (𝐶 ∈ 𝑢 ↔ 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) | 
| 17 |  | sseq2 4009 | . . . . . . . . . . . . 13
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢 ↔ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) | 
| 18 | 17 | anbi2d 630 | . . . . . . . . . . . 12
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ (𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) | 
| 19 | 18 | rexbidv 3178 | . . . . . . . . . . 11
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → (∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢) ↔ ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) | 
| 20 | 16, 19 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑢 = (𝐶(ball‘(abs ∘ − ))𝑥) → ((𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ (𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))))) | 
| 21 | 20 | rspcv 3617 | . . . . . . . . 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 24507 | . . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑣 ∈ (TopOpen‘ℂfld)
∧ 𝐵 ∈ 𝑣) → ∃𝑦 ∈ ℝ+
(𝐵(ball‘(abs ∘
− ))𝑦) ⊆ 𝑣) | 
| 25 | 6, 24 | mp3an1 1449 | . . . . . . . . . 10
⊢ ((𝑣 ∈
(TopOpen‘ℂfld) ∧ 𝐵 ∈ 𝑣) → ∃𝑦 ∈ ℝ+ (𝐵(ball‘(abs ∘ −
))𝑦) ⊆ 𝑣) | 
| 26 |  | ssrin 4241 | . . . . . . . . . . . . 13
⊢ ((𝐵(ball‘(abs ∘ −
))𝑦) ⊆ 𝑣 → ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑣 ∩ (𝐴 ∖ {𝐵}))) | 
| 27 |  | imass2 6119 | . . . . . . . . . . . . 13
⊢ (((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑣 ∩ (𝐴 ∖ {𝐵})) → (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵})))) | 
| 28 |  | sstr2 3989 | . . . . . . . . . . . . 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 3169 | . . . . . . . . . 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 454 | . . . . . . . 8
⊢ ((𝑣 ∈
(TopOpen‘ℂfld) ∧ (𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) → ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) | 
| 34 | 33 | rexlimiva 3146 | . . . . . . 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 3153 | . . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) | 
| 37 | 13 | mopni2 24507 | . . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑢 ∈ (TopOpen‘ℂfld)
∧ 𝐶 ∈ 𝑢) → ∃𝑥 ∈ ℝ+
(𝐶(ball‘(abs ∘
− ))𝑥) ⊆ 𝑢) | 
| 38 | 6, 37 | mp3an1 1449 | . . . . . . . . 9
⊢ ((𝑢 ∈
(TopOpen‘ℂfld) ∧ 𝐶 ∈ 𝑢) → ∃𝑥 ∈ ℝ+ (𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢) | 
| 39 |  | r19.29r 3115 | . . . . . . . . . . 11
⊢
((∃𝑥 ∈
ℝ+ (𝐶(ball‘(abs ∘ − ))𝑥) ⊆ 𝑢 ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑥 ∈ ℝ+
((𝐶(ball‘(abs ∘
− ))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) | 
| 40 | 3 | ad3antrrr 730 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝐵 ∈
ℂ) | 
| 41 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝑦 ∈
ℝ+) | 
| 42 | 41 | rpxrd 13079 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝑦 ∈
ℝ*) | 
| 43 | 13 | blopn 24514 | . . . . . . . . . . . . . . . . 17
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ*) → (𝐵(ball‘(abs ∘ −
))𝑦) ∈
(TopOpen‘ℂfld)) | 
| 44 | 6, 40, 42, 43 | mp3an2i 1467 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ (𝐵(ball‘(abs
∘ − ))𝑦) ∈
(TopOpen‘ℂfld)) | 
| 45 |  | blcntr 24424 | . . . . . . . . . . . . . . . . 17
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℝ+) → 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) | 
| 46 | 6, 40, 41, 45 | mp3an2i 1467 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ 𝐵 ∈ (𝐵(ball‘(abs ∘ −
))𝑦)) | 
| 47 |  | eleq2 2829 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐵 ∈ 𝑣 ↔ 𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) | 
| 48 |  | ineq1 4212 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝑣 ∩ (𝐴 ∖ {𝐵})) = ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) | 
| 49 | 48 | imaeq2d 6077 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) = (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})))) | 
| 50 | 49 | sseq1d 4014 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → ((𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) | 
| 51 | 47, 50 | anbi12d 632 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝐵(ball‘(abs ∘ − ))𝑦) → ((𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ (𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) | 
| 52 | 51 | rspcev 3621 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐵(ball‘(abs ∘ −
))𝑦) ∈
(TopOpen‘ℂfld) ∧ (𝐵 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) | 
| 53 | 52 | expr 456 | . . . . . . . . . . . . . . . 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 3154 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) →
(∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)))) | 
| 56 |  | sstr2 3989 | . . . . . . . . . . . . . . . . 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 3169 | . . . . . . . . . . . . . 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 410 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) → (((𝐶(ball‘(abs ∘ −
))𝑥) ⊆ 𝑢 ∧ ∃𝑦 ∈ ℝ+ (𝐹 “ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥)) → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) | 
| 62 | 61 | rexlimdva 3154 | . . . . . . . . . . 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 415 | . . . . . . . . 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 452 | . . . . . . 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 3153 | . . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) → ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) | 
| 69 | 36, 68 | impbid 212 | . . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
(𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥))) | 
| 70 | 1 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ 𝐹:𝐴⟶ℂ) | 
| 71 | 70 | ffund 6739 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ Fun 𝐹) | 
| 72 |  | inss2 4237 | . . . . . . . . . 10
⊢ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝐴 ∖ {𝐵}) | 
| 73 |  | difss 4135 | . . . . . . . . . . 11
⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴 | 
| 74 | 70 | fdmd 6745 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ dom 𝐹 = 𝐴) | 
| 75 | 73, 74 | sseqtrrid 4026 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝐴 ∖ {𝐵}) ⊆ dom 𝐹) | 
| 76 | 72, 75 | sstrid 3994 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵})) ⊆ dom 𝐹) | 
| 77 |  | funimass4 6972 | . . . . . . . . 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 777 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℝ+) | 
| 81 | 80 | rpxrd 13079 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑦 ∈ ℝ*) | 
| 82 | 3 | ad3antrrr 730 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐵 ∈ ℂ) | 
| 83 | 73, 2 | sstrid 3994 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 ∖ {𝐵}) ⊆ ℂ) | 
| 84 | 83 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝐴 ∖ {𝐵}) ⊆
ℂ) | 
| 85 | 84 | sselda 3982 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑧 ∈ ℂ) | 
| 86 |  | elbl3 24403 | . . . . . . . . . . . . 13
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ ℝ*) ∧ (𝐵 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (𝑧(abs ∘ − )𝐵) < 𝑦)) | 
| 87 | 79, 81, 82, 85, 86 | syl22anc 838 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (𝑧(abs ∘ − )𝐵) < 𝑦)) | 
| 88 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ (abs
∘ − ) = (abs ∘ − ) | 
| 89 | 88 | cnmetdval 24792 | . . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑧(abs ∘ − )𝐵) = (abs‘(𝑧 − 𝐵))) | 
| 90 | 85, 82, 89 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧(abs ∘ − )𝐵) = (abs‘(𝑧 − 𝐵))) | 
| 91 | 90 | breq1d 5152 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝑧(abs ∘ − )𝐵) < 𝑦 ↔ (abs‘(𝑧 − 𝐵)) < 𝑦)) | 
| 92 | 87, 91 | bitrd 279 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ↔ (abs‘(𝑧 − 𝐵)) < 𝑦)) | 
| 93 |  | simplrl 776 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ+) | 
| 94 | 93 | rpxrd 13079 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝑥 ∈ ℝ*) | 
| 95 |  | simpllr 775 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → 𝐶 ∈ ℂ) | 
| 96 |  | eldifi 4130 | . . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧 ∈ 𝐴) | 
| 97 |  | ffvelcdm 7100 | . . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ) | 
| 98 | 70, 96, 97 | syl2an 596 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ ℂ) | 
| 99 |  | elbl3 24403 | . . . . . . . . . . . . 13
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℝ*) ∧ (𝐶 ∈ ℂ ∧ (𝐹‘𝑧) ∈ ℂ)) → ((𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ((𝐹‘𝑧)(abs ∘ − )𝐶) < 𝑥)) | 
| 100 | 79, 94, 95, 98, 99 | syl22anc 838 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ((𝐹‘𝑧)(abs ∘ − )𝐶) < 𝑥)) | 
| 101 | 88 | cnmetdval 24792 | . . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑧) ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐹‘𝑧)(abs ∘ − )𝐶) = (abs‘((𝐹‘𝑧) − 𝐶))) | 
| 102 | 98, 95, 101 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧)(abs ∘ − )𝐶) = (abs‘((𝐹‘𝑧) − 𝐶))) | 
| 103 | 102 | breq1d 5152 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → (((𝐹‘𝑧)(abs ∘ − )𝐶) < 𝑥 ↔ (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) | 
| 104 | 100, 103 | bitrd 279 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) | 
| 105 | 92, 104 | imbi12d 344 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
∧ 𝑧 ∈ (𝐴 ∖ {𝐵})) → ((𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) | 
| 106 | 105 | ralbidva 3175 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (∀𝑧 ∈
(𝐴 ∖ {𝐵})(𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ∀𝑧 ∈ (𝐴 ∖ {𝐵})((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) | 
| 107 |  | elin 3966 | . . . . . . . . . . . . 13
⊢ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ↔ (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) ∧ 𝑧 ∈ (𝐴 ∖ {𝐵}))) | 
| 108 | 107 | biancomi 462 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) ↔ (𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦))) | 
| 109 | 108 | imbi1i 349 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) | 
| 110 |  | impexp 450 | . . . . . . . . . . 11
⊢ (((𝑧 ∈ (𝐴 ∖ {𝐵}) ∧ 𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦)) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ (𝑧 ∈ (𝐴 ∖ {𝐵}) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)))) | 
| 111 | 109, 110 | bitr2i 276 | . . . . . . . . . 10
⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) → (𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) ↔ (𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵})) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥))) | 
| 112 | 111 | ralbii2 3088 | . . . . . . . . 9
⊢
(∀𝑧 ∈
(𝐴 ∖ {𝐵})(𝑧 ∈ (𝐵(ball‘(abs ∘ − ))𝑦) → (𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) ↔ ∀𝑧 ∈ ((𝐵(ball‘(abs ∘ − ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥)) | 
| 113 |  | impexp 450 | . . . . . . . . . . 11
⊢ (((𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ (𝑧 ∈ 𝐴 → (𝑧 ≠ 𝐵 → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) | 
| 114 |  | eldifsn 4785 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵)) | 
| 115 | 114 | imbi1i 349 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ (𝐴 ∖ {𝐵}) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵) → ((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) | 
| 116 |  | impexp 450 | . . . . . . . . . . . 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 3088 | . . . . . . . . 9
⊢
(∀𝑧 ∈
(𝐴 ∖ {𝐵})((abs‘(𝑧 − 𝐵)) < 𝑦 → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)) | 
| 120 | 106, 112,
119 | 3bitr3g 313 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (∀𝑧 ∈
((𝐵(ball‘(abs ∘
− ))𝑦) ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) | 
| 121 | 78, 120 | bitrd 279 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) | 
| 122 | 121 | anassrs 467 | . . . . . 6
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦 ∈ ℝ+)
→ ((𝐹 “ ((𝐵(ball‘(abs ∘ −
))𝑦) ∩ (𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) | 
| 123 | 122 | rexbidva 3176 | . . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑥 ∈ ℝ+) →
(∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) | 
| 124 | 123 | ralbidva 3175 | . . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ (𝐹
“ ((𝐵(ball‘(abs
∘ − ))𝑦) ∩
(𝐴 ∖ {𝐵}))) ⊆ (𝐶(ball‘(abs ∘ − ))𝑥) ↔ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) | 
| 125 | 69, 124 | bitrd 279 | . . 3
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))) | 
| 126 | 125 | pm5.32da 579 | . 2
⊢ (𝜑 → ((𝐶 ∈ ℂ ∧ ∀𝑢 ∈
(TopOpen‘ℂfld)(𝐶 ∈ 𝑢 → ∃𝑣 ∈
(TopOpen‘ℂfld)(𝐵 ∈ 𝑣 ∧ (𝐹 “ (𝑣 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) | 
| 127 | 5, 126 | bitrd 279 | 1
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥)))) |