| Step | Hyp | Ref
| Expression |
| 1 | | eliun 4995 |
. . . . 5
⊢ (𝑦 ∈ ∪ 𝑥 ∈ ℤ (𝑥(,)(𝑥 + 1)) ↔ ∃𝑥 ∈ ℤ 𝑦 ∈ (𝑥(,)(𝑥 + 1))) |
| 2 | | elioore 13417 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑥(,)(𝑥 + 1)) → 𝑦 ∈ ℝ) |
| 3 | 2 | adantl 481 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ (𝑥(,)(𝑥 + 1))) → 𝑦 ∈ ℝ) |
| 4 | | eliooord 13446 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑥(,)(𝑥 + 1)) → (𝑥 < 𝑦 ∧ 𝑦 < (𝑥 + 1))) |
| 5 | | btwnnz 12694 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℤ ∧ 𝑥 < 𝑦 ∧ 𝑦 < (𝑥 + 1)) → ¬ 𝑦 ∈ ℤ) |
| 6 | 5 | 3expb 1121 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℤ ∧ (𝑥 < 𝑦 ∧ 𝑦 < (𝑥 + 1))) → ¬ 𝑦 ∈ ℤ) |
| 7 | 4, 6 | sylan2 593 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ (𝑥(,)(𝑥 + 1))) → ¬ 𝑦 ∈ ℤ) |
| 8 | 3, 7 | eldifd 3962 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ (𝑥(,)(𝑥 + 1))) → 𝑦 ∈ (ℝ ∖
ℤ)) |
| 9 | 8 | rexlimiva 3147 |
. . . . . 6
⊢
(∃𝑥 ∈
ℤ 𝑦 ∈ (𝑥(,)(𝑥 + 1)) → 𝑦 ∈ (ℝ ∖
ℤ)) |
| 10 | | eldifi 4131 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → 𝑦 ∈
ℝ) |
| 11 | 10 | flcld 13838 |
. . . . . . 7
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → (⌊‘𝑦) ∈ ℤ) |
| 12 | 11 | zred 12722 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → (⌊‘𝑦) ∈ ℝ) |
| 13 | | flle 13839 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ →
(⌊‘𝑦) ≤
𝑦) |
| 14 | 10, 13 | syl 17 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → (⌊‘𝑦) ≤ 𝑦) |
| 15 | | eldifn 4132 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → ¬ 𝑦
∈ ℤ) |
| 16 | | nelne2 3040 |
. . . . . . . . . . 11
⊢
(((⌊‘𝑦)
∈ ℤ ∧ ¬ 𝑦 ∈ ℤ) → (⌊‘𝑦) ≠ 𝑦) |
| 17 | 11, 15, 16 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → (⌊‘𝑦) ≠ 𝑦) |
| 18 | 17 | necomd 2996 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → 𝑦 ≠
(⌊‘𝑦)) |
| 19 | 12, 10, 14, 18 | leneltd 11415 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → (⌊‘𝑦) < 𝑦) |
| 20 | | flltp1 13840 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → 𝑦 < ((⌊‘𝑦) + 1)) |
| 21 | 10, 20 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → 𝑦 <
((⌊‘𝑦) +
1)) |
| 22 | 12 | rexrd 11311 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → (⌊‘𝑦) ∈
ℝ*) |
| 23 | | peano2re 11434 |
. . . . . . . . . . 11
⊢
((⌊‘𝑦)
∈ ℝ → ((⌊‘𝑦) + 1) ∈ ℝ) |
| 24 | 12, 23 | syl 17 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → ((⌊‘𝑦) + 1) ∈ ℝ) |
| 25 | 24 | rexrd 11311 |
. . . . . . . . 9
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → ((⌊‘𝑦) + 1) ∈
ℝ*) |
| 26 | | elioo2 13428 |
. . . . . . . . 9
⊢
(((⌊‘𝑦)
∈ ℝ* ∧ ((⌊‘𝑦) + 1) ∈ ℝ*) →
(𝑦 ∈
((⌊‘𝑦)(,)((⌊‘𝑦) + 1)) ↔ (𝑦 ∈ ℝ ∧ (⌊‘𝑦) < 𝑦 ∧ 𝑦 < ((⌊‘𝑦) + 1)))) |
| 27 | 22, 25, 26 | syl2anc 584 |
. . . . . . . 8
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → (𝑦 ∈
((⌊‘𝑦)(,)((⌊‘𝑦) + 1)) ↔ (𝑦 ∈ ℝ ∧ (⌊‘𝑦) < 𝑦 ∧ 𝑦 < ((⌊‘𝑦) + 1)))) |
| 28 | 10, 19, 21, 27 | mpbir3and 1343 |
. . . . . . 7
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → 𝑦 ∈
((⌊‘𝑦)(,)((⌊‘𝑦) + 1))) |
| 29 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = (⌊‘𝑦) → 𝑥 = (⌊‘𝑦)) |
| 30 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑥 = (⌊‘𝑦) → (𝑥 + 1) = ((⌊‘𝑦) + 1)) |
| 31 | 29, 30 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑥 = (⌊‘𝑦) → (𝑥(,)(𝑥 + 1)) = ((⌊‘𝑦)(,)((⌊‘𝑦) + 1))) |
| 32 | 31 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑥 = (⌊‘𝑦) → (𝑦 ∈ (𝑥(,)(𝑥 + 1)) ↔ 𝑦 ∈ ((⌊‘𝑦)(,)((⌊‘𝑦) + 1)))) |
| 33 | 32 | rspcev 3622 |
. . . . . . 7
⊢
(((⌊‘𝑦)
∈ ℤ ∧ 𝑦
∈ ((⌊‘𝑦)(,)((⌊‘𝑦) + 1))) → ∃𝑥 ∈ ℤ 𝑦 ∈ (𝑥(,)(𝑥 + 1))) |
| 34 | 11, 28, 33 | syl2anc 584 |
. . . . . 6
⊢ (𝑦 ∈ (ℝ ∖
ℤ) → ∃𝑥
∈ ℤ 𝑦 ∈
(𝑥(,)(𝑥 + 1))) |
| 35 | 9, 34 | impbii 209 |
. . . . 5
⊢
(∃𝑥 ∈
ℤ 𝑦 ∈ (𝑥(,)(𝑥 + 1)) ↔ 𝑦 ∈ (ℝ ∖
ℤ)) |
| 36 | 1, 35 | bitri 275 |
. . . 4
⊢ (𝑦 ∈ ∪ 𝑥 ∈ ℤ (𝑥(,)(𝑥 + 1)) ↔ 𝑦 ∈ (ℝ ∖
ℤ)) |
| 37 | 36 | eqriv 2734 |
. . 3
⊢ ∪ 𝑥 ∈ ℤ (𝑥(,)(𝑥 + 1)) = (ℝ ∖
ℤ) |
| 38 | | zcld.1 |
. . . . 5
⊢ 𝐽 = (topGen‘ran
(,)) |
| 39 | | retop 24782 |
. . . . 5
⊢
(topGen‘ran (,)) ∈ Top |
| 40 | 38, 39 | eqeltri 2837 |
. . . 4
⊢ 𝐽 ∈ Top |
| 41 | | iooretop 24786 |
. . . . . 6
⊢ (𝑥(,)(𝑥 + 1)) ∈ (topGen‘ran
(,)) |
| 42 | 41, 38 | eleqtrri 2840 |
. . . . 5
⊢ (𝑥(,)(𝑥 + 1)) ∈ 𝐽 |
| 43 | 42 | rgenw 3065 |
. . . 4
⊢
∀𝑥 ∈
ℤ (𝑥(,)(𝑥 + 1)) ∈ 𝐽 |
| 44 | | iunopn 22904 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ ℤ (𝑥(,)(𝑥 + 1)) ∈ 𝐽) → ∪
𝑥 ∈ ℤ (𝑥(,)(𝑥 + 1)) ∈ 𝐽) |
| 45 | 40, 43, 44 | mp2an 692 |
. . 3
⊢ ∪ 𝑥 ∈ ℤ (𝑥(,)(𝑥 + 1)) ∈ 𝐽 |
| 46 | 37, 45 | eqeltrri 2838 |
. 2
⊢ (ℝ
∖ ℤ) ∈ 𝐽 |
| 47 | | zssre 12620 |
. . 3
⊢ ℤ
⊆ ℝ |
| 48 | | uniretop 24783 |
. . . . 5
⊢ ℝ =
∪ (topGen‘ran (,)) |
| 49 | 38 | unieqi 4919 |
. . . . 5
⊢ ∪ 𝐽 =
∪ (topGen‘ran (,)) |
| 50 | 48, 49 | eqtr4i 2768 |
. . . 4
⊢ ℝ =
∪ 𝐽 |
| 51 | 50 | iscld2 23036 |
. . 3
⊢ ((𝐽 ∈ Top ∧ ℤ
⊆ ℝ) → (ℤ ∈ (Clsd‘𝐽) ↔ (ℝ ∖ ℤ) ∈
𝐽)) |
| 52 | 40, 47, 51 | mp2an 692 |
. 2
⊢ (ℤ
∈ (Clsd‘𝐽)
↔ (ℝ ∖ ℤ) ∈ 𝐽) |
| 53 | 46, 52 | mpbir 231 |
1
⊢ ℤ
∈ (Clsd‘𝐽) |