Definition df-area

Description: Define the area of a subset of RR X. RR . (Contributed by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Assertion	df-area	⊢ area = ( 𝑠 ∈ { 𝑡 ∈ 𝒫 ( ℝ × ℝ ) ∣ ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) } ↦ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		carea	⊢ area
1		vs	⊢ 𝑠
2		vt	⊢ 𝑡
3		cr	⊢ ℝ
4	3 3	cxp	⊢ ( ℝ × ℝ )
5	4	cpw	⊢ 𝒫 ( ℝ × ℝ )
6		vx	⊢ 𝑥
7	2	cv	⊢ 𝑡
8	6	cv	⊢ 𝑥
9	8	csn	⊢ { 𝑥 }
10	7 9	cima	⊢ ( 𝑡 “ { 𝑥 } )
11		cvol	⊢ vol
12	11	ccnv	⊢ ◡ vol
13	12 3	cima	⊢ ( ◡ vol “ ℝ )
14	10 13	wcel	⊢ ( 𝑡 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ )
15	14 6 3	wral	⊢ ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ )
16	10 11	cfv	⊢ ( vol ‘ ( 𝑡 “ { 𝑥 } ) )
17	6 3 16	cmpt	⊢ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) )
18		cibl	⊢ 𝐿1
19	17 18	wcel	⊢ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1
20	15 19	wa	⊢ ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 )
21	20 2 5	crab	⊢ { 𝑡 ∈ 𝒫 ( ℝ × ℝ ) ∣ ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) }
22	1	cv	⊢ 𝑠
23	22 9	cima	⊢ ( 𝑠 “ { 𝑥 } )
24	23 11	cfv	⊢ ( vol ‘ ( 𝑠 “ { 𝑥 } ) )
25	6 3 24	citg	⊢ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥
26	1 21 25	cmpt	⊢ ( 𝑠 ∈ { 𝑡 ∈ 𝒫 ( ℝ × ℝ ) ∣ ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) } ↦ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 )
27	0 26	wceq	⊢ area = ( 𝑠 ∈ { 𝑡 ∈ 𝒫 ( ℝ × ℝ ) ∣ ( ∀ 𝑥 ∈ ℝ ( 𝑡 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑡 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) } ↦ ∫ ℝ ( vol ‘ ( 𝑠 “ { 𝑥 } ) ) d 𝑥 )