Step | Hyp | Ref
| Expression |
1 | | restsspw 17152 |
. 2
⊢ (𝐽 ↾t ℤ)
⊆ 𝒫 ℤ |
2 | | elpwi 4542 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝒫 ℤ →
𝑥 ⊆
ℤ) |
3 | 2 | sselda 3920 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → 𝑦 ∈ ℤ) |
4 | 3 | zcnd 12437 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → 𝑦 ∈ ℂ) |
5 | | cnxmet 23946 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
6 | | 1xr 11044 |
. . . . . . . 8
⊢ 1 ∈
ℝ* |
7 | | recld2.1 |
. . . . . . . . . 10
⊢ 𝐽 =
(TopOpen‘ℂfld) |
8 | 7 | cnfldtopn 23955 |
. . . . . . . . 9
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
9 | 8 | blopn 23666 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ ℂ ∧ 1 ∈
ℝ*) → (𝑦(ball‘(abs ∘ − ))1) ∈
𝐽) |
10 | 5, 6, 9 | mp3an13 1451 |
. . . . . . 7
⊢ (𝑦 ∈ ℂ → (𝑦(ball‘(abs ∘ −
))1) ∈ 𝐽) |
11 | 7 | cnfldtop 23957 |
. . . . . . . 8
⊢ 𝐽 ∈ Top |
12 | | zex 12338 |
. . . . . . . 8
⊢ ℤ
∈ V |
13 | | elrestr 17149 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ ℤ ∈
V ∧ (𝑦(ball‘(abs
∘ − ))1) ∈ 𝐽) → ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) ∈ (𝐽
↾t ℤ)) |
14 | 11, 12, 13 | mp3an12 1450 |
. . . . . . 7
⊢ ((𝑦(ball‘(abs ∘ −
))1) ∈ 𝐽 →
((𝑦(ball‘(abs ∘
− ))1) ∩ ℤ) ∈ (𝐽 ↾t
ℤ)) |
15 | 4, 10, 14 | 3syl 18 |
. . . . . 6
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) ∈ (𝐽
↾t ℤ)) |
16 | | 1rp 12744 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
17 | | blcntr 23576 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ ℂ ∧ 1 ∈
ℝ+) → 𝑦 ∈ (𝑦(ball‘(abs ∘ −
))1)) |
18 | 5, 16, 17 | mp3an13 1451 |
. . . . . . . 8
⊢ (𝑦 ∈ ℂ → 𝑦 ∈ (𝑦(ball‘(abs ∘ −
))1)) |
19 | 4, 18 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → 𝑦 ∈ (𝑦(ball‘(abs ∘ −
))1)) |
20 | 19, 3 | elind 4127 |
. . . . . 6
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → 𝑦 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) |
21 | 4 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑦 ∈
ℂ) |
22 | | simpr 485 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑧 ∈
((𝑦(ball‘(abs ∘
− ))1) ∩ ℤ)) |
23 | 22 | elin2d 4132 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑧 ∈
ℤ) |
24 | 23 | zcnd 12437 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑧 ∈
ℂ) |
25 | 3 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑦 ∈
ℤ) |
26 | 25, 23 | zsubcld 12441 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → (𝑦 −
𝑧) ∈
ℤ) |
27 | 26 | zcnd 12437 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → (𝑦 −
𝑧) ∈
ℂ) |
28 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (abs
∘ − ) = (abs ∘ − ) |
29 | 28 | cnmetdval 23944 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦(abs ∘ − )𝑧) = (abs‘(𝑦 − 𝑧))) |
30 | 21, 24, 29 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → (𝑦(abs
∘ − )𝑧) =
(abs‘(𝑦 − 𝑧))) |
31 | 22 | elin1d 4131 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑧 ∈
(𝑦(ball‘(abs ∘
− ))1)) |
32 | | elbl2 23553 |
. . . . . . . . . . . . . . . 16
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (𝑦(ball‘(abs ∘ − ))1) ↔
(𝑦(abs ∘ −
)𝑧) <
1)) |
33 | 5, 6, 32 | mpanl12 699 |
. . . . . . . . . . . . . . 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 231 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → (𝑦(abs
∘ − )𝑧) <
1) |
36 | 30, 35 | eqbrtrrd 5097 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → (abs‘(𝑦 − 𝑧)) < 1) |
37 | | nn0abscl 15034 |
. . . . . . . . . . . . 13
⊢ ((𝑦 − 𝑧) ∈ ℤ → (abs‘(𝑦 − 𝑧)) ∈
ℕ0) |
38 | | nn0lt10b 12392 |
. . . . . . . . . . . . 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 231 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → (abs‘(𝑦 − 𝑧)) = 0) |
41 | 27, 40 | abs00d 15168 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → (𝑦 −
𝑧) = 0) |
42 | 21, 24, 41 | subeq0d 11350 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑦 = 𝑧) |
43 | | simplr 766 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑦 ∈
𝑥) |
44 | 42, 43 | eqeltrrd 2840 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) ∧ 𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ)) → 𝑧 ∈
𝑥) |
45 | 44 | ex 413 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → (𝑧 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) → 𝑧 ∈
𝑥)) |
46 | 45 | ssrdv 3926 |
. . . . . 6
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) ⊆ 𝑥) |
47 | | eleq2 2827 |
. . . . . . . 8
⊢ (𝑧 = ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) → (𝑦 ∈
𝑧 ↔ 𝑦 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ))) |
48 | | sseq1 3945 |
. . . . . . . 8
⊢ (𝑧 = ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) → (𝑧 ⊆
𝑥 ↔ ((𝑦(ball‘(abs ∘ −
))1) ∩ ℤ) ⊆ 𝑥)) |
49 | 47, 48 | anbi12d 631 |
. . . . . . 7
⊢ (𝑧 = ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) → ((𝑦 ∈
𝑧 ∧ 𝑧 ⊆ 𝑥) ↔ (𝑦 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) ∧ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) ⊆ 𝑥))) |
50 | 49 | rspcev 3559 |
. . . . . 6
⊢ ((((𝑦(ball‘(abs ∘ −
))1) ∩ ℤ) ∈ (𝐽 ↾t ℤ) ∧ (𝑦 ∈ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) ∧ ((𝑦(ball‘(abs ∘ − ))1) ∩
ℤ) ⊆ 𝑥)) →
∃𝑧 ∈ (𝐽 ↾t
ℤ)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥)) |
51 | 15, 20, 46, 50 | syl12anc 834 |
. . . . 5
⊢ ((𝑥 ∈ 𝒫 ℤ ∧
𝑦 ∈ 𝑥) → ∃𝑧 ∈ (𝐽 ↾t ℤ)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥)) |
52 | 51 | ralrimiva 3108 |
. . . 4
⊢ (𝑥 ∈ 𝒫 ℤ →
∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (𝐽 ↾t ℤ)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥)) |
53 | | resttop 22321 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ ℤ ∈
V) → (𝐽
↾t ℤ) ∈ Top) |
54 | 11, 12, 53 | mp2an 689 |
. . . . 5
⊢ (𝐽 ↾t ℤ)
∈ Top |
55 | | eltop2 22135 |
. . . . 5
⊢ ((𝐽 ↾t ℤ)
∈ Top → (𝑥 ∈
(𝐽 ↾t
ℤ) ↔ ∀𝑦
∈ 𝑥 ∃𝑧 ∈ (𝐽 ↾t ℤ)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))) |
56 | 54, 55 | ax-mp 5 |
. . . 4
⊢ (𝑥 ∈ (𝐽 ↾t ℤ) ↔
∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (𝐽 ↾t ℤ)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥)) |
57 | 52, 56 | sylibr 233 |
. . 3
⊢ (𝑥 ∈ 𝒫 ℤ →
𝑥 ∈ (𝐽 ↾t
ℤ)) |
58 | 57 | ssriv 3924 |
. 2
⊢ 𝒫
ℤ ⊆ (𝐽
↾t ℤ) |
59 | 1, 58 | eqssi 3936 |
1
⊢ (𝐽 ↾t ℤ) =
𝒫 ℤ |