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 )