Metamath Proof Explorer

Theorem i1fima

Description: Any preimage of a simple function is measurable. (Contributed by Mario Carneiro, 26-Jun-2014)

Ref Expression
Assertion i1fima 
|- ( F e. dom S.1 -> ( `' F " A ) e. dom vol )

Proof

Step Hyp Ref Expression
1 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
2 ffun 
 |-  ( F : RR --> RR -> Fun F )
3 inpreima 
 |-  ( Fun F -> ( `' F " ( A i^i ran F ) ) = ( ( `' F " A ) i^i ( `' F " ran F ) ) )
4 iunid 
 |-  U_ y e. ( A i^i ran F ) { y } = ( A i^i ran F )
5 4 imaeq2i 
 |-  ( `' F " U_ y e. ( A i^i ran F ) { y } ) = ( `' F " ( A i^i ran F ) )
6 imaiun 
 |-  ( `' F " U_ y e. ( A i^i ran F ) { y } ) = U_ y e. ( A i^i ran F ) ( `' F " { y } )
7 5 6 eqtr3i 
 |-  ( `' F " ( A i^i ran F ) ) = U_ y e. ( A i^i ran F ) ( `' F " { y } )
8 cnvimass 
 |-  ( `' F " A ) C_ dom F
9 cnvimarndm 
 |-  ( `' F " ran F ) = dom F
10 8 9 sseqtrri 
 |-  ( `' F " A ) C_ ( `' F " ran F )
11 df-ss 
 |-  ( ( `' F " A ) C_ ( `' F " ran F ) <-> ( ( `' F " A ) i^i ( `' F " ran F ) ) = ( `' F " A ) )
12 10 11 mpbi 
 |-  ( ( `' F " A ) i^i ( `' F " ran F ) ) = ( `' F " A )
13 3 7 12 3eqtr3g 
 |-  ( Fun F -> U_ y e. ( A i^i ran F ) ( `' F " { y } ) = ( `' F " A ) )
14 1 2 13 3syl 
 |-  ( F e. dom S.1 -> U_ y e. ( A i^i ran F ) ( `' F " { y } ) = ( `' F " A ) )
15 i1frn 
 |-  ( F e. dom S.1 -> ran F e. Fin )
16 inss2 
 |-  ( A i^i ran F ) C_ ran F
17 ssfi 
 |-  ( ( ran F e. Fin /\ ( A i^i ran F ) C_ ran F ) -> ( A i^i ran F ) e. Fin )
18 15 16 17 sylancl 
 |-  ( F e. dom S.1 -> ( A i^i ran F ) e. Fin )
19 i1fmbf 
 |-  ( F e. dom S.1 -> F e. MblFn )
20 19 adantr 
 |-  ( ( F e. dom S.1 /\ y e. ( A i^i ran F ) ) -> F e. MblFn )
21 1 adantr 
 |-  ( ( F e. dom S.1 /\ y e. ( A i^i ran F ) ) -> F : RR --> RR )
22 1 frnd 
 |-  ( F e. dom S.1 -> ran F C_ RR )
23 16 22 sstrid 
 |-  ( F e. dom S.1 -> ( A i^i ran F ) C_ RR )
24 23 sselda 
 |-  ( ( F e. dom S.1 /\ y e. ( A i^i ran F ) ) -> y e. RR )
25 mbfimasn 
 |-  ( ( F e. MblFn /\ F : RR --> RR /\ y e. RR ) -> ( `' F " { y } ) e. dom vol )
26 20 21 24 25 syl3anc 
 |-  ( ( F e. dom S.1 /\ y e. ( A i^i ran F ) ) -> ( `' F " { y } ) e. dom vol )
27 26 ralrimiva 
 |-  ( F e. dom S.1 -> A. y e. ( A i^i ran F ) ( `' F " { y } ) e. dom vol )
28 finiunmbl 
 |-  ( ( ( A i^i ran F ) e. Fin /\ A. y e. ( A i^i ran F ) ( `' F " { y } ) e. dom vol ) -> U_ y e. ( A i^i ran F ) ( `' F " { y } ) e. dom vol )
29 18 27 28 syl2anc 
 |-  ( F e. dom S.1 -> U_ y e. ( A i^i ran F ) ( `' F " { y } ) e. dom vol )
30 14 29 eqeltrrd 
 |-  ( F e. dom S.1 -> ( `' F " A ) e. dom vol )