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 ‘ 𝐽 ) |