Metamath Proof Explorer

Theorem cnmbf

Description: A continuous function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014) (Revised by Mario Carneiro, 26-Mar-2015)

Ref Expression
Assertion cnmbf 
|- ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) -> F e. MblFn )

Proof

Step Hyp Ref Expression
1 cncff 
 |-  ( F e. ( A -cn-> CC ) -> F : A --> CC )
2 mblss 
 |-  ( A e. dom vol -> A C_ RR )
3 cnex 
 |-  CC e. _V
4 reex 
 |-  RR e. _V
5 elpm2r 
 |-  ( ( ( CC e. _V /\ RR e. _V ) /\ ( F : A --> CC /\ A C_ RR ) ) -> F e. ( CC ^pm RR ) )
6 3 4 5 mpanl12 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> F e. ( CC ^pm RR ) )
7 1 2 6 syl2anr 
 |-  ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) -> F e. ( CC ^pm RR ) )
8 simpll 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> A e. dom vol )
9 simplr 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> F e. ( A -cn-> CC ) )
10 recncf 
 |-  Re e. ( CC -cn-> RR )
11 10 a1i 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> Re e. ( CC -cn-> RR ) )
12 9 11 cncfco 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> ( Re o. F ) e. ( A -cn-> RR ) )
13 2 ad2antrr 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> A C_ RR )
14 ax-resscn 
 |-  RR C_ CC
15 13 14 sstrdi 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> A C_ CC )
16 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
17 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t A ) = ( ( TopOpen ` CCfld ) |`t A )
18 16 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
19 16 17 18 cncfcn 
 |-  ( ( A C_ CC /\ RR C_ CC ) -> ( A -cn-> RR ) = ( ( ( TopOpen ` CCfld ) |`t A ) Cn ( topGen ` ran (,) ) ) )
20 15 14 19 sylancl 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> ( A -cn-> RR ) = ( ( ( TopOpen ` CCfld ) |`t A ) Cn ( topGen ` ran (,) ) ) )
21 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
22 16 21 rerest 
 |-  ( A C_ RR -> ( ( TopOpen ` CCfld ) |`t A ) = ( ( topGen ` ran (,) ) |`t A ) )
23 13 22 syl 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> ( ( TopOpen ` CCfld ) |`t A ) = ( ( topGen ` ran (,) ) |`t A ) )
24 23 oveq1d 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> ( ( ( TopOpen ` CCfld ) |`t A ) Cn ( topGen ` ran (,) ) ) = ( ( ( topGen ` ran (,) ) |`t A ) Cn ( topGen ` ran (,) ) ) )
25 20 24 eqtrd 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> ( A -cn-> RR ) = ( ( ( topGen ` ran (,) ) |`t A ) Cn ( topGen ` ran (,) ) ) )
26 12 25 eleqtrd 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> ( Re o. F ) e. ( ( ( topGen ` ran (,) ) |`t A ) Cn ( topGen ` ran (,) ) ) )
27 retopbas 
 |-  ran (,) e. TopBases
28 bastg 
 |-  ( ran (,) e. TopBases -> ran (,) C_ ( topGen ` ran (,) ) )
29 27 28 ax-mp 
 |-  ran (,) C_ ( topGen ` ran (,) )
30 simpr 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> x e. ran (,) )
31 29 30 sseldi 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> x e. ( topGen ` ran (,) ) )
32 cnima 
 |-  ( ( ( Re o. F ) e. ( ( ( topGen ` ran (,) ) |`t A ) Cn ( topGen ` ran (,) ) ) /\ x e. ( topGen ` ran (,) ) ) -> ( `' ( Re o. F ) " x ) e. ( ( topGen ` ran (,) ) |`t A ) )
33 26 31 32 syl2anc 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> ( `' ( Re o. F ) " x ) e. ( ( topGen ` ran (,) ) |`t A ) )
34 eqid 
 |-  ( ( topGen ` ran (,) ) |`t A ) = ( ( topGen ` ran (,) ) |`t A )
35 34 subopnmbl 
 |-  ( ( A e. dom vol /\ ( `' ( Re o. F ) " x ) e. ( ( topGen ` ran (,) ) |`t A ) ) -> ( `' ( Re o. F ) " x ) e. dom vol )
36 8 33 35 syl2anc 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> ( `' ( Re o. F ) " x ) e. dom vol )
37 imcncf 
 |-  Im e. ( CC -cn-> RR )
38 37 a1i 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> Im e. ( CC -cn-> RR ) )
39 9 38 cncfco 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> ( Im o. F ) e. ( A -cn-> RR ) )
40 39 25 eleqtrd 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> ( Im o. F ) e. ( ( ( topGen ` ran (,) ) |`t A ) Cn ( topGen ` ran (,) ) ) )
41 cnima 
 |-  ( ( ( Im o. F ) e. ( ( ( topGen ` ran (,) ) |`t A ) Cn ( topGen ` ran (,) ) ) /\ x e. ( topGen ` ran (,) ) ) -> ( `' ( Im o. F ) " x ) e. ( ( topGen ` ran (,) ) |`t A ) )
42 40 31 41 syl2anc 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> ( `' ( Im o. F ) " x ) e. ( ( topGen ` ran (,) ) |`t A ) )
43 34 subopnmbl 
 |-  ( ( A e. dom vol /\ ( `' ( Im o. F ) " x ) e. ( ( topGen ` ran (,) ) |`t A ) ) -> ( `' ( Im o. F ) " x ) e. dom vol )
44 8 42 43 syl2anc 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> ( `' ( Im o. F ) " x ) e. dom vol )
45 36 44 jca 
 |-  ( ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) /\ x e. ran (,) ) -> ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) )
46 45 ralrimiva 
 |-  ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) -> A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) )
47 ismbf1 
 |-  ( F e. MblFn <-> ( F e. ( CC ^pm RR ) /\ A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) )
48 7 46 47 sylanbrc 
 |-  ( ( A e. dom vol /\ F e. ( A -cn-> CC ) ) -> F e. MblFn )