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

Definition df-area 20663
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 20662 . 2  class area
2 vs . . 3  set  s
3 vt . . . . . . . . 9  set  t
43cv 1648 . . . . . . . 8  class  t
5 vx . . . . . . . . . 10  set  x
65cv 1648 . . . . . . . . 9  class  x
76csn 3758 . . . . . . . 8  class  { x }
84, 7cima 4822 . . . . . . 7  class  ( t
" { x }
)
9 cvol 19228 . . . . . . . . 9  class  vol
109ccnv 4818 . . . . . . . 8  class  `' vol
11 cr 8923 . . . . . . . 8  class  RR
1210, 11cima 4822 . . . . . . 7  class  ( `' vol " RR )
138, 12wcel 1717 . . . . . 6  wff  ( t
" { x }
)  e.  ( `' vol " RR )
1413, 5, 11wral 2650 . . . . 5  wff  A. x  e.  RR  ( t " { x } )  e.  ( `' vol " RR )
158, 9cfv 5395 . . . . . . 7  class  ( vol `  ( t " {
x } ) )
165, 11, 15cmpt 4208 . . . . . 6  class  ( x  e.  RR  |->  ( vol `  ( t " {
x } ) ) )
17 cibl 19377 . . . . . 6  class  L ^1
1816, 17wcel 1717 . . . . 5  wff  ( x  e.  RR  |->  ( vol `  ( t " {
x } ) ) )  e.  L ^1
1914, 18wa 359 . . . 4  wff  ( A. x  e.  RR  (
t " { x } )  e.  ( `' vol " RR )  /\  ( x  e.  RR  |->  ( vol `  (
t " { x } ) ) )  e.  L ^1 )
2011, 11cxp 4817 . . . . 5  class  ( RR 
X.  RR )
2120cpw 3743 . . . 4  class  ~P ( RR  X.  RR )
2219, 3, 21crab 2654 . . 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 1648 . . . . . 6  class  s
2423, 7cima 4822 . . . . 5  class  ( s
" { x }
)
2524, 9cfv 5395 . . . 4  class  ( vol `  ( s " {
x } ) )
265, 11, 25citg 19378 . . 3  class  S. RR ( vol `  ( s
" { x }
) )  _d x
272, 22, 26cmpt 4208 . 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 1649 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 set class
This definition is referenced by:  dmarea  20664  dfarea  20667
  Copyright terms: Public domain W3C validator