Step | Hyp | Ref
| Expression |
1 | | itgex 24935 |
. . . 4
⊢
∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥 ∈ V |
2 | | df-area 26106 |
. . . 4
⊢ area =
(𝑠 ∈ {𝑡 ∈ 𝒫 (ℝ
× ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦
(vol‘(𝑡 “
{𝑥}))) ∈
𝐿1)} ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥) |
3 | 1, 2 | dmmpti 6577 |
. . 3
⊢ dom area
= {𝑡 ∈ 𝒫
(ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦
(vol‘(𝑡 “
{𝑥}))) ∈
𝐿1)} |
4 | 3 | eleq2i 2830 |
. 2
⊢ (𝐴 ∈ dom area ↔ 𝐴 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ)
∣ (∀𝑥 ∈
ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦
(vol‘(𝑡 “
{𝑥}))) ∈
𝐿1)}) |
5 | | imaeq1 5964 |
. . . . . 6
⊢ (𝑡 = 𝐴 → (𝑡 “ {𝑥}) = (𝐴 “ {𝑥})) |
6 | 5 | eleq1d 2823 |
. . . . 5
⊢ (𝑡 = 𝐴 → ((𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ↔ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ))) |
7 | 6 | ralbidv 3112 |
. . . 4
⊢ (𝑡 = 𝐴 → (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ↔ ∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ))) |
8 | 5 | fveq2d 6778 |
. . . . . 6
⊢ (𝑡 = 𝐴 → (vol‘(𝑡 “ {𝑥})) = (vol‘(𝐴 “ {𝑥}))) |
9 | 8 | mpteq2dv 5176 |
. . . . 5
⊢ (𝑡 = 𝐴 → (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) = (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥})))) |
10 | 9 | eleq1d 2823 |
. . . 4
⊢ (𝑡 = 𝐴 → ((𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1 ↔
(𝑥 ∈ ℝ ↦
(vol‘(𝐴 “
{𝑥}))) ∈
𝐿1)) |
11 | 7, 10 | anbi12d 631 |
. . 3
⊢ (𝑡 = 𝐴 → ((∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦
(vol‘(𝑡 “
{𝑥}))) ∈
𝐿1) ↔ (∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦
(vol‘(𝐴 “
{𝑥}))) ∈
𝐿1))) |
12 | 11 | elrab 3624 |
. 2
⊢ (𝐴 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ)
∣ (∀𝑥 ∈
ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦
(vol‘(𝑡 “
{𝑥}))) ∈
𝐿1)} ↔ (𝐴 ∈ 𝒫 (ℝ × ℝ)
∧ (∀𝑥 ∈
ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦
(vol‘(𝐴 “
{𝑥}))) ∈
𝐿1))) |
13 | | reex 10962 |
. . . . . 6
⊢ ℝ
∈ V |
14 | 13, 13 | xpex 7603 |
. . . . 5
⊢ (ℝ
× ℝ) ∈ V |
15 | 14 | elpw2 5269 |
. . . 4
⊢ (𝐴 ∈ 𝒫 (ℝ
× ℝ) ↔ 𝐴
⊆ (ℝ × ℝ)) |
16 | 15 | anbi1i 624 |
. . 3
⊢ ((𝐴 ∈ 𝒫 (ℝ
× ℝ) ∧ (∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦
(vol‘(𝐴 “
{𝑥}))) ∈
𝐿1)) ↔ (𝐴 ⊆ (ℝ × ℝ) ∧
(∀𝑥 ∈ ℝ
(𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦
(vol‘(𝐴 “
{𝑥}))) ∈
𝐿1))) |
17 | | 3anass 1094 |
. . 3
⊢ ((𝐴 ⊆ (ℝ ×
ℝ) ∧ ∀𝑥
∈ ℝ (𝐴 “
{𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦
(vol‘(𝐴 “
{𝑥}))) ∈
𝐿1) ↔ (𝐴 ⊆ (ℝ × ℝ) ∧
(∀𝑥 ∈ ℝ
(𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦
(vol‘(𝐴 “
{𝑥}))) ∈
𝐿1))) |
18 | 16, 17 | bitr4i 277 |
. 2
⊢ ((𝐴 ∈ 𝒫 (ℝ
× ℝ) ∧ (∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦
(vol‘(𝐴 “
{𝑥}))) ∈
𝐿1)) ↔ (𝐴 ⊆ (ℝ × ℝ) ∧
∀𝑥 ∈ ℝ
(𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦
(vol‘(𝐴 “
{𝑥}))) ∈
𝐿1)) |
19 | 4, 12, 18 | 3bitri 297 |
1
⊢ (𝐴 ∈ dom area ↔ (𝐴 ⊆ (ℝ ×
ℝ) ∧ ∀𝑥
∈ ℝ (𝐴 “
{𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦
(vol‘(𝐴 “
{𝑥}))) ∈
𝐿1)) |