Metamath Proof Explorer

Theorem 2ndmbfm

Description: The second projection map is measurable with regard to the product sigma-algebra. (Contributed by Thierry Arnoux, 3-Jun-2017)

Ref Expression
Hypotheses 1stmbfm.1 
|- ( ph -> S e. U. ran sigAlgebra )
1stmbfm.2 
|- ( ph -> T e. U. ran sigAlgebra )
Assertion 2ndmbfm 
|- ( ph -> ( 2nd |` ( U. S X. U. T ) ) e. ( ( S sX T ) MblFnM T ) )

Proof

Step Hyp Ref Expression
1 1stmbfm.1 
 |-  ( ph -> S e. U. ran sigAlgebra )
2 1stmbfm.2 
 |-  ( ph -> T e. U. ran sigAlgebra )
3 f2ndres 
 |-  ( 2nd |` ( U. S X. U. T ) ) : ( U. S X. U. T ) --> U. T
4 sxuni 
 |-  ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( U. S X. U. T ) = U. ( S sX T ) )
5 1 2 4 syl2anc 
 |-  ( ph -> ( U. S X. U. T ) = U. ( S sX T ) )
6 5 feq2d 
 |-  ( ph -> ( ( 2nd |` ( U. S X. U. T ) ) : ( U. S X. U. T ) --> U. T <-> ( 2nd |` ( U. S X. U. T ) ) : U. ( S sX T ) --> U. T ) )
7 3 6 mpbii 
 |-  ( ph -> ( 2nd |` ( U. S X. U. T ) ) : U. ( S sX T ) --> U. T )
8 unielsiga 
 |-  ( T e. U. ran sigAlgebra -> U. T e. T )
9 2 8 syl 
 |-  ( ph -> U. T e. T )
10 sxsiga 
 |-  ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( S sX T ) e. U. ran sigAlgebra )
11 1 2 10 syl2anc 
 |-  ( ph -> ( S sX T ) e. U. ran sigAlgebra )
12 unielsiga 
 |-  ( ( S sX T ) e. U. ran sigAlgebra -> U. ( S sX T ) e. ( S sX T ) )
13 11 12 syl 
 |-  ( ph -> U. ( S sX T ) e. ( S sX T ) )
14 9 13 elmapd 
 |-  ( ph -> ( ( 2nd |` ( U. S X. U. T ) ) e. ( U. T ^m U. ( S sX T ) ) <-> ( 2nd |` ( U. S X. U. T ) ) : U. ( S sX T ) --> U. T ) )
15 7 14 mpbird 
 |-  ( ph -> ( 2nd |` ( U. S X. U. T ) ) e. ( U. T ^m U. ( S sX T ) ) )
16 ffn 
 |-  ( ( 2nd |` ( U. S X. U. T ) ) : ( U. S X. U. T ) --> U. T -> ( 2nd |` ( U. S X. U. T ) ) Fn ( U. S X. U. T ) )
17 elpreima 
 |-  ( ( 2nd |` ( U. S X. U. T ) ) Fn ( U. S X. U. T ) -> ( z e. ( `' ( 2nd |` ( U. S X. U. T ) ) " a ) <-> ( z e. ( U. S X. U. T ) /\ ( ( 2nd |` ( U. S X. U. T ) ) ` z ) e. a ) ) )
18 3 16 17 mp2b 
 |-  ( z e. ( `' ( 2nd |` ( U. S X. U. T ) ) " a ) <-> ( z e. ( U. S X. U. T ) /\ ( ( 2nd |` ( U. S X. U. T ) ) ` z ) e. a ) )
19 fvres 
 |-  ( z e. ( U. S X. U. T ) -> ( ( 2nd |` ( U. S X. U. T ) ) ` z ) = ( 2nd ` z ) )
20 19 eleq1d 
 |-  ( z e. ( U. S X. U. T ) -> ( ( ( 2nd |` ( U. S X. U. T ) ) ` z ) e. a <-> ( 2nd ` z ) e. a ) )
21 1st2nd2 
 |-  ( z e. ( U. S X. U. T ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
22 xp1st 
 |-  ( z e. ( U. S X. U. T ) -> ( 1st ` z ) e. U. S )
23 elxp6 
 |-  ( z e. ( U. S X. a ) <-> ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( ( 1st ` z ) e. U. S /\ ( 2nd ` z ) e. a ) ) )
24 anass 
 |-  ( ( ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( 1st ` z ) e. U. S ) /\ ( 2nd ` z ) e. a ) <-> ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( ( 1st ` z ) e. U. S /\ ( 2nd ` z ) e. a ) ) )
25 23 24 bitr4i 
 |-  ( z e. ( U. S X. a ) <-> ( ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( 1st ` z ) e. U. S ) /\ ( 2nd ` z ) e. a ) )
26 25 baib 
 |-  ( ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( 1st ` z ) e. U. S ) -> ( z e. ( U. S X. a ) <-> ( 2nd ` z ) e. a ) )
27 21 22 26 syl2anc 
 |-  ( z e. ( U. S X. U. T ) -> ( z e. ( U. S X. a ) <-> ( 2nd ` z ) e. a ) )
28 20 27 bitr4d 
 |-  ( z e. ( U. S X. U. T ) -> ( ( ( 2nd |` ( U. S X. U. T ) ) ` z ) e. a <-> z e. ( U. S X. a ) ) )
29 28 pm5.32i 
 |-  ( ( z e. ( U. S X. U. T ) /\ ( ( 2nd |` ( U. S X. U. T ) ) ` z ) e. a ) <-> ( z e. ( U. S X. U. T ) /\ z e. ( U. S X. a ) ) )
30 18 29 bitri 
 |-  ( z e. ( `' ( 2nd |` ( U. S X. U. T ) ) " a ) <-> ( z e. ( U. S X. U. T ) /\ z e. ( U. S X. a ) ) )
31 sgon 
 |-  ( T e. U. ran sigAlgebra -> T e. ( sigAlgebra ` U. T ) )
32 sigasspw 
 |-  ( T e. ( sigAlgebra ` U. T ) -> T C_ ~P U. T )
33 pwssb 
 |-  ( T C_ ~P U. T <-> A. a e. T a C_ U. T )
34 33 biimpi 
 |-  ( T C_ ~P U. T -> A. a e. T a C_ U. T )
35 2 31 32 34 4syl 
 |-  ( ph -> A. a e. T a C_ U. T )
36 35 r19.21bi 
 |-  ( ( ph /\ a e. T ) -> a C_ U. T )
37 xpss2 
 |-  ( a C_ U. T -> ( U. S X. a ) C_ ( U. S X. U. T ) )
38 36 37 syl 
 |-  ( ( ph /\ a e. T ) -> ( U. S X. a ) C_ ( U. S X. U. T ) )
39 38 sseld 
 |-  ( ( ph /\ a e. T ) -> ( z e. ( U. S X. a ) -> z e. ( U. S X. U. T ) ) )
40 39 pm4.71rd 
 |-  ( ( ph /\ a e. T ) -> ( z e. ( U. S X. a ) <-> ( z e. ( U. S X. U. T ) /\ z e. ( U. S X. a ) ) ) )
41 30 40 bitr4id 
 |-  ( ( ph /\ a e. T ) -> ( z e. ( `' ( 2nd |` ( U. S X. U. T ) ) " a ) <-> z e. ( U. S X. a ) ) )
42 41 eqrdv 
 |-  ( ( ph /\ a e. T ) -> ( `' ( 2nd |` ( U. S X. U. T ) ) " a ) = ( U. S X. a ) )
43 1 adantr 
 |-  ( ( ph /\ a e. T ) -> S e. U. ran sigAlgebra )
44 2 adantr 
 |-  ( ( ph /\ a e. T ) -> T e. U. ran sigAlgebra )
45 eqid 
 |-  U. S = U. S
46 issgon 
 |-  ( S e. ( sigAlgebra ` U. S ) <-> ( S e. U. ran sigAlgebra /\ U. S = U. S ) )
47 1 45 46 sylanblrc 
 |-  ( ph -> S e. ( sigAlgebra ` U. S ) )
48 baselsiga 
 |-  ( S e. ( sigAlgebra ` U. S ) -> U. S e. S )
49 47 48 syl 
 |-  ( ph -> U. S e. S )
50 49 adantr 
 |-  ( ( ph /\ a e. T ) -> U. S e. S )
51 simpr 
 |-  ( ( ph /\ a e. T ) -> a e. T )
52 elsx 
 |-  ( ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) /\ ( U. S e. S /\ a e. T ) ) -> ( U. S X. a ) e. ( S sX T ) )
53 43 44 50 51 52 syl22anc 
 |-  ( ( ph /\ a e. T ) -> ( U. S X. a ) e. ( S sX T ) )
54 42 53 eqeltrd 
 |-  ( ( ph /\ a e. T ) -> ( `' ( 2nd |` ( U. S X. U. T ) ) " a ) e. ( S sX T ) )
55 54 ralrimiva 
 |-  ( ph -> A. a e. T ( `' ( 2nd |` ( U. S X. U. T ) ) " a ) e. ( S sX T ) )
56 11 2 ismbfm 
 |-  ( ph -> ( ( 2nd |` ( U. S X. U. T ) ) e. ( ( S sX T ) MblFnM T ) <-> ( ( 2nd |` ( U. S X. U. T ) ) e. ( U. T ^m U. ( S sX T ) ) /\ A. a e. T ( `' ( 2nd |` ( U. S X. U. T ) ) " a ) e. ( S sX T ) ) ) )
57 15 55 56 mpbir2and 
 |-  ( ph -> ( 2nd |` ( U. S X. U. T ) ) e. ( ( S sX T ) MblFnM T ) )