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 = topGen ran .
Assertion zcld Clsd J

Proof

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