| Step | Hyp | Ref
| Expression |
| 1 | | df-ico 13393 |
. . . . . 6
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
| 2 | 1 | reseq1i 5993 |
. . . . 5
⊢ ([,)
↾ (ℝ × ℝ)) = ((𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) ↾ (ℝ ×
ℝ)) |
| 3 | | ressxr 11305 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
| 4 | | resmpo 7553 |
. . . . . 6
⊢ ((ℝ
⊆ ℝ* ∧ ℝ ⊆ ℝ*) →
((𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) ↾ (ℝ × ℝ)) =
(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})) |
| 5 | 3, 3, 4 | mp2an 692 |
. . . . 5
⊢ ((𝑥 ∈ ℝ*,
𝑦 ∈
ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) ↾ (ℝ × ℝ)) =
(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
| 6 | 2, 5 | eqtri 2765 |
. . . 4
⊢ ([,)
↾ (ℝ × ℝ)) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
| 7 | 6 | rneqi 5948 |
. . 3
⊢ ran ([,)
↾ (ℝ × ℝ)) = ran (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
| 8 | 7 | eleq2i 2833 |
. 2
⊢ (𝐴 ∈ ran ([,) ↾
(ℝ × ℝ)) ↔ 𝐴 ∈ ran (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})) |
| 9 | | eqid 2737 |
. . 3
⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
| 10 | | xrex 13029 |
. . . 4
⊢
ℝ* ∈ V |
| 11 | 10 | rabex 5339 |
. . 3
⊢ {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} ∈ V |
| 12 | 9, 11 | elrnmpo 7569 |
. 2
⊢ (𝐴 ∈ ran (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
| 13 | 3 | sseli 3979 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
| 14 | 13 | adantr 480 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈
ℝ*) |
| 15 | 3 | sseli 3979 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℝ*) |
| 16 | 15 | adantl 481 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℝ*) |
| 17 | | icoval 13425 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑥[,)𝑦) = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
| 18 | 14, 16, 17 | syl2anc 584 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥[,)𝑦) = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
| 19 | 18 | eqcomd 2743 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} = (𝑥[,)𝑦)) |
| 20 | 19 | eqeq2d 2748 |
. . . 4
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐴 = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} ↔ 𝐴 = (𝑥[,)𝑦))) |
| 21 | 20 | rexbidva 3177 |
. . 3
⊢ (𝑥 ∈ ℝ →
(∃𝑦 ∈ ℝ
𝐴 = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} ↔ ∃𝑦 ∈ ℝ 𝐴 = (𝑥[,)𝑦))) |
| 22 | 21 | rexbiia 3092 |
. 2
⊢
(∃𝑥 ∈
ℝ ∃𝑦 ∈
ℝ 𝐴 = {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥[,)𝑦)) |
| 23 | 8, 12, 22 | 3bitri 297 |
1
⊢ (𝐴 ∈ ran ([,) ↾
(ℝ × ℝ)) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥[,)𝑦)) |