Step | Hyp | Ref
| Expression |
1 | | rexr 10768 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
2 | | peano2re 10894 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ) |
3 | | rexr 10768 |
. . . . . . . 8
⊢ ((𝑥 + 1) ∈ ℝ →
(𝑥 + 1) ∈
ℝ*) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ*) |
5 | | ltp1 11561 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → 𝑥 < (𝑥 + 1)) |
6 | | lbico1 12878 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ (𝑥 + 1) ∈
ℝ* ∧ 𝑥
< (𝑥 + 1)) → 𝑥 ∈ (𝑥[,)(𝑥 + 1))) |
7 | 1, 4, 5, 6 | syl3anc 1372 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (𝑥[,)(𝑥 + 1))) |
8 | | df-ov 7176 |
. . . . . 6
⊢ (𝑥[,)(𝑥 + 1)) = ([,)‘〈𝑥, (𝑥 + 1)〉) |
9 | 7, 8 | eleqtrdi 2844 |
. . . . 5
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ([,)‘〈𝑥, (𝑥 + 1)〉)) |
10 | | opelxpi 5563 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ (𝑥 + 1) ∈ ℝ) →
〈𝑥, (𝑥 + 1)〉 ∈ (ℝ
× ℝ)) |
11 | 2, 10 | mpdan 687 |
. . . . . 6
⊢ (𝑥 ∈ ℝ →
〈𝑥, (𝑥 + 1)〉 ∈ (ℝ
× ℝ)) |
12 | | fvres 6696 |
. . . . . 6
⊢
(〈𝑥, (𝑥 + 1)〉 ∈ (ℝ
× ℝ) → (([,) ↾ (ℝ ×
ℝ))‘〈𝑥,
(𝑥 + 1)〉) =
([,)‘〈𝑥, (𝑥 + 1)〉)) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ ℝ → (([,)
↾ (ℝ × ℝ))‘〈𝑥, (𝑥 + 1)〉) = ([,)‘〈𝑥, (𝑥 + 1)〉)) |
14 | 9, 13 | eleqtrrd 2837 |
. . . 4
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (([,) ↾ (ℝ
× ℝ))‘〈𝑥, (𝑥 + 1)〉)) |
15 | | icoreresf 35169 |
. . . . . . . 8
⊢ ([,)
↾ (ℝ × ℝ)):(ℝ × ℝ)⟶𝒫
ℝ |
16 | 15 | fdmi 6517 |
. . . . . . 7
⊢ dom ([,)
↾ (ℝ × ℝ)) = (ℝ × ℝ) |
17 | 10, 16 | eleqtrrdi 2845 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ (𝑥 + 1) ∈ ℝ) →
〈𝑥, (𝑥 + 1)〉 ∈ dom ([,)
↾ (ℝ × ℝ))) |
18 | 2, 17 | mpdan 687 |
. . . . 5
⊢ (𝑥 ∈ ℝ →
〈𝑥, (𝑥 + 1)〉 ∈ dom ([,)
↾ (ℝ × ℝ))) |
19 | | ffun 6508 |
. . . . . . . 8
⊢ (([,)
↾ (ℝ × ℝ)):(ℝ × ℝ)⟶𝒫
ℝ → Fun ([,) ↾ (ℝ × ℝ))) |
20 | 15, 19 | ax-mp 5 |
. . . . . . 7
⊢ Fun ([,)
↾ (ℝ × ℝ)) |
21 | | fvelrn 6857 |
. . . . . . 7
⊢ ((Fun
([,) ↾ (ℝ × ℝ)) ∧ 〈𝑥, (𝑥 + 1)〉 ∈ dom ([,) ↾ (ℝ
× ℝ))) → (([,) ↾ (ℝ ×
ℝ))‘〈𝑥,
(𝑥 + 1)〉) ∈ ran
([,) ↾ (ℝ × ℝ))) |
22 | 20, 21 | mpan 690 |
. . . . . 6
⊢
(〈𝑥, (𝑥 + 1)〉 ∈ dom ([,)
↾ (ℝ × ℝ)) → (([,) ↾ (ℝ ×
ℝ))‘〈𝑥,
(𝑥 + 1)〉) ∈ ran
([,) ↾ (ℝ × ℝ))) |
23 | | icoreunrn.1 |
. . . . . . 7
⊢ 𝐼 = ([,) “ (ℝ ×
ℝ)) |
24 | | df-ima 5539 |
. . . . . . 7
⊢ ([,)
“ (ℝ × ℝ)) = ran ([,) ↾ (ℝ ×
ℝ)) |
25 | 23, 24 | eqtri 2762 |
. . . . . 6
⊢ 𝐼 = ran ([,) ↾ (ℝ
× ℝ)) |
26 | 22, 25 | eleqtrrdi 2845 |
. . . . 5
⊢
(〈𝑥, (𝑥 + 1)〉 ∈ dom ([,)
↾ (ℝ × ℝ)) → (([,) ↾ (ℝ ×
ℝ))‘〈𝑥,
(𝑥 + 1)〉) ∈ 𝐼) |
27 | 18, 26 | syl 17 |
. . . 4
⊢ (𝑥 ∈ ℝ → (([,)
↾ (ℝ × ℝ))‘〈𝑥, (𝑥 + 1)〉) ∈ 𝐼) |
28 | | elunii 4802 |
. . . 4
⊢ ((𝑥 ∈ (([,) ↾ (ℝ
× ℝ))‘〈𝑥, (𝑥 + 1)〉) ∧ (([,) ↾ (ℝ
× ℝ))‘〈𝑥, (𝑥 + 1)〉) ∈ 𝐼) → 𝑥 ∈ ∪ 𝐼) |
29 | 14, 27, 28 | syl2anc 587 |
. . 3
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ∪ 𝐼) |
30 | 29 | ssriv 3882 |
. 2
⊢ ℝ
⊆ ∪ 𝐼 |
31 | | frn 6512 |
. . . . 5
⊢ (([,)
↾ (ℝ × ℝ)):(ℝ × ℝ)⟶𝒫
ℝ → ran ([,) ↾ (ℝ × ℝ)) ⊆ 𝒫
ℝ) |
32 | 15, 31 | ax-mp 5 |
. . . 4
⊢ ran ([,)
↾ (ℝ × ℝ)) ⊆ 𝒫 ℝ |
33 | 25, 32 | eqsstri 3912 |
. . 3
⊢ 𝐼 ⊆ 𝒫
ℝ |
34 | | uniss 4805 |
. . . 4
⊢ (𝐼 ⊆ 𝒫 ℝ
→ ∪ 𝐼 ⊆ ∪
𝒫 ℝ) |
35 | | unipw 5310 |
. . . 4
⊢ ∪ 𝒫 ℝ = ℝ |
36 | 34, 35 | sseqtrdi 3928 |
. . 3
⊢ (𝐼 ⊆ 𝒫 ℝ
→ ∪ 𝐼 ⊆ ℝ) |
37 | 33, 36 | ax-mp 5 |
. 2
⊢ ∪ 𝐼
⊆ ℝ |
38 | 30, 37 | eqssi 3894 |
1
⊢ ℝ =
∪ 𝐼 |