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

Definition df-area 20267
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 20266 . 2  class area
2 vs . . 3  set  s
3 vt . . . . . . . . 9  set  t
43cv 1631 . . . . . . . 8  class  t
5 vx . . . . . . . . . 10  set  x
65cv 1631 . . . . . . . . 9  class  x
76csn 3653 . . . . . . . 8  class  { x }
84, 7cima 4708 . . . . . . 7  class  ( t
" { x }
)
9 cvol 18839 . . . . . . . . 9  class  vol
109ccnv 4704 . . . . . . . 8  class  `' vol
11 cr 8752 . . . . . . . 8  class  RR
1210, 11cima 4708 . . . . . . 7  class  ( `' vol " RR )
138, 12wcel 1696 . . . . . 6  wff  ( t
" { x }
)  e.  ( `' vol " RR )
1413, 5, 11wral 2556 . . . . 5  wff  A. x  e.  RR  ( t " { x } )  e.  ( `' vol " RR )
158, 9cfv 5271 . . . . . . 7  class  ( vol `  ( t " {
x } ) )
165, 11, 15cmpt 4093 . . . . . 6  class  ( x  e.  RR  |->  ( vol `  ( t " {
x } ) ) )
17 cibl 18988 . . . . . 6  class  L ^1
1816, 17wcel 1696 . . . . 5  wff  ( x  e.  RR  |->  ( vol `  ( t " {
x } ) ) )  e.  L ^1
1914, 18wa 358 . . . 4  wff  ( A. x  e.  RR  (
t " { x } )  e.  ( `' vol " RR )  /\  ( x  e.  RR  |->  ( vol `  (
t " { x } ) ) )  e.  L ^1 )
2011, 11cxp 4703 . . . . 5  class  ( RR 
X.  RR )
2120cpw 3638 . . . 4  class  ~P ( RR  X.  RR )
2219, 3, 21crab 2560 . . 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 1631 . . . . . 6  class  s
2423, 7cima 4708 . . . . 5  class  ( s
" { x }
)
2524, 9cfv 5271 . . . 4  class  ( vol `  ( s " {
x } ) )
265, 11, 25citg 18989 . . 3  class  S. RR ( vol `  ( s
" { x }
) )  _d x
272, 22, 26cmpt 4093 . 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 1632 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  20268  dfarea  20271
  Copyright terms: Public domain W3C validator