Metamath Proof Explorer

Theorem zdis

Description: The integers are a discrete set in the topology on CC . (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Hypothesis recld2.1 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion zdis ( 𝐽 ↾t ℤ ) = 𝒫 ℤ

Proof

Step Hyp Ref Expression
1 recld2.1 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 restsspw ⊢ ( 𝐽 ↾t ℤ ) ⊆ 𝒫 ℤ
3 elpwi ⊢ ( 𝑥 ∈ 𝒫 ℤ → 𝑥 ⊆ ℤ )
4 3 sselda ⊢ ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ℤ )
5 4 zcnd ⊢ ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ℂ )
6 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
7 1xr ⊢ 1 ∈ ℝ*
8 1 cnfldtopn ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
9 8 blopn ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑦 ∈ ℂ ∧ 1 ∈ ℝ* ) → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∈ 𝐽 )
10 6 7 9 mp3an13 ⊢ ( 𝑦 ∈ ℂ → ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∈ 𝐽 )
11 1 cnfldtop ⊢ 𝐽 ∈ Top
12 zex ⊢ ℤ ∈ V
13 elrestr ⊢ ( ( 𝐽 ∈ Top ∧ ℤ ∈ V ∧ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∈ 𝐽 ) → ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ∈ ( 𝐽 ↾t ℤ ) )
14 11 12 13 mp3an12 ⊢ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∈ 𝐽 → ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ∈ ( 𝐽 ↾t ℤ ) )
15 5 10 14 3syl ⊢ ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ∈ ( 𝐽 ↾t ℤ ) )
16 1rp ⊢ 1 ∈ ℝ+
17 blcntr ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑦 ∈ ℂ ∧ 1 ∈ ℝ+ ) → 𝑦 ∈ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) )
18 6 16 17 mp3an13 ⊢ ( 𝑦 ∈ ℂ → 𝑦 ∈ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) )
19 5 18 syl ⊢ ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) )
20 19 4 elind ⊢ ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) )
21 5 adantr ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → 𝑦 ∈ ℂ )
22 simpr ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) )
23 22 elin2d ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → 𝑧 ∈ ℤ )
24 23 zcnd ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → 𝑧 ∈ ℂ )
25 4 adantr ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → 𝑦 ∈ ℤ )
26 25 23 zsubcld ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → ( 𝑦 − 𝑧 ) ∈ ℤ )
27 26 zcnd ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → ( 𝑦 − 𝑧 ) ∈ ℂ )
28 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
29 28 cnmetdval ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 ( abs ∘ − ) 𝑧 ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
30 21 24 29 syl2anc ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → ( 𝑦 ( abs ∘ − ) 𝑧 ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
31 22 elin1d ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → 𝑧 ∈ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) )
32 elbl2 ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 1 ∈ ℝ* ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( 𝑧 ∈ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑦 ( abs ∘ − ) 𝑧 ) < 1 ) )
33 6 7 32 mpanl12 ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑧 ∈ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑦 ( abs ∘ − ) 𝑧 ) < 1 ) )
34 21 24 33 syl2anc ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → ( 𝑧 ∈ ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑦 ( abs ∘ − ) 𝑧 ) < 1 ) )
35 31 34 mpbid ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → ( 𝑦 ( abs ∘ − ) 𝑧 ) < 1 )
36 30 35 eqbrtrrd ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → ( abs ‘ ( 𝑦 − 𝑧 ) ) < 1 )
37 nn0abscl ⊢ ( ( 𝑦 − 𝑧 ) ∈ ℤ → ( abs ‘ ( 𝑦 − 𝑧 ) ) ∈ ℕ0 )
38 nn0lt10b ⊢ ( ( abs ‘ ( 𝑦 − 𝑧 ) ) ∈ ℕ0 → ( ( abs ‘ ( 𝑦 − 𝑧 ) ) < 1 ↔ ( abs ‘ ( 𝑦 − 𝑧 ) ) = 0 ) )
39 26 37 38 3syl ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → ( ( abs ‘ ( 𝑦 − 𝑧 ) ) < 1 ↔ ( abs ‘ ( 𝑦 − 𝑧 ) ) = 0 ) )
40 36 39 mpbid ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → ( abs ‘ ( 𝑦 − 𝑧 ) ) = 0 )
41 27 40 abs00d ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → ( 𝑦 − 𝑧 ) = 0 )
42 21 24 41 subeq0d ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → 𝑦 = 𝑧 )
43 simplr ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → 𝑦 ∈ 𝑥 )
44 42 43 eqeltrrd ⊢ ( ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) → 𝑧 ∈ 𝑥 )
45 44 ex ⊢ ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) → ( 𝑧 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) → 𝑧 ∈ 𝑥 ) )
46 45 ssrdv ⊢ ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ⊆ 𝑥 )
47 eleq2 ⊢ ( 𝑧 = ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ) )
48 sseq1 ⊢ ( 𝑧 = ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) → ( 𝑧 ⊆ 𝑥 ↔ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ⊆ 𝑥 ) )
49 47 48 anbi12d ⊢ ( 𝑧 = ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ↔ ( 𝑦 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ∧ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ⊆ 𝑥 ) ) )
50 49 rspcev ⊢ ( ( ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ∈ ( 𝐽 ↾t ℤ ) ∧ ( 𝑦 ∈ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ∧ ( ( 𝑦 ( ball ‘ ( abs ∘ − ) ) 1 ) ∩ ℤ ) ⊆ 𝑥 ) ) → ∃ 𝑧 ∈ ( 𝐽 ↾t ℤ ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
51 15 20 46 50 syl12anc ⊢ ( ( 𝑥 ∈ 𝒫 ℤ ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑧 ∈ ( 𝐽 ↾t ℤ ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
52 51 ralrimiva ⊢ ( 𝑥 ∈ 𝒫 ℤ → ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ ( 𝐽 ↾t ℤ ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
53 resttop ⊢ ( ( 𝐽 ∈ Top ∧ ℤ ∈ V ) → ( 𝐽 ↾t ℤ ) ∈ Top )
54 11 12 53 mp2an ⊢ ( 𝐽 ↾t ℤ ) ∈ Top
55 eltop2 ⊢ ( ( 𝐽 ↾t ℤ ) ∈ Top → ( 𝑥 ∈ ( 𝐽 ↾t ℤ ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ ( 𝐽 ↾t ℤ ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) )
56 54 55 ax-mp ⊢ ( 𝑥 ∈ ( 𝐽 ↾t ℤ ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ ( 𝐽 ↾t ℤ ) ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) )
57 52 56 sylibr ⊢ ( 𝑥 ∈ 𝒫 ℤ → 𝑥 ∈ ( 𝐽 ↾t ℤ ) )
58 57 ssriv ⊢ 𝒫 ℤ ⊆ ( 𝐽 ↾t ℤ )
59 2 58 eqssi ⊢ ( 𝐽 ↾t ℤ ) = 𝒫 ℤ