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

Definition df-area 23014
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
StepHypRef Expression
1 carea 23013 . 2  class area
2 vs . . 3  setvar  s
3 vt . . . . . . . . 9  setvar  t
43cv 1378 . . . . . . . 8  class  t
5 vx . . . . . . . . . 10  setvar  x
65cv 1378 . . . . . . . . 9  class  x
76csn 4027 . . . . . . . 8  class  { x }
84, 7cima 5002 . . . . . . 7  class  ( t
" { x }
)
9 cvol 21610 . . . . . . . . 9  class  vol
109ccnv 4998 . . . . . . . 8  class  `' vol
11 cr 9487 . . . . . . . 8  class  RR
1210, 11cima 5002 . . . . . . 7  class  ( `' vol " RR )
138, 12wcel 1767 . . . . . 6  wff  ( t
" { x }
)  e.  ( `' vol " RR )
1413, 5, 11wral 2814 . . . . 5  wff  A. x  e.  RR  ( t " { x } )  e.  ( `' vol " RR )
158, 9cfv 5586 . . . . . . 7  class  ( vol `  ( t " {
x } ) )
165, 11, 15cmpt 4505 . . . . . 6  class  ( x  e.  RR  |->  ( vol `  ( t " {
x } ) ) )
17 cibl 21761 . . . . . 6  class  L^1
1816, 17wcel 1767 . . . . 5  wff  ( x  e.  RR  |->  ( vol `  ( t " {
x } ) ) )  e.  L^1
1914, 18wa 369 . . . 4  wff  ( A. x  e.  RR  (
t " { x } )  e.  ( `' vol " RR )  /\  ( x  e.  RR  |->  ( vol `  (
t " { x } ) ) )  e.  L^1 )
2011, 11cxp 4997 . . . . 5  class  ( RR 
X.  RR )
2120cpw 4010 . . . 4  class  ~P ( RR  X.  RR )
2219, 3, 21crab 2818 . . 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 ) }
232cv 1378 . . . . . 6  class  s
2423, 7cima 5002 . . . . 5  class  ( s
" { x }
)
2524, 9cfv 5586 . . . 4  class  ( vol `  ( s " {
x } ) )
265, 11, 25citg 21762 . . 3  class  S. RR ( vol `  ( s
" { x }
) )  _d x
272, 22, 26cmpt 4505 . 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 )
281, 27wceq 1379 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 )
Colors of variables: wff setvar class
This definition is referenced by:  dmarea  23015  dfarea  23018
  Copyright terms: Public domain W3C validator