Metamath Proof Explorer

Theorem areambl

Description: The fibers of a measurable region are finitely measurable subsets of RR . (Contributed by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion areambl 
|- ( ( S e. dom area /\ A e. RR ) -> ( ( S " { A } ) e. dom vol /\ ( vol ` ( S " { A } ) ) e. RR ) )

Proof

Step Hyp Ref Expression
1 dmarea 
 |-  ( S e. dom area <-> ( S C_ ( RR X. RR ) /\ A. x e. RR ( S " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1 ) )
2 1 simp2bi 
 |-  ( S e. dom area -> A. x e. RR ( S " { x } ) e. ( `' vol " RR ) )
3 sneq 
 |-  ( x = A -> { x } = { A } )
4 3 imaeq2d 
 |-  ( x = A -> ( S " { x } ) = ( S " { A } ) )
5 4 eleq1d 
 |-  ( x = A -> ( ( S " { x } ) e. ( `' vol " RR ) <-> ( S " { A } ) e. ( `' vol " RR ) ) )
6 5 rspccva 
 |-  ( ( A. x e. RR ( S " { x } ) e. ( `' vol " RR ) /\ A e. RR ) -> ( S " { A } ) e. ( `' vol " RR ) )
7 2 6 sylan 
 |-  ( ( S e. dom area /\ A e. RR ) -> ( S " { A } ) e. ( `' vol " RR ) )
8 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
9 ffn 
 |-  ( vol : dom vol --> ( 0 [,] +oo ) -> vol Fn dom vol )
10 elpreima 
 |-  ( vol Fn dom vol -> ( ( S " { A } ) e. ( `' vol " RR ) <-> ( ( S " { A } ) e. dom vol /\ ( vol ` ( S " { A } ) ) e. RR ) ) )
11 8 9 10 mp2b 
 |-  ( ( S " { A } ) e. ( `' vol " RR ) <-> ( ( S " { A } ) e. dom vol /\ ( vol ` ( S " { A } ) ) e. RR ) )
12 7 11 sylib 
 |-  ( ( S e. dom area /\ A e. RR ) -> ( ( S " { A } ) e. dom vol /\ ( vol ` ( S " { A } ) ) e. RR ) )