MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-area Structured version   Visualization version   GIF version

Definition df-area 25461
Description: Define the area of a subset of ℝ × ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.)
Assertion
Ref Expression
df-area area = (𝑠 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)} ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥)
Distinct variable group:   𝑡,𝑠,𝑥

Detailed syntax breakdown of Definition df-area
StepHypRef Expression
1 carea 25460 . 2 class area
2 vs . . 3 setvar 𝑠
3 vt . . . . . . . . 9 setvar 𝑡
43cv 1527 . . . . . . . 8 class 𝑡
5 vx . . . . . . . . . 10 setvar 𝑥
65cv 1527 . . . . . . . . 9 class 𝑥
76csn 4557 . . . . . . . 8 class {𝑥}
84, 7cima 5551 . . . . . . 7 class (𝑡 “ {𝑥})
9 cvol 23991 . . . . . . . . 9 class vol
109ccnv 5547 . . . . . . . 8 class vol
11 cr 10524 . . . . . . . 8 class
1210, 11cima 5551 . . . . . . 7 class (vol “ ℝ)
138, 12wcel 2105 . . . . . 6 wff (𝑡 “ {𝑥}) ∈ (vol “ ℝ)
1413, 5, 11wral 3135 . . . . 5 wff 𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (vol “ ℝ)
158, 9cfv 6348 . . . . . . 7 class (vol‘(𝑡 “ {𝑥}))
165, 11, 15cmpt 5137 . . . . . 6 class (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥})))
17 cibl 24145 . . . . . 6 class 𝐿1
1816, 17wcel 2105 . . . . 5 wff (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1
1914, 18wa 396 . . . 4 wff (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)
2011, 11cxp 5546 . . . . 5 class (ℝ × ℝ)
2120cpw 4535 . . . 4 class 𝒫 (ℝ × ℝ)
2219, 3, 21crab 3139 . . 3 class {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)}
232cv 1527 . . . . . 6 class 𝑠
2423, 7cima 5551 . . . . 5 class (𝑠 “ {𝑥})
2524, 9cfv 6348 . . . 4 class (vol‘(𝑠 “ {𝑥}))
265, 11, 25citg 24146 . . 3 class ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥
272, 22, 26cmpt 5137 . 2 class (𝑠 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)} ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥)
281, 27wceq 1528 1 wff area = (𝑠 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)} ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥)
Colors of variables: wff setvar class
This definition is referenced by:  dmarea  25462  dfarea  25465
  Copyright terms: Public domain W3C validator