Step | Hyp | Ref
| Expression |
1 | | eliun 4745 |
. . . . 5
⊢ (𝑦 ∈ ∪ 𝑥 ∈ ℤ (𝑥(,)(𝑥 + 1)) ↔ ∃𝑥 ∈ ℤ 𝑦 ∈ (𝑥(,)(𝑥 + 1))) |
2 | | elioore 12494 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑥(,)(𝑥 + 1)) → 𝑦 ∈ ℝ) |
3 | 2 | adantl 475 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ (𝑥(,)(𝑥 + 1))) → 𝑦 ∈ ℝ) |
4 | | eliooord 12522 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑥(,)(𝑥 + 1)) → (𝑥 < 𝑦 ∧ 𝑦 < (𝑥 + 1))) |
5 | | btwnnz 11782 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℤ ∧ 𝑥 < 𝑦 ∧ 𝑦 < (𝑥 + 1)) → ¬ 𝑦 ∈ ℤ) |
6 | 5 | 3expb 1155 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℤ ∧ (𝑥 < 𝑦 ∧ 𝑦 < (𝑥 + 1))) → ¬ 𝑦 ∈ ℤ) |
7 | 4, 6 | sylan2 588 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ (𝑥(,)(𝑥 + 1))) → ¬ 𝑦 ∈ ℤ) |
8 | 3, 7 | eldifd 3810 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ (𝑥(,)(𝑥 + 1))) → 𝑦 ∈ (ℝ ∖
ℤ)) |
9 | 8 | rexlimiva 3238 |
. . . . . 6
⊢
(∃𝑥 ∈
ℤ 𝑦 ∈ (𝑥(,)(𝑥 + 1)) → 𝑦 ∈ (ℝ ∖
ℤ)) |
10 | | eldifi 3960 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → 𝑦 ∈
ℝ) |
11 | 10 | flcld 12895 |
. . . . . . 7
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → (⌊‘𝑦) ∈ ℤ) |
12 | | flle 12896 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ →
(⌊‘𝑦) ≤
𝑦) |
13 | 10, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → (⌊‘𝑦) ≤ 𝑦) |
14 | | eldifn 3961 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → ¬ 𝑦
∈ ℤ) |
15 | | nelne2 3097 |
. . . . . . . . . . 11
⊢
(((⌊‘𝑦)
∈ ℤ ∧ ¬ 𝑦 ∈ ℤ) → (⌊‘𝑦) ≠ 𝑦) |
16 | 11, 14, 15 | syl2anc 581 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → (⌊‘𝑦) ≠ 𝑦) |
17 | 16 | necomd 3055 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → 𝑦 ≠
(⌊‘𝑦)) |
18 | 11 | zred 11811 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → (⌊‘𝑦) ∈ ℝ) |
19 | 18, 10 | ltlend 10502 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → ((⌊‘𝑦) < 𝑦 ↔ ((⌊‘𝑦) ≤ 𝑦 ∧ 𝑦 ≠ (⌊‘𝑦)))) |
20 | 13, 17, 19 | mpbir2and 706 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → (⌊‘𝑦) < 𝑦) |
21 | | flltp1 12897 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → 𝑦 < ((⌊‘𝑦) + 1)) |
22 | 10, 21 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → 𝑦 <
((⌊‘𝑦) +
1)) |
23 | 18 | rexrd 10407 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → (⌊‘𝑦) ∈
ℝ*) |
24 | | peano2re 10529 |
. . . . . . . . . . 11
⊢
((⌊‘𝑦)
∈ ℝ → ((⌊‘𝑦) + 1) ∈ ℝ) |
25 | 18, 24 | syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → ((⌊‘𝑦) + 1) ∈ ℝ) |
26 | 25 | rexrd 10407 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → ((⌊‘𝑦) + 1) ∈
ℝ*) |
27 | | elioo2 12505 |
. . . . . . . . 9
⊢
(((⌊‘𝑦)
∈ ℝ* ∧ ((⌊‘𝑦) + 1) ∈ ℝ*) →
(𝑦 ∈
((⌊‘𝑦)(,)((⌊‘𝑦) + 1)) ↔ (𝑦 ∈ ℝ ∧ (⌊‘𝑦) < 𝑦 ∧ 𝑦 < ((⌊‘𝑦) + 1)))) |
28 | 23, 26, 27 | syl2anc 581 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → (𝑦 ∈
((⌊‘𝑦)(,)((⌊‘𝑦) + 1)) ↔ (𝑦 ∈ ℝ ∧ (⌊‘𝑦) < 𝑦 ∧ 𝑦 < ((⌊‘𝑦) + 1)))) |
29 | 10, 20, 22, 28 | mpbir3and 1448 |
. . . . . . 7
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → 𝑦 ∈
((⌊‘𝑦)(,)((⌊‘𝑦) + 1))) |
30 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = (⌊‘𝑦) → 𝑥 = (⌊‘𝑦)) |
31 | | oveq1 6913 |
. . . . . . . . . 10
⊢ (𝑥 = (⌊‘𝑦) → (𝑥 + 1) = ((⌊‘𝑦) + 1)) |
32 | 30, 31 | oveq12d 6924 |
. . . . . . . . 9
⊢ (𝑥 = (⌊‘𝑦) → (𝑥(,)(𝑥 + 1)) = ((⌊‘𝑦)(,)((⌊‘𝑦) + 1))) |
33 | 32 | eleq2d 2893 |
. . . . . . . 8
⊢ (𝑥 = (⌊‘𝑦) → (𝑦 ∈ (𝑥(,)(𝑥 + 1)) ↔ 𝑦 ∈ ((⌊‘𝑦)(,)((⌊‘𝑦) + 1)))) |
34 | 33 | rspcev 3527 |
. . . . . . 7
⊢
(((⌊‘𝑦)
∈ ℤ ∧ 𝑦
∈ ((⌊‘𝑦)(,)((⌊‘𝑦) + 1))) → ∃𝑥 ∈ ℤ 𝑦 ∈ (𝑥(,)(𝑥 + 1))) |
35 | 11, 29, 34 | syl2anc 581 |
. . . . . 6
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → ∃𝑥
∈ ℤ 𝑦 ∈
(𝑥(,)(𝑥 + 1))) |
36 | 9, 35 | impbii 201 |
. . . . 5
⊢
(∃𝑥 ∈
ℤ 𝑦 ∈ (𝑥(,)(𝑥 + 1)) ↔ 𝑦 ∈ (ℝ ∖
ℤ)) |
37 | 1, 36 | bitri 267 |
. . . 4
⊢ (𝑦 ∈ ∪ 𝑥 ∈ ℤ (𝑥(,)(𝑥 + 1)) ↔ 𝑦 ∈ (ℝ ∖
ℤ)) |
38 | 37 | eqriv 2823 |
. . 3
⊢ ∪ 𝑥 ∈ ℤ (𝑥(,)(𝑥 + 1)) = (ℝ ∖
ℤ) |
39 | | zcld.1 |
. . . . 5
⊢ 𝐽 = (topGen‘ran
(,)) |
40 | | retop 22936 |
. . . . 5
⊢
(topGen‘ran (,)) ∈ Top |
41 | 39, 40 | eqeltri 2903 |
. . . 4
⊢ 𝐽 ∈ Top |
42 | | iooretop 22940 |
. . . . . 6
⊢ (𝑥(,)(𝑥 + 1)) ∈ (topGen‘ran
(,)) |
43 | 42, 39 | eleqtrri 2906 |
. . . . 5
⊢ (𝑥(,)(𝑥 + 1)) ∈ 𝐽 |
44 | 43 | rgenw 3134 |
. . . 4
⊢
∀𝑥 ∈
ℤ (𝑥(,)(𝑥 + 1)) ∈ 𝐽 |
45 | | iunopn 21074 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ ℤ (𝑥(,)(𝑥 + 1)) ∈ 𝐽) → ∪
𝑥 ∈ ℤ (𝑥(,)(𝑥 + 1)) ∈ 𝐽) |
46 | 41, 44, 45 | mp2an 685 |
. . 3
⊢ ∪ 𝑥 ∈ ℤ (𝑥(,)(𝑥 + 1)) ∈ 𝐽 |
47 | 38, 46 | eqeltrri 2904 |
. 2
⊢ (ℝ
∖ ℤ) ∈ 𝐽 |
48 | | zssre 11712 |
. . 3
⊢ ℤ
⊆ ℝ |
49 | | uniretop 22937 |
. . . . 5
⊢ ℝ =
∪ (topGen‘ran (,)) |
50 | 39 | unieqi 4668 |
. . . . 5
⊢ ∪ 𝐽 =
∪ (topGen‘ran (,)) |
51 | 49, 50 | eqtr4i 2853 |
. . . 4
⊢ ℝ =
∪ 𝐽 |
52 | 51 | iscld2 21204 |
. . 3
⊢ ((𝐽 ∈ Top ∧ ℤ
⊆ ℝ) → (ℤ ∈ (Clsd‘𝐽) ↔ (ℝ ∖ ℤ) ∈
𝐽)) |
53 | 41, 48, 52 | mp2an 685 |
. 2
⊢ (ℤ
∈ (Clsd‘𝐽)
↔ (ℝ ∖ ℤ) ∈ 𝐽) |
54 | 47, 53 | mpbir 223 |
1
⊢ ℤ
∈ (Clsd‘𝐽) |