Step | Hyp | Ref
| Expression |
1 | | rexr 11021 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
2 | | peano2re 11148 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ) |
3 | | rexr 11021 |
. . . . . . . 8
⊢ ((𝑥 + 1) ∈ ℝ →
(𝑥 + 1) ∈
ℝ*) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ*) |
5 | | ltp1 11815 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → 𝑥 < (𝑥 + 1)) |
6 | | lbico1 13133 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ (𝑥 + 1) ∈
ℝ* ∧ 𝑥
< (𝑥 + 1)) → 𝑥 ∈ (𝑥[,)(𝑥 + 1))) |
7 | 1, 4, 5, 6 | syl3anc 1370 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (𝑥[,)(𝑥 + 1))) |
8 | | df-ov 7278 |
. . . . . 6
⊢ (𝑥[,)(𝑥 + 1)) = ([,)‘〈𝑥, (𝑥 + 1)〉) |
9 | 7, 8 | eleqtrdi 2849 |
. . . . 5
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ([,)‘〈𝑥, (𝑥 + 1)〉)) |
10 | | opelxpi 5626 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ (𝑥 + 1) ∈ ℝ) →
〈𝑥, (𝑥 + 1)〉 ∈ (ℝ
× ℝ)) |
11 | 2, 10 | mpdan 684 |
. . . . . 6
⊢ (𝑥 ∈ ℝ →
〈𝑥, (𝑥 + 1)〉 ∈ (ℝ
× ℝ)) |
12 | | fvres 6793 |
. . . . . 6
⊢
(〈𝑥, (𝑥 + 1)〉 ∈ (ℝ
× ℝ) → (([,) ↾ (ℝ ×
ℝ))‘〈𝑥,
(𝑥 + 1)〉) =
([,)‘〈𝑥, (𝑥 + 1)〉)) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ ℝ → (([,)
↾ (ℝ × ℝ))‘〈𝑥, (𝑥 + 1)〉) = ([,)‘〈𝑥, (𝑥 + 1)〉)) |
14 | 9, 13 | eleqtrrd 2842 |
. . . 4
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (([,) ↾ (ℝ
× ℝ))‘〈𝑥, (𝑥 + 1)〉)) |
15 | | icoreresf 35523 |
. . . . . . . 8
⊢ ([,)
↾ (ℝ × ℝ)):(ℝ × ℝ)⟶𝒫
ℝ |
16 | 15 | fdmi 6612 |
. . . . . . 7
⊢ dom ([,)
↾ (ℝ × ℝ)) = (ℝ × ℝ) |
17 | 10, 16 | eleqtrrdi 2850 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ (𝑥 + 1) ∈ ℝ) →
〈𝑥, (𝑥 + 1)〉 ∈ dom ([,)
↾ (ℝ × ℝ))) |
18 | 2, 17 | mpdan 684 |
. . . . 5
⊢ (𝑥 ∈ ℝ →
〈𝑥, (𝑥 + 1)〉 ∈ dom ([,)
↾ (ℝ × ℝ))) |
19 | | ffun 6603 |
. . . . . . . 8
⊢ (([,)
↾ (ℝ × ℝ)):(ℝ × ℝ)⟶𝒫
ℝ → Fun ([,) ↾ (ℝ × ℝ))) |
20 | 15, 19 | ax-mp 5 |
. . . . . . 7
⊢ Fun ([,)
↾ (ℝ × ℝ)) |
21 | | fvelrn 6954 |
. . . . . . 7
⊢ ((Fun
([,) ↾ (ℝ × ℝ)) ∧ 〈𝑥, (𝑥 + 1)〉 ∈ dom ([,) ↾ (ℝ
× ℝ))) → (([,) ↾ (ℝ ×
ℝ))‘〈𝑥,
(𝑥 + 1)〉) ∈ ran
([,) ↾ (ℝ × ℝ))) |
22 | 20, 21 | mpan 687 |
. . . . . 6
⊢
(〈𝑥, (𝑥 + 1)〉 ∈ dom ([,)
↾ (ℝ × ℝ)) → (([,) ↾ (ℝ ×
ℝ))‘〈𝑥,
(𝑥 + 1)〉) ∈ ran
([,) ↾ (ℝ × ℝ))) |
23 | | icoreunrn.1 |
. . . . . . 7
⊢ 𝐼 = ([,) “ (ℝ ×
ℝ)) |
24 | | df-ima 5602 |
. . . . . . 7
⊢ ([,)
“ (ℝ × ℝ)) = ran ([,) ↾ (ℝ ×
ℝ)) |
25 | 23, 24 | eqtri 2766 |
. . . . . 6
⊢ 𝐼 = ran ([,) ↾ (ℝ
× ℝ)) |
26 | 22, 25 | eleqtrrdi 2850 |
. . . . 5
⊢
(〈𝑥, (𝑥 + 1)〉 ∈ dom ([,)
↾ (ℝ × ℝ)) → (([,) ↾ (ℝ ×
ℝ))‘〈𝑥,
(𝑥 + 1)〉) ∈ 𝐼) |
27 | 18, 26 | syl 17 |
. . . 4
⊢ (𝑥 ∈ ℝ → (([,)
↾ (ℝ × ℝ))‘〈𝑥, (𝑥 + 1)〉) ∈ 𝐼) |
28 | | elunii 4844 |
. . . 4
⊢ ((𝑥 ∈ (([,) ↾ (ℝ
× ℝ))‘〈𝑥, (𝑥 + 1)〉) ∧ (([,) ↾ (ℝ
× ℝ))‘〈𝑥, (𝑥 + 1)〉) ∈ 𝐼) → 𝑥 ∈ ∪ 𝐼) |
29 | 14, 27, 28 | syl2anc 584 |
. . 3
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ∪ 𝐼) |
30 | 29 | ssriv 3925 |
. 2
⊢ ℝ
⊆ ∪ 𝐼 |
31 | | frn 6607 |
. . . . 5
⊢ (([,)
↾ (ℝ × ℝ)):(ℝ × ℝ)⟶𝒫
ℝ → ran ([,) ↾ (ℝ × ℝ)) ⊆ 𝒫
ℝ) |
32 | 15, 31 | ax-mp 5 |
. . . 4
⊢ ran ([,)
↾ (ℝ × ℝ)) ⊆ 𝒫 ℝ |
33 | 25, 32 | eqsstri 3955 |
. . 3
⊢ 𝐼 ⊆ 𝒫
ℝ |
34 | | uniss 4847 |
. . . 4
⊢ (𝐼 ⊆ 𝒫 ℝ
→ ∪ 𝐼 ⊆ ∪
𝒫 ℝ) |
35 | | unipw 5366 |
. . . 4
⊢ ∪ 𝒫 ℝ = ℝ |
36 | 34, 35 | sseqtrdi 3971 |
. . 3
⊢ (𝐼 ⊆ 𝒫 ℝ
→ ∪ 𝐼 ⊆ ℝ) |
37 | 33, 36 | ax-mp 5 |
. 2
⊢ ∪ 𝐼
⊆ ℝ |
38 | 30, 37 | eqssi 3937 |
1
⊢ ℝ =
∪ 𝐼 |