Step | Hyp | Ref
| Expression |
1 | | df-ico 12052 |
. . . . . . . . 9
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
2 | 1 | reseq1i 5313 |
. . . . . . . 8
⊢ ([,)
↾ (ℝ × ℝ)) = ((𝑥 ∈ ℝ*, 𝑦 ∈ ℝ*
↦ {𝑧 ∈
ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) ↾ (ℝ ×
ℝ)) |
3 | | ressxr 9962 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ* |
4 | | resmpt2 6656 |
. . . . . . . . 9
⊢ ((ℝ
⊆ ℝ* ∧ ℝ ⊆ ℝ*) →
((𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) ↾ (ℝ × ℝ)) =
(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})) |
5 | 3, 3, 4 | mp2an 704 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ*,
𝑦 ∈
ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) ↾ (ℝ × ℝ)) =
(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
6 | 2, 5 | eqtri 2632 |
. . . . . . 7
⊢ ([,)
↾ (ℝ × ℝ)) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
7 | 6 | rneqi 5273 |
. . . . . 6
⊢ ran ([,)
↾ (ℝ × ℝ)) = ran (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
8 | 7 | eleq2i 2680 |
. . . . 5
⊢ (𝐴 ∈ ran ([,) ↾
(ℝ × ℝ)) ↔ 𝐴 ∈ ran (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})) |
9 | 8 | biimpi 205 |
. . . 4
⊢ (𝐴 ∈ ran ([,) ↾
(ℝ × ℝ)) → 𝐴 ∈ ran (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})) |
10 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
11 | | xrex 11705 |
. . . . . 6
⊢
ℝ* ∈ V |
12 | 11 | rabex 4740 |
. . . . 5
⊢ {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} ∈ V |
13 | 10, 12 | elrnmpt2 6671 |
. . . 4
⊢ (𝐴 ∈ ran (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) ↔ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
14 | 9, 13 | sylib 207 |
. . 3
⊢ (𝐴 ∈ ran ([,) ↾
(ℝ × ℝ)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
15 | | simpr 476 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐴 = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) → 𝐴 = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
16 | 3 | sseli 3564 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
17 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈
ℝ*) |
18 | 3 | sseli 3564 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℝ*) |
19 | 18 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℝ*) |
20 | | icoval 12084 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑥[,)𝑦) = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
21 | 17, 19, 20 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥[,)𝑦) = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
22 | 21 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → {𝑧 ∈ ℝ*
∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} = (𝑥[,)𝑦)) |
23 | 22 | adantr 480 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐴 = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) → {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} = (𝑥[,)𝑦)) |
24 | 15, 23 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐴 = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) → 𝐴 = (𝑥[,)𝑦)) |
25 | 24 | ex 449 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐴 = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} → 𝐴 = (𝑥[,)𝑦))) |
26 | 25 | adantll 746 |
. . . . 5
⊢ (((𝐴 ∈ ran ([,) ↾
(ℝ × ℝ)) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (𝐴 = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} → 𝐴 = (𝑥[,)𝑦))) |
27 | 26 | reximdva 3000 |
. . . 4
⊢ ((𝐴 ∈ ran ([,) ↾
(ℝ × ℝ)) ∧ 𝑥 ∈ ℝ) → (∃𝑦 ∈ ℝ 𝐴 = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} → ∃𝑦 ∈ ℝ 𝐴 = (𝑥[,)𝑦))) |
28 | 27 | reximdva 3000 |
. . 3
⊢ (𝐴 ∈ ran ([,) ↾
(ℝ × ℝ)) → (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)} → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥[,)𝑦))) |
29 | 14, 28 | mpd 15 |
. 2
⊢ (𝐴 ∈ ran ([,) ↾
(ℝ × ℝ)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥[,)𝑦)) |
30 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝐴 = (𝑥[,)𝑦) → (vol‘𝐴) = (vol‘(𝑥[,)𝑦))) |
31 | 30 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐴 = (𝑥[,)𝑦)) → (vol‘𝐴) = (vol‘(𝑥[,)𝑦))) |
32 | | volicorecl 39436 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(vol‘(𝑥[,)𝑦)) ∈
ℝ) |
33 | 32 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐴 = (𝑥[,)𝑦)) → (vol‘(𝑥[,)𝑦)) ∈ ℝ) |
34 | 31, 33 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐴 = (𝑥[,)𝑦)) → (vol‘𝐴) ∈ ℝ) |
35 | 34 | ex 449 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐴 = (𝑥[,)𝑦) → (vol‘𝐴) ∈ ℝ)) |
36 | 35 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ran ([,) ↾
(ℝ × ℝ)) → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐴 = (𝑥[,)𝑦) → (vol‘𝐴) ∈ ℝ))) |
37 | 36 | rexlimdvv 3019 |
. . . . 5
⊢ (𝐴 ∈ ran ([,) ↾
(ℝ × ℝ)) → (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥[,)𝑦) → (vol‘𝐴) ∈ ℝ)) |
38 | 29, 37 | mpd 15 |
. . . 4
⊢ (𝐴 ∈ ran ([,) ↾
(ℝ × ℝ)) → (vol‘𝐴) ∈ ℝ) |
39 | 38 | 2a1d 26 |
. . 3
⊢ (𝐴 ∈ ran ([,) ↾
(ℝ × ℝ)) → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐴 = (𝑥[,)𝑦) → (vol‘𝐴) ∈ ℝ))) |
40 | 39 | rexlimdvv 3019 |
. 2
⊢ (𝐴 ∈ ran ([,) ↾
(ℝ × ℝ)) → (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥[,)𝑦) → (vol‘𝐴) ∈ ℝ)) |
41 | 29, 40 | mpd 15 |
1
⊢ (𝐴 ∈ ran ([,) ↾
(ℝ × ℝ)) → (vol‘𝐴) ∈ ℝ) |