Metamath Proof Explorer

Theorem cnmbfm

Description: A continuous function is measurable with respect to the Borel Algebra of its domain and range. (Contributed by Thierry Arnoux, 3-Jun-2017)

Ref Expression
Hypotheses cnmbfm.1 
|- ( ph -> F e. ( J Cn K ) )
cnmbfm.2 
|- ( ph -> S = ( sigaGen ` J ) )
cnmbfm.3 
|- ( ph -> T = ( sigaGen ` K ) )
Assertion cnmbfm 
|- ( ph -> F e. ( S MblFnM T ) )

Proof

Step Hyp Ref Expression
1 cnmbfm.1 
 |-  ( ph -> F e. ( J Cn K ) )
2 cnmbfm.2 
 |-  ( ph -> S = ( sigaGen ` J ) )
3 cnmbfm.3 
 |-  ( ph -> T = ( sigaGen ` K ) )
4 eqid 
 |-  U. J = U. J
5 eqid 
 |-  U. K = U. K
6 4 5 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> U. K )
7 1 6 syl 
 |-  ( ph -> F : U. J --> U. K )
8 2 unieqd 
 |-  ( ph -> U. S = U. ( sigaGen ` J ) )
9 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
10 unisg 
 |-  ( J e. Top -> U. ( sigaGen ` J ) = U. J )
11 1 9 10 3syl 
 |-  ( ph -> U. ( sigaGen ` J ) = U. J )
12 8 11 eqtrd 
 |-  ( ph -> U. S = U. J )
13 3 unieqd 
 |-  ( ph -> U. T = U. ( sigaGen ` K ) )
14 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
15 unisg 
 |-  ( K e. Top -> U. ( sigaGen ` K ) = U. K )
16 1 14 15 3syl 
 |-  ( ph -> U. ( sigaGen ` K ) = U. K )
17 13 16 eqtrd 
 |-  ( ph -> U. T = U. K )
18 12 17 feq23d 
 |-  ( ph -> ( F : U. S --> U. T <-> F : U. J --> U. K ) )
19 7 18 mpbird 
 |-  ( ph -> F : U. S --> U. T )
20 sssigagen 
 |-  ( J e. Top -> J C_ ( sigaGen ` J ) )
21 1 9 20 3syl 
 |-  ( ph -> J C_ ( sigaGen ` J ) )
22 21 2 sseqtrrd 
 |-  ( ph -> J C_ S )
23 22 adantr 
 |-  ( ( ph /\ a e. K ) -> J C_ S )
24 cnima 
 |-  ( ( F e. ( J Cn K ) /\ a e. K ) -> ( `' F " a ) e. J )
25 1 24 sylan 
 |-  ( ( ph /\ a e. K ) -> ( `' F " a ) e. J )
26 23 25 sseldd 
 |-  ( ( ph /\ a e. K ) -> ( `' F " a ) e. S )
27 26 ralrimiva 
 |-  ( ph -> A. a e. K ( `' F " a ) e. S )
28 elex 
 |-  ( K e. Top -> K e. _V )
29 1 14 28 3syl 
 |-  ( ph -> K e. _V )
30 sigagensiga 
 |-  ( J e. Top -> ( sigaGen ` J ) e. ( sigAlgebra ` U. J ) )
31 1 9 30 3syl 
 |-  ( ph -> ( sigaGen ` J ) e. ( sigAlgebra ` U. J ) )
32 2 31 eqeltrd 
 |-  ( ph -> S e. ( sigAlgebra ` U. J ) )
33 elrnsiga 
 |-  ( S e. ( sigAlgebra ` U. J ) -> S e. U. ran sigAlgebra )
34 32 33 syl 
 |-  ( ph -> S e. U. ran sigAlgebra )
35 29 34 3 imambfm 
 |-  ( ph -> ( F e. ( S MblFnM T ) <-> ( F : U. S --> U. T /\ A. a e. K ( `' F " a ) e. S ) ) )
36 19 27 35 mpbir2and 
 |-  ( ph -> F e. ( S MblFnM T ) )