Metamath Proof Explorer

Theorem mbfimaopn2

Description: The preimage of any set open in the subspace topology of the range of the function is measurable. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses mbfimaopn.1 
|- J = ( TopOpen ` CCfld )
mbfimaopn2.2 
|- K = ( J |`t B )
Assertion mbfimaopn2 
|- ( ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) /\ C e. K ) -> ( `' F " C ) e. dom vol )

Proof

Step Hyp Ref Expression
1 mbfimaopn.1 
 |-  J = ( TopOpen ` CCfld )
2 mbfimaopn2.2 
 |-  K = ( J |`t B )
3 2 eleq2i 
 |-  ( C e. K <-> C e. ( J |`t B ) )
4 1 cnfldtop 
 |-  J e. Top
5 simp3 
 |-  ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) -> B C_ CC )
6 cnex 
 |-  CC e. _V
7 ssexg 
 |-  ( ( B C_ CC /\ CC e. _V ) -> B e. _V )
8 5 6 7 sylancl 
 |-  ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) -> B e. _V )
9 elrest 
 |-  ( ( J e. Top /\ B e. _V ) -> ( C e. ( J |`t B ) <-> E. u e. J C = ( u i^i B ) ) )
10 4 8 9 sylancr 
 |-  ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) -> ( C e. ( J |`t B ) <-> E. u e. J C = ( u i^i B ) ) )
11 3 10 bitrid 
 |-  ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) -> ( C e. K <-> E. u e. J C = ( u i^i B ) ) )
12 simpl2 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) /\ u e. J ) -> F : A --> B )
13 ffun 
 |-  ( F : A --> B -> Fun F )
14 inpreima 
 |-  ( Fun F -> ( `' F " ( u i^i B ) ) = ( ( `' F " u ) i^i ( `' F " B ) ) )
15 12 13 14 3syl 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) /\ u e. J ) -> ( `' F " ( u i^i B ) ) = ( ( `' F " u ) i^i ( `' F " B ) ) )
16 1 mbfimaopn 
 |-  ( ( F e. MblFn /\ u e. J ) -> ( `' F " u ) e. dom vol )
17 16 3ad2antl1 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) /\ u e. J ) -> ( `' F " u ) e. dom vol )
18 fimacnv 
 |-  ( F : A --> B -> ( `' F " B ) = A )
19 fdm 
 |-  ( F : A --> B -> dom F = A )
20 18 19 eqtr4d 
 |-  ( F : A --> B -> ( `' F " B ) = dom F )
21 12 20 syl 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) /\ u e. J ) -> ( `' F " B ) = dom F )
22 simpl1 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) /\ u e. J ) -> F e. MblFn )
23 mbfdm 
 |-  ( F e. MblFn -> dom F e. dom vol )
24 22 23 syl 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) /\ u e. J ) -> dom F e. dom vol )
25 21 24 eqeltrd 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) /\ u e. J ) -> ( `' F " B ) e. dom vol )
26 inmbl 
 |-  ( ( ( `' F " u ) e. dom vol /\ ( `' F " B ) e. dom vol ) -> ( ( `' F " u ) i^i ( `' F " B ) ) e. dom vol )
27 17 25 26 syl2anc 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) /\ u e. J ) -> ( ( `' F " u ) i^i ( `' F " B ) ) e. dom vol )
28 15 27 eqeltrd 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) /\ u e. J ) -> ( `' F " ( u i^i B ) ) e. dom vol )
29 imaeq2 
 |-  ( C = ( u i^i B ) -> ( `' F " C ) = ( `' F " ( u i^i B ) ) )
30 29 eleq1d 
 |-  ( C = ( u i^i B ) -> ( ( `' F " C ) e. dom vol <-> ( `' F " ( u i^i B ) ) e. dom vol ) )
31 28 30 syl5ibrcom 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) /\ u e. J ) -> ( C = ( u i^i B ) -> ( `' F " C ) e. dom vol ) )
32 31 rexlimdva 
 |-  ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) -> ( E. u e. J C = ( u i^i B ) -> ( `' F " C ) e. dom vol ) )
33 11 32 sylbid 
 |-  ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) -> ( C e. K -> ( `' F " C ) e. dom vol ) )
34 33 imp 
 |-  ( ( ( F e. MblFn /\ F : A --> B /\ B C_ CC ) /\ C e. K ) -> ( `' F " C ) e. dom vol )