Metamath Proof Explorer

Definition df-area

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

Ref Expression
Assertion 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 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 carea 
 |-  area
1 vs 
 |-  s
2 vt 
 |-  t
3 cr 
 |-  RR
4 3 3 cxp 
 |-  ( RR X. RR )
5 4 cpw 
 |-  ~P ( RR X. RR )
6 vx 
 |-  x
7 2 cv 
 |-  t
8 6 cv 
 |-  x
9 8 csn 
 |-  { x }
10 7 9 cima 
 |-  ( t " { x } )
11 cvol 
 |-  vol
12 11 ccnv 
 |-  `' vol
13 12 3 cima 
 |-  ( `' vol " RR )
14 10 13 wcel 
 |-  ( t " { x } ) e. ( `' vol " RR )
15 14 6 3 wral 
 |-  A. x e. RR ( t " { x } ) e. ( `' vol " RR )
16 10 11 cfv 
 |-  ( vol ` ( t " { x } ) )
17 6 3 16 cmpt 
 |-  ( x e. RR |-> ( vol ` ( t " { x } ) ) )
18 cibl 
 |-  L^1
19 17 18 wcel 
 |-  ( x e. RR |-> ( vol ` ( t " { x } ) ) ) e. L^1
20 15 19 wa 
 |-  ( A. x e. RR ( t " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( t " { x } ) ) ) e. L^1 )
21 20 2 5 crab 
 |-  { t e. ~P ( RR X. RR ) | ( A. x e. RR ( t " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( t " { x } ) ) ) e. L^1 ) }
22 1 cv 
 |-  s
23 22 9 cima 
 |-  ( s " { x } )
24 23 11 cfv 
 |-  ( vol ` ( s " { x } ) )
25 6 3 24 citg 
 |-  S. RR ( vol ` ( s " { x } ) ) _d x
26 1 21 25 cmpt 
 |-  ( 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 )
27 0 26 wceq 
 |-  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 )