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 β„€ ) = 𝒫 β„€