Metamath Proof Explorer

Theorem mbfimaicc

Description: The preimage of any closed interval under a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion mbfimaicc 
|- ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR /\ C e. RR ) ) -> ( `' F " ( B [,] C ) ) e. dom vol )

Proof

Step Hyp Ref Expression
1 iccssre 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B [,] C ) C_ RR )
2 1 adantl 
 |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR /\ C e. RR ) ) -> ( B [,] C ) C_ RR )
3 dfss4 
 |-  ( ( B [,] C ) C_ RR <-> ( RR \ ( RR \ ( B [,] C ) ) ) = ( B [,] C ) )
4 2 3 sylib 
 |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR /\ C e. RR ) ) -> ( RR \ ( RR \ ( B [,] C ) ) ) = ( B [,] C ) )
5 difreicc 
 |-  ( ( B e. RR /\ C e. RR ) -> ( RR \ ( B [,] C ) ) = ( ( -oo (,) B ) u. ( C (,) +oo ) ) )
6 5 adantl 
 |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR /\ C e. RR ) ) -> ( RR \ ( B [,] C ) ) = ( ( -oo (,) B ) u. ( C (,) +oo ) ) )
7 6 difeq2d 
 |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR /\ C e. RR ) ) -> ( RR \ ( RR \ ( B [,] C ) ) ) = ( RR \ ( ( -oo (,) B ) u. ( C (,) +oo ) ) ) )
8 4 7 eqtr3d 
 |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR /\ C e. RR ) ) -> ( B [,] C ) = ( RR \ ( ( -oo (,) B ) u. ( C (,) +oo ) ) ) )
9 8 imaeq2d 
 |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR /\ C e. RR ) ) -> ( `' F " ( B [,] C ) ) = ( `' F " ( RR \ ( ( -oo (,) B ) u. ( C (,) +oo ) ) ) ) )
10 ffun 
 |-  ( F : A --> RR -> Fun F )
11 funcnvcnv 
 |-  ( Fun F -> Fun `' `' F )
12 10 11 syl 
 |-  ( F : A --> RR -> Fun `' `' F )
13 12 ad2antlr 
 |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR /\ C e. RR ) ) -> Fun `' `' F )
14 imadif 
 |-  ( Fun `' `' F -> ( `' F " ( RR \ ( ( -oo (,) B ) u. ( C (,) +oo ) ) ) ) = ( ( `' F " RR ) \ ( `' F " ( ( -oo (,) B ) u. ( C (,) +oo ) ) ) ) )
15 13 14 syl 
 |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR /\ C e. RR ) ) -> ( `' F " ( RR \ ( ( -oo (,) B ) u. ( C (,) +oo ) ) ) ) = ( ( `' F " RR ) \ ( `' F " ( ( -oo (,) B ) u. ( C (,) +oo ) ) ) ) )
16 9 15 eqtrd 
 |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR /\ C e. RR ) ) -> ( `' F " ( B [,] C ) ) = ( ( `' F " RR ) \ ( `' F " ( ( -oo (,) B ) u. ( C (,) +oo ) ) ) ) )
17 fimacnv 
 |-  ( F : A --> RR -> ( `' F " RR ) = A )
18 17 adantl 
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " RR ) = A )
19 mbfdm 
 |-  ( F e. MblFn -> dom F e. dom vol )
20 fdm 
 |-  ( F : A --> RR -> dom F = A )
21 20 eleq1d 
 |-  ( F : A --> RR -> ( dom F e. dom vol <-> A e. dom vol ) )
22 21 biimpac 
 |-  ( ( dom F e. dom vol /\ F : A --> RR ) -> A e. dom vol )
23 19 22 sylan 
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> A e. dom vol )
24 18 23 eqeltrd 
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " RR ) e. dom vol )
25 imaundi 
 |-  ( `' F " ( ( -oo (,) B ) u. ( C (,) +oo ) ) ) = ( ( `' F " ( -oo (,) B ) ) u. ( `' F " ( C (,) +oo ) ) )
26 mbfima 
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " ( -oo (,) B ) ) e. dom vol )
27 mbfima 
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " ( C (,) +oo ) ) e. dom vol )
28 unmbl 
 |-  ( ( ( `' F " ( -oo (,) B ) ) e. dom vol /\ ( `' F " ( C (,) +oo ) ) e. dom vol ) -> ( ( `' F " ( -oo (,) B ) ) u. ( `' F " ( C (,) +oo ) ) ) e. dom vol )
29 26 27 28 syl2anc 
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( ( `' F " ( -oo (,) B ) ) u. ( `' F " ( C (,) +oo ) ) ) e. dom vol )
30 25 29 eqeltrid 
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( `' F " ( ( -oo (,) B ) u. ( C (,) +oo ) ) ) e. dom vol )
31 difmbl 
 |-  ( ( ( `' F " RR ) e. dom vol /\ ( `' F " ( ( -oo (,) B ) u. ( C (,) +oo ) ) ) e. dom vol ) -> ( ( `' F " RR ) \ ( `' F " ( ( -oo (,) B ) u. ( C (,) +oo ) ) ) ) e. dom vol )
32 24 30 31 syl2anc 
 |-  ( ( F e. MblFn /\ F : A --> RR ) -> ( ( `' F " RR ) \ ( `' F " ( ( -oo (,) B ) u. ( C (,) +oo ) ) ) ) e. dom vol )
33 32 adantr 
 |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR /\ C e. RR ) ) -> ( ( `' F " RR ) \ ( `' F " ( ( -oo (,) B ) u. ( C (,) +oo ) ) ) ) e. dom vol )
34 16 33 eqeltrd 
 |-  ( ( ( F e. MblFn /\ F : A --> RR ) /\ ( B e. RR /\ C e. RR ) ) -> ( `' F " ( B [,] C ) ) e. dom vol )