Metamath Proof Explorer

Theorem 1stmbfm

Description: The first 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 1stmbfm 
|- ( ph -> ( 1st |` ( U. S X. U. T ) ) e. ( ( S sX T ) MblFnM S ) )

Proof

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