Metamath Proof Explorer


Theorem zcld

Description: The integers are a closed set in the topology on RR . (Contributed by Mario Carneiro, 17-Feb-2015)

Ref Expression
Hypothesis zcld.1 J=topGenran.
Assertion zcld ClsdJ

Proof

Step Hyp Ref Expression
1 zcld.1 J=topGenran.
2 eliun yxxx+1xyxx+1
3 elioore yxx+1y
4 3 adantl xyxx+1y
5 eliooord yxx+1x<yy<x+1
6 btwnnz xx<yy<x+1¬y
7 6 3expb xx<yy<x+1¬y
8 5 7 sylan2 xyxx+1¬y
9 4 8 eldifd xyxx+1y
10 9 rexlimiva xyxx+1y
11 eldifi yy
12 11 flcld yy
13 12 zred yy
14 flle yyy
15 11 14 syl yyy
16 eldifn y¬y
17 nelne2 y¬yyy
18 12 16 17 syl2anc yyy
19 18 necomd yyy
20 13 11 15 19 leneltd yy<y
21 flltp1 yy<y+1
22 11 21 syl yy<y+1
23 13 rexrd yy*
24 peano2re yy+1
25 13 24 syl yy+1
26 25 rexrd yy+1*
27 elioo2 y*y+1*yyy+1yy<yy<y+1
28 23 26 27 syl2anc yyyy+1yy<yy<y+1
29 11 20 22 28 mpbir3and yyyy+1
30 id x=yx=y
31 oveq1 x=yx+1=y+1
32 30 31 oveq12d x=yxx+1=yy+1
33 32 eleq2d x=yyxx+1yyy+1
34 33 rspcev yyyy+1xyxx+1
35 12 29 34 syl2anc yxyxx+1
36 10 35 impbii xyxx+1y
37 2 36 bitri yxxx+1y
38 37 eqriv xxx+1=
39 retop topGenran.Top
40 1 39 eqeltri JTop
41 iooretop xx+1topGenran.
42 41 1 eleqtrri xx+1J
43 42 rgenw xxx+1J
44 iunopn JTopxxx+1Jxxx+1J
45 40 43 44 mp2an xxx+1J
46 38 45 eqeltrri J
47 zssre
48 uniretop =topGenran.
49 1 unieqi J=topGenran.
50 48 49 eqtr4i =J
51 50 iscld2 JTopClsdJJ
52 40 47 51 mp2an ClsdJJ
53 46 52 mpbir ClsdJ