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 
|- J = ( TopOpen ` CCfld )
Assertion zdis 
|- ( J |`t ZZ ) = ~P ZZ

Proof

Step Hyp Ref Expression
1 recld2.1 
 |-  J = ( TopOpen ` CCfld )
2 restsspw 
 |-  ( J |`t ZZ ) C_ ~P ZZ
3 elpwi 
 |-  ( x e. ~P ZZ -> x C_ ZZ )
4 3 sselda 
 |-  ( ( x e. ~P ZZ /\ y e. x ) -> y e. ZZ )
5 4 zcnd 
 |-  ( ( x e. ~P ZZ /\ y e. x ) -> y e. CC )
6 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
7 1xr 
 |-  1 e. RR*
8 1 cnfldtopn 
 |-  J = ( MetOpen ` ( abs o. - ) )
9 8 blopn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ y e. CC /\ 1 e. RR* ) -> ( y ( ball ` ( abs o. - ) ) 1 ) e. J )
10 6 7 9 mp3an13 
 |-  ( y e. CC -> ( y ( ball ` ( abs o. - ) ) 1 ) e. J )
11 1 cnfldtop 
 |-  J e. Top
12 zex 
 |-  ZZ e. _V
13 elrestr 
 |-  ( ( J e. Top /\ ZZ e. _V /\ ( y ( ball ` ( abs o. - ) ) 1 ) e. J ) -> ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) e. ( J |`t ZZ ) )
14 11 12 13 mp3an12 
 |-  ( ( y ( ball ` ( abs o. - ) ) 1 ) e. J -> ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) e. ( J |`t ZZ ) )
15 5 10 14 3syl 
 |-  ( ( x e. ~P ZZ /\ y e. x ) -> ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) e. ( J |`t ZZ ) )
16 1rp 
 |-  1 e. RR+
17 blcntr 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ y e. CC /\ 1 e. RR+ ) -> y e. ( y ( ball ` ( abs o. - ) ) 1 ) )
18 6 16 17 mp3an13 
 |-  ( y e. CC -> y e. ( y ( ball ` ( abs o. - ) ) 1 ) )
19 5 18 syl 
 |-  ( ( x e. ~P ZZ /\ y e. x ) -> y e. ( y ( ball ` ( abs o. - ) ) 1 ) )
20 19 4 elind 
 |-  ( ( x e. ~P ZZ /\ y e. x ) -> y e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) )
21 5 adantr 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> y e. CC )
22 simpr 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) )
23 22 elin2d 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> z e. ZZ )
24 23 zcnd 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> z e. CC )
25 4 adantr 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> y e. ZZ )
26 25 23 zsubcld 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> ( y - z ) e. ZZ )
27 26 zcnd 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> ( y - z ) e. CC )
28 eqid 
 |-  ( abs o. - ) = ( abs o. - )
29 28 cnmetdval 
 |-  ( ( y e. CC /\ z e. CC ) -> ( y ( abs o. - ) z ) = ( abs ` ( y - z ) ) )
30 21 24 29 syl2anc 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> ( y ( abs o. - ) z ) = ( abs ` ( y - z ) ) )
31 22 elin1d 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> z e. ( y ( ball ` ( abs o. - ) ) 1 ) )
32 elbl2 
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 1 e. RR* ) /\ ( y e. CC /\ z e. CC ) ) -> ( z e. ( y ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) z ) < 1 ) )
33 6 7 32 mpanl12 
 |-  ( ( y e. CC /\ z e. CC ) -> ( z e. ( y ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) z ) < 1 ) )
34 21 24 33 syl2anc 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> ( z e. ( y ( ball ` ( abs o. - ) ) 1 ) <-> ( y ( abs o. - ) z ) < 1 ) )
35 31 34 mpbid 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> ( y ( abs o. - ) z ) < 1 )
36 30 35 eqbrtrrd 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> ( abs ` ( y - z ) ) < 1 )
37 nn0abscl 
 |-  ( ( y - z ) e. ZZ -> ( abs ` ( y - z ) ) e. NN0 )
38 nn0lt10b 
 |-  ( ( abs ` ( y - z ) ) e. NN0 -> ( ( abs ` ( y - z ) ) < 1 <-> ( abs ` ( y - z ) ) = 0 ) )
39 26 37 38 3syl 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> ( ( abs ` ( y - z ) ) < 1 <-> ( abs ` ( y - z ) ) = 0 ) )
40 36 39 mpbid 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> ( abs ` ( y - z ) ) = 0 )
41 27 40 abs00d 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> ( y - z ) = 0 )
42 21 24 41 subeq0d 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> y = z )
43 simplr 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> y e. x )
44 42 43 eqeltrrd 
 |-  ( ( ( x e. ~P ZZ /\ y e. x ) /\ z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) -> z e. x )
45 44 ex 
 |-  ( ( x e. ~P ZZ /\ y e. x ) -> ( z e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) -> z e. x ) )
46 45 ssrdv 
 |-  ( ( x e. ~P ZZ /\ y e. x ) -> ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) C_ x )
47 eleq2 
 |-  ( z = ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) -> ( y e. z <-> y e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) ) )
48 sseq1 
 |-  ( z = ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) -> ( z C_ x <-> ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) C_ x ) )
49 47 48 anbi12d 
 |-  ( z = ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) -> ( ( y e. z /\ z C_ x ) <-> ( y e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) /\ ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) C_ x ) ) )
50 49 rspcev 
 |-  ( ( ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) e. ( J |`t ZZ ) /\ ( y e. ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) /\ ( ( y ( ball ` ( abs o. - ) ) 1 ) i^i ZZ ) C_ x ) ) -> E. z e. ( J |`t ZZ ) ( y e. z /\ z C_ x ) )
51 15 20 46 50 syl12anc 
 |-  ( ( x e. ~P ZZ /\ y e. x ) -> E. z e. ( J |`t ZZ ) ( y e. z /\ z C_ x ) )
52 51 ralrimiva 
 |-  ( x e. ~P ZZ -> A. y e. x E. z e. ( J |`t ZZ ) ( y e. z /\ z C_ x ) )
53 resttop 
 |-  ( ( J e. Top /\ ZZ e. _V ) -> ( J |`t ZZ ) e. Top )
54 11 12 53 mp2an 
 |-  ( J |`t ZZ ) e. Top
55 eltop2 
 |-  ( ( J |`t ZZ ) e. Top -> ( x e. ( J |`t ZZ ) <-> A. y e. x E. z e. ( J |`t ZZ ) ( y e. z /\ z C_ x ) ) )
56 54 55 ax-mp 
 |-  ( x e. ( J |`t ZZ ) <-> A. y e. x E. z e. ( J |`t ZZ ) ( y e. z /\ z C_ x ) )
57 52 56 sylibr 
 |-  ( x e. ~P ZZ -> x e. ( J |`t ZZ ) )
58 57 ssriv 
 |-  ~P ZZ C_ ( J |`t ZZ )
59 2 58 eqssi 
 |-  ( J |`t ZZ ) = ~P ZZ