Definition df-area 26935

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

Step	Hyp	Ref	Expression
1		carea 26934	. 2 class area
2		vs	. . 3 setvar 𝑠
3		vt	. . . . . . . . 9 setvar 𝑡
4	3	cv 1538	. . . . . . . 8 class 𝑡
5		vx	. . . . . . . . . 10 setvar 𝑥
6	5	cv 1538	. . . . . . . . 9 class 𝑥
7	6	csn 4606	. . . . . . . 8 class {𝑥}
8	4, 7	cima 5668	. . . . . . 7 class (𝑡 “ {𝑥})
9		cvol 25434	. . . . . . . . 9 class vol
10	9	ccnv 5664	. . . . . . . 8 class ◡vol
11		cr 11136	. . . . . . . 8 class ℝ
12	10, 11	cima 5668	. . . . . . 7 class (◡vol “ ℝ)
13	8, 12	wcel 2107	. . . . . 6 wff (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ)
14	13, 5, 11	wral 3050	. . . . 5 wff ∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ)
15	8, 9	cfv 6541	. . . . . . 7 class (vol‘(𝑡 “ {𝑥}))
16	5, 11, 15	cmpt 5205	. . . . . 6 class (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥})))
17		cibl 25588	. . . . . 6 class 𝐿1
18	16, 17	wcel 2107	. . . . 5 wff (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1
19	14, 18	wa 395	. . . 4 wff (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)
20	11, 11	cxp 5663	. . . . 5 class (ℝ × ℝ)
21	20	cpw 4580	. . . 4 class 𝒫 (ℝ × ℝ)
22	19, 3, 21	crab 3419	. . 3 class {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)}
23	2	cv 1538	. . . . . 6 class 𝑠
24	23, 7	cima 5668	. . . . 5 class (𝑠 “ {𝑥})
25	24, 9	cfv 6541	. . . 4 class (vol‘(𝑠 “ {𝑥}))
26	5, 11, 25	citg 25589	. . 3 class ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥
27	2, 22, 26	cmpt 5205	. 2 class (𝑠 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)} ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥)
28	1, 27	wceq 1539	1 wff area = (𝑠 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)} ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥)

This definition is referenced by:  dmarea  26936  dfarea  26939