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 
|- ZZ e. ( Clsd ` J )

Proof

Step Hyp Ref Expression
1 zcld.1 
 |-  J = ( topGen ` ran (,) )
2 eliun 
 |-  ( y e. U_ x e. ZZ ( x (,) ( x + 1 ) ) <-> E. x e. ZZ y e. ( x (,) ( x + 1 ) ) )
3 elioore 
 |-  ( y e. ( x (,) ( x + 1 ) ) -> y e. RR )
4 3 adantl 
 |-  ( ( x e. ZZ /\ y e. ( x (,) ( x + 1 ) ) ) -> y e. RR )
5 eliooord 
 |-  ( y e. ( x (,) ( x + 1 ) ) -> ( x < y /\ y < ( x + 1 ) ) )
6 btwnnz 
 |-  ( ( x e. ZZ /\ x < y /\ y < ( x + 1 ) ) -> -. y e. ZZ )
7 6 3expb 
 |-  ( ( x e. ZZ /\ ( x < y /\ y < ( x + 1 ) ) ) -> -. y e. ZZ )
8 5 7 sylan2 
 |-  ( ( x e. ZZ /\ y e. ( x (,) ( x + 1 ) ) ) -> -. y e. ZZ )
9 4 8 eldifd 
 |-  ( ( x e. ZZ /\ y e. ( x (,) ( x + 1 ) ) ) -> y e. ( RR \ ZZ ) )
10 9 rexlimiva 
 |-  ( E. x e. ZZ y e. ( x (,) ( x + 1 ) ) -> y e. ( RR \ ZZ ) )
11 eldifi 
 |-  ( y e. ( RR \ ZZ ) -> y e. RR )
12 11 flcld 
 |-  ( y e. ( RR \ ZZ ) -> ( |_ ` y ) e. ZZ )
13 12 zred 
 |-  ( y e. ( RR \ ZZ ) -> ( |_ ` y ) e. RR )
14 flle 
 |-  ( y e. RR -> ( |_ ` y ) <_ y )
15 11 14 syl 
 |-  ( y e. ( RR \ ZZ ) -> ( |_ ` y ) <_ y )
16 eldifn 
 |-  ( y e. ( RR \ ZZ ) -> -. y e. ZZ )
17 nelne2 
 |-  ( ( ( |_ ` y ) e. ZZ /\ -. y e. ZZ ) -> ( |_ ` y ) =/= y )
18 12 16 17 syl2anc 
 |-  ( y e. ( RR \ ZZ ) -> ( |_ ` y ) =/= y )
19 18 necomd 
 |-  ( y e. ( RR \ ZZ ) -> y =/= ( |_ ` y ) )
20 13 11 15 19 leneltd 
 |-  ( y e. ( RR \ ZZ ) -> ( |_ ` y ) < y )
21 flltp1 
 |-  ( y e. RR -> y < ( ( |_ ` y ) + 1 ) )
22 11 21 syl 
 |-  ( y e. ( RR \ ZZ ) -> y < ( ( |_ ` y ) + 1 ) )
23 13 rexrd 
 |-  ( y e. ( RR \ ZZ ) -> ( |_ ` y ) e. RR* )
24 peano2re 
 |-  ( ( |_ ` y ) e. RR -> ( ( |_ ` y ) + 1 ) e. RR )
25 13 24 syl 
 |-  ( y e. ( RR \ ZZ ) -> ( ( |_ ` y ) + 1 ) e. RR )
26 25 rexrd 
 |-  ( y e. ( RR \ ZZ ) -> ( ( |_ ` y ) + 1 ) e. RR* )
27 elioo2 
 |-  ( ( ( |_ ` y ) e. RR* /\ ( ( |_ ` y ) + 1 ) e. RR* ) -> ( y e. ( ( |_ ` y ) (,) ( ( |_ ` y ) + 1 ) ) <-> ( y e. RR /\ ( |_ ` y ) < y /\ y < ( ( |_ ` y ) + 1 ) ) ) )
28 23 26 27 syl2anc 
 |-  ( y e. ( RR \ ZZ ) -> ( y e. ( ( |_ ` y ) (,) ( ( |_ ` y ) + 1 ) ) <-> ( y e. RR /\ ( |_ ` y ) < y /\ y < ( ( |_ ` y ) + 1 ) ) ) )
29 11 20 22 28 mpbir3and 
 |-  ( y e. ( RR \ ZZ ) -> y e. ( ( |_ ` 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 e. ( x (,) ( x + 1 ) ) <-> y e. ( ( |_ ` y ) (,) ( ( |_ ` y ) + 1 ) ) ) )
34 33 rspcev 
 |-  ( ( ( |_ ` y ) e. ZZ /\ y e. ( ( |_ ` y ) (,) ( ( |_ ` y ) + 1 ) ) ) -> E. x e. ZZ y e. ( x (,) ( x + 1 ) ) )
35 12 29 34 syl2anc 
 |-  ( y e. ( RR \ ZZ ) -> E. x e. ZZ y e. ( x (,) ( x + 1 ) ) )
36 10 35 impbii 
 |-  ( E. x e. ZZ y e. ( x (,) ( x + 1 ) ) <-> y e. ( RR \ ZZ ) )
37 2 36 bitri 
 |-  ( y e. U_ x e. ZZ ( x (,) ( x + 1 ) ) <-> y e. ( RR \ ZZ ) )
38 37 eqriv 
 |-  U_ x e. ZZ ( x (,) ( x + 1 ) ) = ( RR \ ZZ )
39 retop 
 |-  ( topGen ` ran (,) ) e. Top
40 1 39 eqeltri 
 |-  J e. Top
41 iooretop 
 |-  ( x (,) ( x + 1 ) ) e. ( topGen ` ran (,) )
42 41 1 eleqtrri 
 |-  ( x (,) ( x + 1 ) ) e. J
43 42 rgenw 
 |-  A. x e. ZZ ( x (,) ( x + 1 ) ) e. J
44 iunopn 
 |-  ( ( J e. Top /\ A. x e. ZZ ( x (,) ( x + 1 ) ) e. J ) -> U_ x e. ZZ ( x (,) ( x + 1 ) ) e. J )
45 40 43 44 mp2an 
 |-  U_ x e. ZZ ( x (,) ( x + 1 ) ) e. J
46 38 45 eqeltrri 
 |-  ( RR \ ZZ ) e. J
47 zssre 
 |-  ZZ C_ RR
48 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
49 1 unieqi 
 |-  U. J = U. ( topGen ` ran (,) )
50 48 49 eqtr4i 
 |-  RR = U. J
51 50 iscld2 
 |-  ( ( J e. Top /\ ZZ C_ RR ) -> ( ZZ e. ( Clsd ` J ) <-> ( RR \ ZZ ) e. J ) )
52 40 47 51 mp2an 
 |-  ( ZZ e. ( Clsd ` J ) <-> ( RR \ ZZ ) e. J )
53 46 52 mpbir 
 |-  ZZ e. ( Clsd ` J )