| Step | Hyp | Ref
| Expression |
| 1 | | cnxmet 24793 |
. . . . . . 7
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 2 | | reperflem.3 |
. . . . . . . 8
⊢ 𝑆 ⊆
ℂ |
| 3 | 2 | sseli 3979 |
. . . . . . 7
⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ ℂ) |
| 4 | | recld2.1 |
. . . . . . . . 9
⊢ 𝐽 =
(TopOpen‘ℂfld) |
| 5 | 4 | cnfldtopn 24802 |
. . . . . . . 8
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
| 6 | 5 | neibl 24514 |
. . . . . . 7
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑢 ∈ ℂ) → (𝑛 ∈ ((nei‘𝐽)‘{𝑢}) ↔ (𝑛 ⊆ ℂ ∧ ∃𝑟 ∈ ℝ+
(𝑢(ball‘(abs ∘
− ))𝑟) ⊆ 𝑛))) |
| 7 | 1, 3, 6 | sylancr 587 |
. . . . . 6
⊢ (𝑢 ∈ 𝑆 → (𝑛 ∈ ((nei‘𝐽)‘{𝑢}) ↔ (𝑛 ⊆ ℂ ∧ ∃𝑟 ∈ ℝ+
(𝑢(ball‘(abs ∘
− ))𝑟) ⊆ 𝑛))) |
| 8 | | ssrin 4242 |
. . . . . . . . 9
⊢ ((𝑢(ball‘(abs ∘ −
))𝑟) ⊆ 𝑛 → ((𝑢(ball‘(abs ∘ − ))𝑟) ∩ (𝑆 ∖ {𝑢})) ⊆ (𝑛 ∩ (𝑆 ∖ {𝑢}))) |
| 9 | | reperflem.2 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ ℝ) → (𝑢 + 𝑣) ∈ 𝑆) |
| 10 | 9 | ralrimiva 3146 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ 𝑆 → ∀𝑣 ∈ ℝ (𝑢 + 𝑣) ∈ 𝑆) |
| 11 | | rpre 13043 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
| 12 | 11 | rehalfcld 12513 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ) |
| 13 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = (𝑟 / 2) → (𝑢 + 𝑣) = (𝑢 + (𝑟 / 2))) |
| 14 | 13 | eleq1d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = (𝑟 / 2) → ((𝑢 + 𝑣) ∈ 𝑆 ↔ (𝑢 + (𝑟 / 2)) ∈ 𝑆)) |
| 15 | 14 | rspccva 3621 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑣 ∈
ℝ (𝑢 + 𝑣) ∈ 𝑆 ∧ (𝑟 / 2) ∈ ℝ) → (𝑢 + (𝑟 / 2)) ∈ 𝑆) |
| 16 | 10, 12, 15 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑢 + (𝑟 / 2)) ∈ 𝑆) |
| 17 | 2, 16 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑢 + (𝑟 / 2)) ∈ ℂ) |
| 18 | 3 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → 𝑢 ∈
ℂ) |
| 19 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (abs
∘ − ) = (abs ∘ − ) |
| 20 | 19 | cnmetdval 24791 |
. . . . . . . . . . . . . 14
⊢ (((𝑢 + (𝑟 / 2)) ∈ ℂ ∧ 𝑢 ∈ ℂ) → ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) = (abs‘((𝑢 + (𝑟 / 2)) − 𝑢))) |
| 21 | 17, 18, 20 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) = (abs‘((𝑢 + (𝑟 / 2)) − 𝑢))) |
| 22 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ+) |
| 23 | 22 | rphalfcld 13089 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℝ+) |
| 24 | 23 | rpcnd 13079 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℂ) |
| 25 | 18, 24 | pncan2d 11622 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2)) − 𝑢) = (𝑟 / 2)) |
| 26 | 25 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) →
(abs‘((𝑢 + (𝑟 / 2)) − 𝑢)) = (abs‘(𝑟 / 2))) |
| 27 | 23 | rpred 13077 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℝ) |
| 28 | 23 | rpge0d 13081 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → 0 ≤
(𝑟 / 2)) |
| 29 | 27, 28 | absidd 15461 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) →
(abs‘(𝑟 / 2)) =
(𝑟 / 2)) |
| 30 | 21, 26, 29 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) = (𝑟 / 2)) |
| 31 | | rphalflt 13064 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) < 𝑟) |
| 32 | 31 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) < 𝑟) |
| 33 | 30, 32 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) < 𝑟) |
| 34 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (abs
∘ − ) ∈ (∞Met‘ℂ)) |
| 35 | | rpxr 13044 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
| 36 | 35 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ*) |
| 37 | | elbl3 24402 |
. . . . . . . . . . . 12
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝑢 ∈ ℂ ∧ (𝑢 + (𝑟 / 2)) ∈ ℂ)) → ((𝑢 + (𝑟 / 2)) ∈ (𝑢(ball‘(abs ∘ − ))𝑟) ↔ ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) < 𝑟)) |
| 38 | 34, 36, 18, 17, 37 | syl22anc 839 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2)) ∈ (𝑢(ball‘(abs ∘ − ))𝑟) ↔ ((𝑢 + (𝑟 / 2))(abs ∘ − )𝑢) < 𝑟)) |
| 39 | 33, 38 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑢 + (𝑟 / 2)) ∈ (𝑢(ball‘(abs ∘ − ))𝑟)) |
| 40 | 23 | rpne0d 13082 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ≠ 0) |
| 41 | 25, 40 | eqnetrd 3008 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢 + (𝑟 / 2)) − 𝑢) ≠ 0) |
| 42 | 17, 18, 41 | subne0ad 11631 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑢 + (𝑟 / 2)) ≠ 𝑢) |
| 43 | | eldifsn 4786 |
. . . . . . . . . . 11
⊢ ((𝑢 + (𝑟 / 2)) ∈ (𝑆 ∖ {𝑢}) ↔ ((𝑢 + (𝑟 / 2)) ∈ 𝑆 ∧ (𝑢 + (𝑟 / 2)) ≠ 𝑢)) |
| 44 | 16, 42, 43 | sylanbrc 583 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → (𝑢 + (𝑟 / 2)) ∈ (𝑆 ∖ {𝑢})) |
| 45 | | inelcm 4465 |
. . . . . . . . . 10
⊢ (((𝑢 + (𝑟 / 2)) ∈ (𝑢(ball‘(abs ∘ − ))𝑟) ∧ (𝑢 + (𝑟 / 2)) ∈ (𝑆 ∖ {𝑢})) → ((𝑢(ball‘(abs ∘ − ))𝑟) ∩ (𝑆 ∖ {𝑢})) ≠ ∅) |
| 46 | 39, 44, 45 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢(ball‘(abs ∘ −
))𝑟) ∩ (𝑆 ∖ {𝑢})) ≠ ∅) |
| 47 | | ssn0 4404 |
. . . . . . . . . 10
⊢ ((((𝑢(ball‘(abs ∘ −
))𝑟) ∩ (𝑆 ∖ {𝑢})) ⊆ (𝑛 ∩ (𝑆 ∖ {𝑢})) ∧ ((𝑢(ball‘(abs ∘ − ))𝑟) ∩ (𝑆 ∖ {𝑢})) ≠ ∅) → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅) |
| 48 | 47 | ex 412 |
. . . . . . . . 9
⊢ (((𝑢(ball‘(abs ∘ −
))𝑟) ∩ (𝑆 ∖ {𝑢})) ⊆ (𝑛 ∩ (𝑆 ∖ {𝑢})) → (((𝑢(ball‘(abs ∘ − ))𝑟) ∩ (𝑆 ∖ {𝑢})) ≠ ∅ → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
| 49 | 8, 46, 48 | syl2imc 41 |
. . . . . . . 8
⊢ ((𝑢 ∈ 𝑆 ∧ 𝑟 ∈ ℝ+) → ((𝑢(ball‘(abs ∘ −
))𝑟) ⊆ 𝑛 → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
| 50 | 49 | rexlimdva 3155 |
. . . . . . 7
⊢ (𝑢 ∈ 𝑆 → (∃𝑟 ∈ ℝ+ (𝑢(ball‘(abs ∘ −
))𝑟) ⊆ 𝑛 → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
| 51 | 50 | adantld 490 |
. . . . . 6
⊢ (𝑢 ∈ 𝑆 → ((𝑛 ⊆ ℂ ∧ ∃𝑟 ∈ ℝ+
(𝑢(ball‘(abs ∘
− ))𝑟) ⊆ 𝑛) → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
| 52 | 7, 51 | sylbid 240 |
. . . . 5
⊢ (𝑢 ∈ 𝑆 → (𝑛 ∈ ((nei‘𝐽)‘{𝑢}) → (𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
| 53 | 52 | ralrimiv 3145 |
. . . 4
⊢ (𝑢 ∈ 𝑆 → ∀𝑛 ∈ ((nei‘𝐽)‘{𝑢})(𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅) |
| 54 | 4 | cnfldtop 24804 |
. . . . 5
⊢ 𝐽 ∈ Top |
| 55 | 4 | cnfldtopon 24803 |
. . . . . . 7
⊢ 𝐽 ∈
(TopOn‘ℂ) |
| 56 | 55 | toponunii 22922 |
. . . . . 6
⊢ ℂ =
∪ 𝐽 |
| 57 | 56 | islp2 23153 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ℂ ∧ 𝑢 ∈ ℂ) → (𝑢 ∈ ((limPt‘𝐽)‘𝑆) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑢})(𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
| 58 | 54, 2, 3, 57 | mp3an12i 1467 |
. . . 4
⊢ (𝑢 ∈ 𝑆 → (𝑢 ∈ ((limPt‘𝐽)‘𝑆) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑢})(𝑛 ∩ (𝑆 ∖ {𝑢})) ≠ ∅)) |
| 59 | 53, 58 | mpbird 257 |
. . 3
⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ ((limPt‘𝐽)‘𝑆)) |
| 60 | 59 | ssriv 3987 |
. 2
⊢ 𝑆 ⊆ ((limPt‘𝐽)‘𝑆) |
| 61 | | eqid 2737 |
. . . 4
⊢ (𝐽 ↾t 𝑆) = (𝐽 ↾t 𝑆) |
| 62 | 56, 61 | restperf 23192 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ ℂ) → ((𝐽 ↾t 𝑆) ∈ Perf ↔ 𝑆 ⊆ ((limPt‘𝐽)‘𝑆))) |
| 63 | 54, 2, 62 | mp2an 692 |
. 2
⊢ ((𝐽 ↾t 𝑆) ∈ Perf ↔ 𝑆 ⊆ ((limPt‘𝐽)‘𝑆)) |
| 64 | 60, 63 | mpbir 231 |
1
⊢ (𝐽 ↾t 𝑆) ∈ Perf |