Step |
Hyp |
Ref |
Expression |
1 |
|
itgex |
|- S. RR ( vol ` ( s " { x } ) ) _d x e. _V |
2 |
|
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 ) |
3 |
1 2
|
dmmpti |
|- dom area = { t e. ~P ( RR X. RR ) | ( A. x e. RR ( t " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( t " { x } ) ) ) e. L^1 ) } |
4 |
3
|
eleq2i |
|- ( A e. dom area <-> A 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 ) } ) |
5 |
|
imaeq1 |
|- ( t = A -> ( t " { x } ) = ( A " { x } ) ) |
6 |
5
|
eleq1d |
|- ( t = A -> ( ( t " { x } ) e. ( `' vol " RR ) <-> ( A " { x } ) e. ( `' vol " RR ) ) ) |
7 |
6
|
ralbidv |
|- ( t = A -> ( A. x e. RR ( t " { x } ) e. ( `' vol " RR ) <-> A. x e. RR ( A " { x } ) e. ( `' vol " RR ) ) ) |
8 |
5
|
fveq2d |
|- ( t = A -> ( vol ` ( t " { x } ) ) = ( vol ` ( A " { x } ) ) ) |
9 |
8
|
mpteq2dv |
|- ( t = A -> ( x e. RR |-> ( vol ` ( t " { x } ) ) ) = ( x e. RR |-> ( vol ` ( A " { x } ) ) ) ) |
10 |
9
|
eleq1d |
|- ( t = A -> ( ( x e. RR |-> ( vol ` ( t " { x } ) ) ) e. L^1 <-> ( x e. RR |-> ( vol ` ( A " { x } ) ) ) e. L^1 ) ) |
11 |
7 10
|
anbi12d |
|- ( t = A -> ( ( A. x e. RR ( t " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( t " { x } ) ) ) e. L^1 ) <-> ( A. x e. RR ( A " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( A " { x } ) ) ) e. L^1 ) ) ) |
12 |
11
|
elrab |
|- ( A 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 ) } <-> ( A e. ~P ( RR X. RR ) /\ ( A. x e. RR ( A " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( A " { x } ) ) ) e. L^1 ) ) ) |
13 |
|
reex |
|- RR e. _V |
14 |
13 13
|
xpex |
|- ( RR X. RR ) e. _V |
15 |
14
|
elpw2 |
|- ( A e. ~P ( RR X. RR ) <-> A C_ ( RR X. RR ) ) |
16 |
15
|
anbi1i |
|- ( ( A e. ~P ( RR X. RR ) /\ ( A. x e. RR ( A " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( A " { x } ) ) ) e. L^1 ) ) <-> ( A C_ ( RR X. RR ) /\ ( A. x e. RR ( A " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( A " { x } ) ) ) e. L^1 ) ) ) |
17 |
|
3anass |
|- ( ( A C_ ( RR X. RR ) /\ A. x e. RR ( A " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( A " { x } ) ) ) e. L^1 ) <-> ( A C_ ( RR X. RR ) /\ ( A. x e. RR ( A " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( A " { x } ) ) ) e. L^1 ) ) ) |
18 |
16 17
|
bitr4i |
|- ( ( A e. ~P ( RR X. RR ) /\ ( A. x e. RR ( A " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( A " { x } ) ) ) e. L^1 ) ) <-> ( A C_ ( RR X. RR ) /\ A. x e. RR ( A " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( A " { x } ) ) ) e. L^1 ) ) |
19 |
4 12 18
|
3bitri |
|- ( A e. dom area <-> ( A C_ ( RR X. RR ) /\ A. x e. RR ( A " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( A " { x } ) ) ) e. L^1 ) ) |