| Step | Hyp | Ref
| Expression |
| 1 | | restsspw 17476 |
. 2
⊢ (𝐽 ↾t ℤ)
⊆ 𝒫 ℤ |
| 2 | | elpwi 4607 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝒫 ℤ →
𝑥 ⊆
ℤ) |
| 3 | 2 | sselda 3983 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → 𝑦 ∈ ℤ) |
| 4 | 3 | zcnd 12723 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → 𝑦 ∈ ℂ) |
| 5 | | cnxmet 24793 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 6 | | 1xr 11320 |
. . . . . . . 8
⊢ 1 ∈
ℝ* |
| 7 | | recld2.1 |
. . . . . . . . . 10
⊢ 𝐽 =
(TopOpen‘ℂfld) |
| 8 | 7 | cnfldtopn 24802 |
. . . . . . . . 9
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
| 9 | 8 | blopn 24513 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ ℂ ∧ 1 ∈
ℝ*) → (𝑦(ball‘(abs ∘ − ))1) ∈
𝐽) |
| 10 | 5, 6, 9 | mp3an13 1454 |
. . . . . . 7
⊢ (𝑦 ∈ ℂ → (𝑦(ball‘(abs ∘ −
))1) ∈ 𝐽) |
| 11 | 7 | cnfldtop 24804 |
. . . . . . . 8
⊢ 𝐽 ∈ Top |
| 12 | | zex 12622 |
. . . . . . . 8
⊢ ℤ
∈ V |
| 13 | | elrestr 17473 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ ℤ ∈
V ∧ (𝑦(ball‘(abs
∘ − ))1) ∈ 𝐽) → ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) ∈ (𝐽
↾t ℤ)) |
| 14 | 11, 12, 13 | mp3an12 1453 |
. . . . . . 7
⊢ ((𝑦(ball‘(abs ∘ −
))1) ∈ 𝐽 →
((𝑦(ball‘(abs ∘
− ))1) ∩ ℤ) ∈ (𝐽 ↾t
ℤ)) |
| 15 | 4, 10, 14 | 3syl 18 |
. . . . . 6
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) ∈ (𝐽
↾t ℤ)) |
| 16 | | 1rp 13038 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
| 17 | | blcntr 24423 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ ℂ ∧ 1 ∈
ℝ+) → 𝑦 ∈ (𝑦(ball‘(abs ∘ −
))1)) |
| 18 | 5, 16, 17 | mp3an13 1454 |
. . . . . . . 8
⊢ (𝑦 ∈ ℂ → 𝑦 ∈ (𝑦(ball‘(abs ∘ −
))1)) |
| 19 | 4, 18 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → 𝑦 ∈ (𝑦(ball‘(abs ∘ −
))1)) |
| 20 | 19, 3 | elind 4200 |
. . . . . 6
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → 𝑦 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) |
| 21 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑦 ∈
ℂ) |
| 22 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑧 ∈
((𝑦(ball‘(abs ∘
− ))1) ∩ ℤ)) |
| 23 | 22 | elin2d 4205 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑧 ∈
ℤ) |
| 24 | 23 | zcnd 12723 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑧 ∈
ℂ) |
| 25 | 3 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑦 ∈
ℤ) |
| 26 | 25, 23 | zsubcld 12727 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → (𝑦 −
𝑧) ∈
ℤ) |
| 27 | 26 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → (𝑦 −
𝑧) ∈
ℂ) |
| 28 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (abs
∘ − ) = (abs ∘ − ) |
| 29 | 28 | cnmetdval 24791 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦(abs ∘ − )𝑧) = (abs‘(𝑦 − 𝑧))) |
| 30 | 21, 24, 29 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → (𝑦(abs
∘ − )𝑧) =
(abs‘(𝑦 − 𝑧))) |
| 31 | 22 | elin1d 4204 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑧 ∈
(𝑦(ball‘(abs ∘
− ))1)) |
| 32 | | elbl2 24400 |
. . . . . . . . . . . . . . . 16
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (𝑦(ball‘(abs ∘ − ))1) ↔
(𝑦(abs ∘ −
)𝑧) <
1)) |
| 33 | 5, 6, 32 | mpanl12 702 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑧 ∈ (𝑦(ball‘(abs ∘ − ))1) ↔
(𝑦(abs ∘ −
)𝑧) <
1)) |
| 34 | 21, 24, 33 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → (𝑧 ∈
(𝑦(ball‘(abs ∘
− ))1) ↔ (𝑦(abs
∘ − )𝑧) <
1)) |
| 35 | 31, 34 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → (𝑦(abs
∘ − )𝑧) <
1) |
| 36 | 30, 35 | eqbrtrrd 5167 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → (abs‘(𝑦 − 𝑧)) < 1) |
| 37 | | nn0abscl 15351 |
. . . . . . . . . . . . 13
⊢ ((𝑦 − 𝑧) ∈ ℤ → (abs‘(𝑦 − 𝑧)) ∈
ℕ0) |
| 38 | | nn0lt10b 12680 |
. . . . . . . . . . . . 13
⊢
((abs‘(𝑦
− 𝑧)) ∈
ℕ0 → ((abs‘(𝑦 − 𝑧)) < 1 ↔ (abs‘(𝑦 − 𝑧)) = 0)) |
| 39 | 26, 37, 38 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → ((abs‘(𝑦 − 𝑧)) < 1 ↔ (abs‘(𝑦 − 𝑧)) = 0)) |
| 40 | 36, 39 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → (abs‘(𝑦 − 𝑧)) = 0) |
| 41 | 27, 40 | abs00d 15485 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → (𝑦 −
𝑧) = 0) |
| 42 | 21, 24, 41 | subeq0d 11628 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑦 = 𝑧) |
| 43 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑦 ∈
𝑥) |
| 44 | 42, 43 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑧 ∈
𝑥) |
| 45 | 44 | ex 412 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → (𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) → 𝑧 ∈
𝑥)) |
| 46 | 45 | ssrdv 3989 |
. . . . . 6
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) ⊆ 𝑥) |
| 47 | | eleq2 2830 |
. . . . . . . 8
⊢ (𝑧 = ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) → (𝑦 ∈
𝑧 ↔ 𝑦 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ))) |
| 48 | | sseq1 4009 |
. . . . . . . 8
⊢ (𝑧 = ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) → (𝑧 ⊆
𝑥 ↔ ((𝑦(ball‘(abs ∘ −
))1) ∩ ℤ) ⊆ 𝑥)) |
| 49 | 47, 48 | anbi12d 632 |
. . . . . . 7
⊢ (𝑧 = ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) → ((𝑦 ∈
𝑧 ∧ 𝑧 ⊆ 𝑥) ↔ (𝑦 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) ∧ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) ⊆ 𝑥))) |
| 50 | 49 | rspcev 3622 |
. . . . . 6
⊢ ((((𝑦(ball‘(abs ∘ −
))1) ∩ ℤ) ∈ (𝐽 ↾t ℤ) ∧ (𝑦 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) ∧ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) ⊆ 𝑥)) →
∃𝑧 ∈ (𝐽 ↾t
ℤ)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥)) |
| 51 | 15, 20, 46, 50 | syl12anc 837 |
. . . . 5
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → ∃𝑧 ∈ (𝐽 ↾t ℤ)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥)) |
| 52 | 51 | ralrimiva 3146 |
. . . 4
⊢ (𝑥 ∈ 𝒫 ℤ →
∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (𝐽 ↾t ℤ)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥)) |
| 53 | | resttop 23168 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ ℤ ∈
V) → (𝐽
↾t ℤ) ∈ Top) |
| 54 | 11, 12, 53 | mp2an 692 |
. . . . 5
⊢ (𝐽 ↾t ℤ)
∈ Top |
| 55 | | eltop2 22982 |
. . . . 5
⊢ ((𝐽 ↾t ℤ)
∈ Top → (𝑥 ∈
(𝐽 ↾t
ℤ) ↔ ∀𝑦
∈ 𝑥 ∃𝑧 ∈ (𝐽 ↾t ℤ)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))) |
| 56 | 54, 55 | ax-mp 5 |
. . . 4
⊢ (𝑥 ∈ (𝐽 ↾t ℤ) ↔
∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (𝐽 ↾t ℤ)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥)) |
| 57 | 52, 56 | sylibr 234 |
. . 3
⊢ (𝑥 ∈ 𝒫 ℤ →
𝑥 ∈ (𝐽 ↾t
ℤ)) |
| 58 | 57 | ssriv 3987 |
. 2
⊢ 𝒫
ℤ ⊆ (𝐽
↾t ℤ) |
| 59 | 1, 58 | eqssi 4000 |
1
⊢ (𝐽 ↾t ℤ) =
𝒫 ℤ |