| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rexr 11308 | . . . . . . 7
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) | 
| 2 |  | peano2re 11435 | . . . . . . . 8
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ) | 
| 3 |  | rexr 11308 | . . . . . . . 8
⊢ ((𝑥 + 1) ∈ ℝ →
(𝑥 + 1) ∈
ℝ*) | 
| 4 | 2, 3 | syl 17 | . . . . . . 7
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ*) | 
| 5 |  | ltp1 12108 | . . . . . . 7
⊢ (𝑥 ∈ ℝ → 𝑥 < (𝑥 + 1)) | 
| 6 |  | lbico1 13442 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ (𝑥 + 1) ∈
ℝ* ∧ 𝑥
< (𝑥 + 1)) → 𝑥 ∈ (𝑥[,)(𝑥 + 1))) | 
| 7 | 1, 4, 5, 6 | syl3anc 1372 | . . . . . 6
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (𝑥[,)(𝑥 + 1))) | 
| 8 |  | df-ov 7435 | . . . . . 6
⊢ (𝑥[,)(𝑥 + 1)) = ([,)‘〈𝑥, (𝑥 + 1)〉) | 
| 9 | 7, 8 | eleqtrdi 2850 | . . . . 5
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ([,)‘〈𝑥, (𝑥 + 1)〉)) | 
| 10 |  | opelxpi 5721 | . . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ (𝑥 + 1) ∈ ℝ) →
〈𝑥, (𝑥 + 1)〉 ∈ (ℝ
× ℝ)) | 
| 11 | 2, 10 | mpdan 687 | . . . . . 6
⊢ (𝑥 ∈ ℝ →
〈𝑥, (𝑥 + 1)〉 ∈ (ℝ
× ℝ)) | 
| 12 |  | fvres 6924 | . . . . . 6
⊢
(〈𝑥, (𝑥 + 1)〉 ∈ (ℝ
× ℝ) → (([,) ↾ (ℝ ×
ℝ))‘〈𝑥,
(𝑥 + 1)〉) =
([,)‘〈𝑥, (𝑥 + 1)〉)) | 
| 13 | 11, 12 | syl 17 | . . . . 5
⊢ (𝑥 ∈ ℝ → (([,)
↾ (ℝ × ℝ))‘〈𝑥, (𝑥 + 1)〉) = ([,)‘〈𝑥, (𝑥 + 1)〉)) | 
| 14 | 9, 13 | eleqtrrd 2843 | . . . 4
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (([,) ↾ (ℝ
× ℝ))‘〈𝑥, (𝑥 + 1)〉)) | 
| 15 |  | icoreresf 37354 | . . . . . . . 8
⊢ ([,)
↾ (ℝ × ℝ)):(ℝ × ℝ)⟶𝒫
ℝ | 
| 16 | 15 | fdmi 6746 | . . . . . . 7
⊢ dom ([,)
↾ (ℝ × ℝ)) = (ℝ × ℝ) | 
| 17 | 10, 16 | eleqtrrdi 2851 | . . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ (𝑥 + 1) ∈ ℝ) →
〈𝑥, (𝑥 + 1)〉 ∈ dom ([,)
↾ (ℝ × ℝ))) | 
| 18 | 2, 17 | mpdan 687 | . . . . 5
⊢ (𝑥 ∈ ℝ →
〈𝑥, (𝑥 + 1)〉 ∈ dom ([,)
↾ (ℝ × ℝ))) | 
| 19 |  | ffun 6738 | . . . . . . . 8
⊢ (([,)
↾ (ℝ × ℝ)):(ℝ × ℝ)⟶𝒫
ℝ → Fun ([,) ↾ (ℝ × ℝ))) | 
| 20 | 15, 19 | ax-mp 5 | . . . . . . 7
⊢ Fun ([,)
↾ (ℝ × ℝ)) | 
| 21 |  | fvelrn 7095 | . . . . . . 7
⊢ ((Fun
([,) ↾ (ℝ × ℝ)) ∧ 〈𝑥, (𝑥 + 1)〉 ∈ dom ([,) ↾ (ℝ
× ℝ))) → (([,) ↾ (ℝ ×
ℝ))‘〈𝑥,
(𝑥 + 1)〉) ∈ ran
([,) ↾ (ℝ × ℝ))) | 
| 22 | 20, 21 | mpan 690 | . . . . . 6
⊢
(〈𝑥, (𝑥 + 1)〉 ∈ dom ([,)
↾ (ℝ × ℝ)) → (([,) ↾ (ℝ ×
ℝ))‘〈𝑥,
(𝑥 + 1)〉) ∈ ran
([,) ↾ (ℝ × ℝ))) | 
| 23 |  | icoreunrn.1 | . . . . . . 7
⊢ 𝐼 = ([,) “ (ℝ ×
ℝ)) | 
| 24 |  | df-ima 5697 | . . . . . . 7
⊢ ([,)
“ (ℝ × ℝ)) = ran ([,) ↾ (ℝ ×
ℝ)) | 
| 25 | 23, 24 | eqtri 2764 | . . . . . 6
⊢ 𝐼 = ran ([,) ↾ (ℝ
× ℝ)) | 
| 26 | 22, 25 | eleqtrrdi 2851 | . . . . 5
⊢
(〈𝑥, (𝑥 + 1)〉 ∈ dom ([,)
↾ (ℝ × ℝ)) → (([,) ↾ (ℝ ×
ℝ))‘〈𝑥,
(𝑥 + 1)〉) ∈ 𝐼) | 
| 27 | 18, 26 | syl 17 | . . . 4
⊢ (𝑥 ∈ ℝ → (([,)
↾ (ℝ × ℝ))‘〈𝑥, (𝑥 + 1)〉) ∈ 𝐼) | 
| 28 |  | elunii 4911 | . . . 4
⊢ ((𝑥 ∈ (([,) ↾ (ℝ
× ℝ))‘〈𝑥, (𝑥 + 1)〉) ∧ (([,) ↾ (ℝ
× ℝ))‘〈𝑥, (𝑥 + 1)〉) ∈ 𝐼) → 𝑥 ∈ ∪ 𝐼) | 
| 29 | 14, 27, 28 | syl2anc 584 | . . 3
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ∪ 𝐼) | 
| 30 | 29 | ssriv 3986 | . 2
⊢ ℝ
⊆ ∪ 𝐼 | 
| 31 |  | frn 6742 | . . . . 5
⊢ (([,)
↾ (ℝ × ℝ)):(ℝ × ℝ)⟶𝒫
ℝ → ran ([,) ↾ (ℝ × ℝ)) ⊆ 𝒫
ℝ) | 
| 32 | 15, 31 | ax-mp 5 | . . . 4
⊢ ran ([,)
↾ (ℝ × ℝ)) ⊆ 𝒫 ℝ | 
| 33 | 25, 32 | eqsstri 4029 | . . 3
⊢ 𝐼 ⊆ 𝒫
ℝ | 
| 34 |  | uniss 4914 | . . . 4
⊢ (𝐼 ⊆ 𝒫 ℝ
→ ∪ 𝐼 ⊆ ∪
𝒫 ℝ) | 
| 35 |  | unipw 5454 | . . . 4
⊢ ∪ 𝒫 ℝ = ℝ | 
| 36 | 34, 35 | sseqtrdi 4023 | . . 3
⊢ (𝐼 ⊆ 𝒫 ℝ
→ ∪ 𝐼 ⊆ ℝ) | 
| 37 | 33, 36 | ax-mp 5 | . 2
⊢ ∪ 𝐼
⊆ ℝ | 
| 38 | 30, 37 | eqssi 3999 | 1
⊢ ℝ =
∪ 𝐼 |