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 𝐽 = ( topGen ‘ ran (,) )
Assertion zcld ℤ ∈ ( Clsd ‘ 𝐽 )

Proof

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