Definition df-area 24683

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

Assertion

Ref	Expression
df-area	|- area = ( s e. { t e. ~P ( RR X. RR ) | ( A. x e. RR ( t " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( t " { x } ) ) ) e. L^1 ) } |-> S. RR ( vol ` ( s " { x } ) ) _d x )

Distinct variable group:   t, s, x

Detailed syntax breakdown of Definition df-area

Step	Hyp	Ref	Expression
1		carea 24682	. 2 class area
2		vs	. . 3 setvar s
3		vt	. . . . . . . . 9 setvar t
4	3	cv 1482	. . . . . . . 8 class t
5		vx	. . . . . . . . . 10 setvar x
6	5	cv 1482	. . . . . . . . 9 class x
7	6	csn 4177	. . . . . . . 8 class { x }
8	4, 7	cima 5117	. . . . . . 7 class ( t " { x } )
9		cvol 23232	. . . . . . . . 9 class vol
10	9	ccnv 5113	. . . . . . . 8 class `' vol
11		cr 9935	. . . . . . . 8 class RR
12	10, 11	cima 5117	. . . . . . 7 class ( `' vol " RR )
13	8, 12	wcel 1990	. . . . . 6 wff ( t " { x } ) e. ( `' vol " RR )
14	13, 5, 11	wral 2912	. . . . 5 wff A. x e. RR ( t " { x } ) e. ( `' vol " RR )
15	8, 9	cfv 5888	. . . . . . 7 class ( vol ` ( t " { x } ) )
16	5, 11, 15	cmpt 4729	. . . . . 6 class ( x e. RR |-> ( vol ` ( t " { x } ) ) )
17		cibl 23386	. . . . . 6 class L^1
18	16, 17	wcel 1990	. . . . 5 wff ( x e. RR |-> ( vol ` ( t " { x } ) ) ) e. L^1
19	14, 18	wa 384	. . . 4 wff ( A. x e. RR ( t " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( t " { x } ) ) ) e. L^1 )
20	11, 11	cxp 5112	. . . . 5 class ( RR X. RR )
21	20	cpw 4158	. . . 4 class ~P ( RR X. RR )
22	19, 3, 21	crab 2916	. . 3 class { t e. ~P ( RR X. RR ) | ( A. x e. RR ( t " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( t " { x } ) ) ) e. L^1 ) }
23	2	cv 1482	. . . . . 6 class s
24	23, 7	cima 5117	. . . . 5 class ( s " { x } )
25	24, 9	cfv 5888	. . . 4 class ( vol ` ( s " { x } ) )
26	5, 11, 25	citg 23387	. . 3 class S. RR ( vol ` ( s " { x } ) ) _d x
27	2, 22, 26	cmpt 4729	. 2 class ( s e. { t e. ~P ( RR X. RR ) | ( A. x e. RR ( t " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( t " { x } ) ) ) e. L^1 ) } |-> S. RR ( vol ` ( s " { x } ) ) _d x )
28	1, 27	wceq 1483	1 wff area = ( s e. { t e. ~P ( RR X. RR ) | ( A. x e. RR ( t " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( t " { x } ) ) ) e. L^1 ) } |-> S. RR ( vol ` ( s " { x } ) ) _d x )

This definition is referenced by:  dmarea  24684  dfarea  24687