| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 2 | 1 | cnfldtop 24804 | . . . 4
⊢
(TopOpen‘ℂfld) ∈ Top | 
| 3 | 2 | a1i 11 | . . 3
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈ Top) | 
| 4 |  | islpcn.s | . . 3
⊢ (𝜑 → 𝑆 ⊆ ℂ) | 
| 5 |  | islpcn.p | . . 3
⊢ (𝜑 → 𝑃 ∈ ℂ) | 
| 6 |  | unicntop 24806 | . . . 4
⊢ ℂ =
∪
(TopOpen‘ℂfld) | 
| 7 | 6 | islp2 23153 | . . 3
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ⊆ ℂ ∧ 𝑃 ∈ ℂ) → (𝑃 ∈
((limPt‘(TopOpen‘ℂfld))‘𝑆) ↔ ∀𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅)) | 
| 8 | 3, 4, 5, 7 | syl3anc 1373 | . 2
⊢ (𝜑 → (𝑃 ∈
((limPt‘(TopOpen‘ℂfld))‘𝑆) ↔ ∀𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅)) | 
| 9 |  | cnxmet 24793 | . . . . . . . . . . 11
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) | 
| 10 | 9 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (abs
∘ − ) ∈ (∞Met‘ℂ)) | 
| 11 | 5 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑃 ∈
ℂ) | 
| 12 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
ℝ+) | 
| 13 | 1 | cnfldtopn 24802 | . . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) | 
| 14 | 13 | blnei 24515 | . . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑒 ∈ ℝ+) → (𝑃(ball‘(abs ∘ −
))𝑒) ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})) | 
| 15 | 10, 11, 12, 14 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (𝑃(ball‘(abs ∘ −
))𝑒) ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})) | 
| 16 | 15 | adantlr 715 | . . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) ∧ 𝑒 ∈ ℝ+) → (𝑃(ball‘(abs ∘ −
))𝑒) ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})) | 
| 17 |  | simplr 769 | . . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) ∧ 𝑒 ∈ ℝ+) →
∀𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) | 
| 18 |  | ineq1 4213 | . . . . . . . . . 10
⊢ (𝑛 = (𝑃(ball‘(abs ∘ − ))𝑒) → (𝑛 ∩ (𝑆 ∖ {𝑃})) = ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) | 
| 19 | 18 | neeq1d 3000 | . . . . . . . . 9
⊢ (𝑛 = (𝑃(ball‘(abs ∘ − ))𝑒) → ((𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅ ↔ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃})) ≠ ∅)) | 
| 20 | 19 | rspcva 3620 | . . . . . . . 8
⊢ (((𝑃(ball‘(abs ∘ −
))𝑒) ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃}) ∧ ∀𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) → ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃})) ≠ ∅) | 
| 21 | 16, 17, 20 | syl2anc 584 | . . . . . . 7
⊢ (((𝜑 ∧ ∀𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) ∧ 𝑒 ∈ ℝ+) → ((𝑃(ball‘(abs ∘ −
))𝑒) ∩ (𝑆 ∖ {𝑃})) ≠ ∅) | 
| 22 |  | n0 4353 | . . . . . . 7
⊢ (((𝑃(ball‘(abs ∘ −
))𝑒) ∩ (𝑆 ∖ {𝑃})) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) | 
| 23 | 21, 22 | sylib 218 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) ∧ 𝑒 ∈ ℝ+) →
∃𝑥 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) | 
| 24 |  | elinel2 4202 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃})) → 𝑥 ∈ (𝑆 ∖ {𝑃})) | 
| 25 | 24 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → 𝑥 ∈ (𝑆 ∖ {𝑃})) | 
| 26 | 4 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → 𝑆 ⊆ ℂ) | 
| 27 | 24 | eldifad 3963 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃})) → 𝑥 ∈ 𝑆) | 
| 28 | 27 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → 𝑥 ∈ 𝑆) | 
| 29 | 26, 28 | sseldd 3984 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → 𝑥 ∈ ℂ) | 
| 30 | 5 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → 𝑃 ∈ ℂ) | 
| 31 | 29, 30 | abssubd 15492 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → (abs‘(𝑥 − 𝑃)) = (abs‘(𝑃 − 𝑥))) | 
| 32 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢ (abs
∘ − ) = (abs ∘ − ) | 
| 33 | 32 | cnmetdval 24791 | . . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑃(abs ∘ − )𝑥) = (abs‘(𝑃 − 𝑥))) | 
| 34 | 30, 29, 33 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → (𝑃(abs ∘ − )𝑥) = (abs‘(𝑃 − 𝑥))) | 
| 35 | 31, 34 | eqtr4d 2780 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → (abs‘(𝑥 − 𝑃)) = (𝑃(abs ∘ − )𝑥)) | 
| 36 | 35 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → (abs‘(𝑥 − 𝑃)) = (𝑃(abs ∘ − )𝑥)) | 
| 37 |  | elinel1 4201 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃})) → 𝑥 ∈ (𝑃(ball‘(abs ∘ − ))𝑒)) | 
| 38 | 37 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → 𝑥 ∈ (𝑃(ball‘(abs ∘ − ))𝑒)) | 
| 39 | 9 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → (abs ∘ − ) ∈
(∞Met‘ℂ)) | 
| 40 | 11 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → 𝑃 ∈ ℂ) | 
| 41 |  | rpxr 13044 | . . . . . . . . . . . . . . 15
⊢ (𝑒 ∈ ℝ+
→ 𝑒 ∈
ℝ*) | 
| 42 | 41 | ad2antlr 727 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → 𝑒 ∈ ℝ*) | 
| 43 |  | elbl 24398 | . . . . . . . . . . . . . 14
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ ∧ 𝑒 ∈ ℝ*) → (𝑥 ∈ (𝑃(ball‘(abs ∘ − ))𝑒) ↔ (𝑥 ∈ ℂ ∧ (𝑃(abs ∘ − )𝑥) < 𝑒))) | 
| 44 | 39, 40, 42, 43 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → (𝑥 ∈ (𝑃(ball‘(abs ∘ − ))𝑒) ↔ (𝑥 ∈ ℂ ∧ (𝑃(abs ∘ − )𝑥) < 𝑒))) | 
| 45 | 38, 44 | mpbid 232 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → (𝑥 ∈ ℂ ∧ (𝑃(abs ∘ − )𝑥) < 𝑒)) | 
| 46 | 45 | simprd 495 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → (𝑃(abs ∘ − )𝑥) < 𝑒) | 
| 47 | 36, 46 | eqbrtrd 5165 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → (abs‘(𝑥 − 𝑃)) < 𝑒) | 
| 48 | 25, 47 | jca 511 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃}))) → (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) | 
| 49 | 48 | ex 412 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → (𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃})) → (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒))) | 
| 50 | 49 | adantlr 715 | . . . . . . 7
⊢ (((𝜑 ∧ ∀𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) ∧ 𝑒 ∈ ℝ+) → (𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃})) → (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒))) | 
| 51 | 50 | eximdv 1917 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) ∧ 𝑒 ∈ ℝ+) →
(∃𝑥 𝑥 ∈ ((𝑃(ball‘(abs ∘ − ))𝑒) ∩ (𝑆 ∖ {𝑃})) → ∃𝑥(𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒))) | 
| 52 | 23, 51 | mpd 15 | . . . . 5
⊢ (((𝜑 ∧ ∀𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) ∧ 𝑒 ∈ ℝ+) →
∃𝑥(𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) | 
| 53 |  | df-rex 3071 | . . . . 5
⊢
(∃𝑥 ∈
(𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒 ↔ ∃𝑥(𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) | 
| 54 | 52, 53 | sylibr 234 | . . . 4
⊢ (((𝜑 ∧ ∀𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) ∧ 𝑒 ∈ ℝ+) →
∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) | 
| 55 | 54 | ralrimiva 3146 | . . 3
⊢ ((𝜑 ∧ ∀𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) → ∀𝑒 ∈ ℝ+
∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) | 
| 56 | 9 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) | 
| 57 | 13 | neibl 24514 | . . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑃 ∈ ℂ) → (𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃}) ↔ (𝑛 ⊆ ℂ ∧ ∃𝑒 ∈ ℝ+
(𝑃(ball‘(abs ∘
− ))𝑒) ⊆ 𝑛))) | 
| 58 | 56, 5, 57 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃}) ↔ (𝑛 ⊆ ℂ ∧ ∃𝑒 ∈ ℝ+
(𝑃(ball‘(abs ∘
− ))𝑒) ⊆ 𝑛))) | 
| 59 | 58 | simplbda 499 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})) → ∃𝑒 ∈ ℝ+ (𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛) | 
| 60 | 59 | adantlr 715 | . . . . 5
⊢ (((𝜑 ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ 𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})) → ∃𝑒 ∈ ℝ+ (𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛) | 
| 61 |  | nfv 1914 | . . . . . . . 8
⊢
Ⅎ𝑒𝜑 | 
| 62 |  | nfra1 3284 | . . . . . . . 8
⊢
Ⅎ𝑒∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒 | 
| 63 | 61, 62 | nfan 1899 | . . . . . . 7
⊢
Ⅎ𝑒(𝜑 ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) | 
| 64 |  | nfv 1914 | . . . . . . 7
⊢
Ⅎ𝑒 𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃}) | 
| 65 | 63, 64 | nfan 1899 | . . . . . 6
⊢
Ⅎ𝑒((𝜑 ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ 𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})) | 
| 66 |  | nfv 1914 | . . . . . 6
⊢
Ⅎ𝑒(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅ | 
| 67 |  | simp1l 1198 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ 𝑒 ∈ ℝ+ ∧ (𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛) → 𝜑) | 
| 68 |  | simp2 1138 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ 𝑒 ∈ ℝ+ ∧ (𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛) → 𝑒 ∈ ℝ+) | 
| 69 | 67, 68 | jca 511 | . . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ 𝑒 ∈ ℝ+ ∧ (𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛) → (𝜑 ∧ 𝑒 ∈
ℝ+)) | 
| 70 |  | rspa 3248 | . . . . . . . . . . 11
⊢
((∀𝑒 ∈
ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒 ∧ 𝑒 ∈ ℝ+) →
∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) | 
| 71 | 70 | adantll 714 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ 𝑒 ∈ ℝ+) →
∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) | 
| 72 | 71 | 3adant3 1133 | . . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ 𝑒 ∈ ℝ+ ∧ (𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛) → ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) | 
| 73 |  | simp3 1139 | . . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ 𝑒 ∈ ℝ+ ∧ (𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛) → (𝑃(ball‘(abs ∘ − ))𝑒) ⊆ 𝑛) | 
| 74 | 53 | biimpi 216 | . . . . . . . . . . . 12
⊢
(∃𝑥 ∈
(𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒 → ∃𝑥(𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) | 
| 75 | 74 | ad2antlr 727 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧
∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ (𝑃(ball‘(abs ∘ − ))𝑒) ⊆ 𝑛) → ∃𝑥(𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) | 
| 76 |  | nfv 1914 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝜑 ∧ 𝑒 ∈ ℝ+) | 
| 77 |  | nfre1 3285 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒 | 
| 78 | 76, 77 | nfan 1899 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥((𝜑 ∧ 𝑒 ∈ ℝ+) ∧
∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) | 
| 79 |  | nfv 1914 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛 | 
| 80 | 78, 79 | nfan 1899 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥(((𝜑 ∧ 𝑒 ∈ ℝ+) ∧
∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ (𝑃(ball‘(abs ∘ − ))𝑒) ⊆ 𝑛) | 
| 81 |  | simplr 769 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛) ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → (𝑃(ball‘(abs ∘ − ))𝑒) ⊆ 𝑛) | 
| 82 | 4 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑆 ∖ {𝑃})) → 𝑆 ⊆ ℂ) | 
| 83 |  | eldifi 4131 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ (𝑆 ∖ {𝑃}) → 𝑥 ∈ 𝑆) | 
| 84 | 83 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑆 ∖ {𝑃})) → 𝑥 ∈ 𝑆) | 
| 85 | 82, 84 | sseldd 3984 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑆 ∖ {𝑃})) → 𝑥 ∈ ℂ) | 
| 86 | 85 | adantrr 717 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → 𝑥 ∈ ℂ) | 
| 87 | 5 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑆 ∖ {𝑃})) → 𝑃 ∈ ℂ) | 
| 88 | 87, 85, 33 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑆 ∖ {𝑃})) → (𝑃(abs ∘ − )𝑥) = (abs‘(𝑃 − 𝑥))) | 
| 89 | 87, 85 | abssubd 15492 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑆 ∖ {𝑃})) → (abs‘(𝑃 − 𝑥)) = (abs‘(𝑥 − 𝑃))) | 
| 90 | 88, 89 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑆 ∖ {𝑃})) → (𝑃(abs ∘ − )𝑥) = (abs‘(𝑥 − 𝑃))) | 
| 91 | 90 | adantrr 717 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → (𝑃(abs ∘ − )𝑥) = (abs‘(𝑥 − 𝑃))) | 
| 92 |  | simprr 773 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → (abs‘(𝑥 − 𝑃)) < 𝑒) | 
| 93 | 91, 92 | eqbrtrd 5165 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → (𝑃(abs ∘ − )𝑥) < 𝑒) | 
| 94 | 86, 93 | jca 511 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → (𝑥 ∈ ℂ ∧ (𝑃(abs ∘ − )𝑥) < 𝑒)) | 
| 95 | 94 | adantlr 715 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → (𝑥 ∈ ℂ ∧ (𝑃(abs ∘ − )𝑥) < 𝑒)) | 
| 96 | 9 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → (abs ∘ − ) ∈
(∞Met‘ℂ)) | 
| 97 | 11 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → 𝑃 ∈ ℂ) | 
| 98 | 41 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → 𝑒 ∈ ℝ*) | 
| 99 | 96, 97, 98, 43 | syl3anc 1373 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → (𝑥 ∈ (𝑃(ball‘(abs ∘ − ))𝑒) ↔ (𝑥 ∈ ℂ ∧ (𝑃(abs ∘ − )𝑥) < 𝑒))) | 
| 100 | 95, 99 | mpbird 257 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → 𝑥 ∈ (𝑃(ball‘(abs ∘ − ))𝑒)) | 
| 101 | 100 | adantlr 715 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛) ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → 𝑥 ∈ (𝑃(ball‘(abs ∘ − ))𝑒)) | 
| 102 | 81, 101 | sseldd 3984 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛) ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → 𝑥 ∈ 𝑛) | 
| 103 |  | simprl 771 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛) ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → 𝑥 ∈ (𝑆 ∖ {𝑃})) | 
| 104 | 102, 103 | elind 4200 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛) ∧ (𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒)) → 𝑥 ∈ (𝑛 ∩ (𝑆 ∖ {𝑃}))) | 
| 105 | 104 | ex 412 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛) → ((𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒) → 𝑥 ∈ (𝑛 ∩ (𝑆 ∖ {𝑃})))) | 
| 106 | 105 | adantlr 715 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧
∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ (𝑃(ball‘(abs ∘ − ))𝑒) ⊆ 𝑛) → ((𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒) → 𝑥 ∈ (𝑛 ∩ (𝑆 ∖ {𝑃})))) | 
| 107 | 80, 106 | eximd 2216 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧
∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ (𝑃(ball‘(abs ∘ − ))𝑒) ⊆ 𝑛) → (∃𝑥(𝑥 ∈ (𝑆 ∖ {𝑃}) ∧ (abs‘(𝑥 − 𝑃)) < 𝑒) → ∃𝑥 𝑥 ∈ (𝑛 ∩ (𝑆 ∖ {𝑃})))) | 
| 108 | 75, 107 | mpd 15 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧
∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ (𝑃(ball‘(abs ∘ − ))𝑒) ⊆ 𝑛) → ∃𝑥 𝑥 ∈ (𝑛 ∩ (𝑆 ∖ {𝑃}))) | 
| 109 |  | n0 4353 | . . . . . . . . . 10
⊢ ((𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝑛 ∩ (𝑆 ∖ {𝑃}))) | 
| 110 | 108, 109 | sylibr 234 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧
∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ (𝑃(ball‘(abs ∘ − ))𝑒) ⊆ 𝑛) → (𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) | 
| 111 | 69, 72, 73, 110 | syl21anc 838 | . . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ 𝑒 ∈ ℝ+ ∧ (𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛) → (𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) | 
| 112 | 111 | 3exp 1120 | . . . . . . 7
⊢ ((𝜑 ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) → (𝑒 ∈ ℝ+ → ((𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛 → (𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅))) | 
| 113 | 112 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ 𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})) → (𝑒 ∈ ℝ+ → ((𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛 → (𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅))) | 
| 114 | 65, 66, 113 | rexlimd 3266 | . . . . 5
⊢ (((𝜑 ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ 𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})) → (∃𝑒 ∈ ℝ+ (𝑃(ball‘(abs ∘ −
))𝑒) ⊆ 𝑛 → (𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅)) | 
| 115 | 60, 114 | mpd 15 | . . . 4
⊢ (((𝜑 ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) ∧ 𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})) → (𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) | 
| 116 | 115 | ralrimiva 3146 | . . 3
⊢ ((𝜑 ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒) → ∀𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅) | 
| 117 | 55, 116 | impbida 801 | . 2
⊢ (𝜑 → (∀𝑛 ∈
((nei‘(TopOpen‘ℂfld))‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅ ↔ ∀𝑒 ∈ ℝ+
∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒)) | 
| 118 | 8, 117 | bitrd 279 | 1
⊢ (𝜑 → (𝑃 ∈
((limPt‘(TopOpen‘ℂfld))‘𝑆) ↔ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ (𝑆 ∖ {𝑃})(abs‘(𝑥 − 𝑃)) < 𝑒)) |