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

Definition df-area 20251
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 20250 . 2  class area
2 vs . . 3  set  s
3 vt . . . . . . . . 9  set  t
43cv 1622 . . . . . . . 8  class  t
5 vx . . . . . . . . . 10  set  x
65cv 1622 . . . . . . . . 9  class  x
76csn 3640 . . . . . . . 8  class  { x }
84, 7cima 4692 . . . . . . 7  class  ( t
" { x }
)
9 cvol 18823 . . . . . . . . 9  class  vol
109ccnv 4688 . . . . . . . 8  class  `' vol
11 cr 8736 . . . . . . . 8  class  RR
1210, 11cima 4692 . . . . . . 7  class  ( `' vol " RR )
138, 12wcel 1684 . . . . . 6  wff  ( t
" { x }
)  e.  ( `' vol " RR )
1413, 5, 11wral 2543 . . . . 5  wff  A. x  e.  RR  ( t " { x } )  e.  ( `' vol " RR )
158, 9cfv 5255 . . . . . . 7  class  ( vol `  ( t " {
x } ) )
165, 11, 15cmpt 4077 . . . . . 6  class  ( x  e.  RR  |->  ( vol `  ( t " {
x } ) ) )
17 cibl 18972 . . . . . 6  class  L ^1
1816, 17wcel 1684 . . . . 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 4687 . . . . 5  class  ( RR 
X.  RR )
2120cpw 3625 . . . 4  class  ~P ( RR  X.  RR )
2219, 3, 21crab 2547 . . 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 1622 . . . . . 6  class  s
2423, 7cima 4692 . . . . 5  class  ( s
" { x }
)
2524, 9cfv 5255 . . . 4  class  ( vol `  ( s " {
x } ) )
265, 11, 25citg 18973 . . 3  class  S. RR ( vol `  ( s
" { x }
) )  _d x
272, 22, 26cmpt 4077 . 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 1623 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  20252  dfarea  20255
  Copyright terms: Public domain W3C validator