Theorem 1stmbfm 24563

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

Hypotheses

Ref	Expression
1stmbfm.1	|- ( ph -> S e. U. ran sigAlgebra )
1stmbfm.2	|- ( ph -> T e. U. ran sigAlgebra )

Assertion

Ref	Expression
1stmbfm	|- ( ph -> ( 1st |` ( U. S X. U. T ) ) e. ( ( S ×s T )MblFnM S ) )

Proof of Theorem 1stmbfm

Dummy variables z a are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1stres 6327	. . . 4 |- ( 1st |` ( U. S X. U. T ) ) : ( U. S X. U. T ) --> U. S
2		1stmbfm.1	. . . . . 6 |- ( ph -> S e. U. ran sigAlgebra )
3		1stmbfm.2	. . . . . 6 |- ( ph -> T e. U. ran sigAlgebra )
4		sxuni 24500	. . . . . 6 |- ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( U. S X. U. T ) = U. ( S ×s T ) )
5	2, 3, 4	syl2anc 643	. . . . 5 |- ( ph -> ( U. S X. U. T ) = U. ( S ×s T ) )
6	5	feq2d 5540	. . . 4 |- ( ph -> ( ( 1st |` ( U. S X. U. T ) ) : ( U. S X. U. T ) --> U. S <-> ( 1st |` ( U. S X. U. T ) ) : U. ( S ×s T ) --> U. S ) )
7	1, 6	mpbii 203	. . 3 |- ( ph -> ( 1st |` ( U. S X. U. T ) ) : U. ( S ×s T ) --> U. S )
8		unielsiga 24464	. . . . 5 |- ( S e. U. ran sigAlgebra -> U. S e. S )
9	2, 8	syl 16	. . . 4 |- ( ph -> U. S e. S )
10		sxsiga 24498	. . . . . 6 |- ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( S ×s T ) e. U. ran sigAlgebra )
11	2, 3, 10	syl2anc 643	. . . . 5 |- ( ph -> ( S ×s T ) e. U. ran sigAlgebra )
12		unielsiga 24464	. . . . 5 |- ( ( S ×s T ) e. U. ran sigAlgebra -> U. ( S ×s T ) e. ( S ×s T ) )
13	11, 12	syl 16	. . . 4 |- ( ph -> U. ( S ×s T ) e. ( S ×s T ) )
14		elmapg 6990	. . . 4 |- ( ( U. S e. S /\ U. ( S ×s T ) e. ( S ×s T ) ) -> ( ( 1st |` ( U. S X. U. T ) ) e. ( U. S ^m U. ( S ×s T ) ) <-> ( 1st |` ( U. S X. U. T ) ) : U. ( S ×s T ) --> U. S ) )
15	9, 13, 14	syl2anc 643	. . 3 |- ( ph -> ( ( 1st |` ( U. S X. U. T ) ) e. ( U. S ^m U. ( S ×s T ) ) <-> ( 1st |` ( U. S X. U. T ) ) : U. ( S ×s T ) --> U. S ) )
16	7, 15	mpbird 224	. 2 |- ( ph -> ( 1st |` ( U. S X. U. T ) ) e. ( U. S ^m U. ( S ×s T ) ) )
17		sgon 24460	. . . . . . . . . . . 12 |- ( S e. U. ran sigAlgebra -> S e. (sigAlgebra ` U. S ) )
18	2, 17	syl 16	. . . . . . . . . . 11 |- ( ph -> S e. (sigAlgebra ` U. S ) )
19		sigasspw 24452	. . . . . . . . . . 11 |- ( S e. (sigAlgebra ` U. S ) -> S C_ ~P U. S )
20		pwssb 4137	. . . . . . . . . . . 12 |- ( S C_ ~P U. S <-> A. a e. S a C_ U. S )
21	20	biimpi 187	. . . . . . . . . . 11 |- ( S C_ ~P U. S -> A. a e. S a C_ U. S )
22	18, 19, 21	3syl 19	. . . . . . . . . 10 |- ( ph -> A. a e. S a C_ U. S )
23	22	r19.21bi 2764	. . . . . . . . 9 |- ( ( ph /\ a e. S ) -> a C_ U. S )
24		xpss1 4943	. . . . . . . . 9 |- ( a C_ U. S -> ( a X. U. T ) C_ ( U. S X. U. T ) )
25	23, 24	syl 16	. . . . . . . 8 |- ( ( ph /\ a e. S ) -> ( a X. U. T ) C_ ( U. S X. U. T ) )
26	25	sseld 3307	. . . . . . 7 |- ( ( ph /\ a e. S ) -> ( z e. ( a X. U. T ) -> z e. ( U. S X. U. T ) ) )
27	26	pm4.71rd 617	. . . . . 6 |- ( ( ph /\ a e. S ) -> ( z e. ( a X. U. T ) <-> ( z e. ( U. S X. U. T ) /\ z e. ( a X. U. T ) ) ) )
28		ffn 5550	. . . . . . . 8 |- ( ( 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 ) )
29		elpreima 5809	. . . . . . . 8 |- ( ( 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 ) ) )
30	1, 28, 29	mp2b 10	. . . . . . 7 |- ( 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 ) )
31		fvres 5704	. . . . . . . . . 10 |- ( z e. ( U. S X. U. T ) -> ( ( 1st |` ( U. S X. U. T ) ) ` z ) = ( 1st ` z ) )
32	31	eleq1d 2470	. . . . . . . . 9 |- ( z e. ( U. S X. U. T ) -> ( ( ( 1st |` ( U. S X. U. T ) ) ` z ) e. a <-> ( 1st ` z ) e. a ) )
33		1st2nd2 6345	. . . . . . . . . 10 |- ( z e. ( U. S X. U. T ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
34		xp2nd 6336	. . . . . . . . . 10 |- ( z e. ( U. S X. U. T ) -> ( 2nd ` z ) e. U. T )
35		elxp6 6337	. . . . . . . . . . . 12 |- ( z e. ( a X. U. T ) <-> ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( ( 1st ` z ) e. a /\ ( 2nd ` z ) e. U. T ) ) )
36		anass 631	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
37		an32 774	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
38	35, 36, 37	3bitr2i 265	. . . . . . . . . . 11 |- ( z e. ( a X. U. T ) <-> ( ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( 2nd ` z ) e. U. T ) /\ ( 1st ` z ) e. a ) )
39	38	baib 872	. . . . . . . . . 10 |- ( ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( 2nd ` z ) e. U. T ) -> ( z e. ( a X. U. T ) <-> ( 1st ` z ) e. a ) )
40	33, 34, 39	syl2anc 643	. . . . . . . . 9 |- ( z e. ( U. S X. U. T ) -> ( z e. ( a X. U. T ) <-> ( 1st ` z ) e. a ) )
41	32, 40	bitr4d 248	. . . . . . . 8 |- ( z e. ( U. S X. U. T ) -> ( ( ( 1st |` ( U. S X. U. T ) ) ` z ) e. a <-> z e. ( a X. U. T ) ) )
42	41	pm5.32i 619	. . . . . . 7 |- ( ( 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 ) ) )
43	30, 42	bitri 241	. . . . . 6 |- ( z e. ( `' ( 1st |` ( U. S X. U. T ) ) " a ) <-> ( z e. ( U. S X. U. T ) /\ z e. ( a X. U. T ) ) )
44	27, 43	syl6rbbr 256	. . . . 5 |- ( ( ph /\ a e. S ) -> ( z e. ( `' ( 1st |` ( U. S X. U. T ) ) " a ) <-> z e. ( a X. U. T ) ) )
45	44	eqrdv 2402	. . . 4 |- ( ( ph /\ a e. S ) -> ( `' ( 1st |` ( U. S X. U. T ) ) " a ) = ( a X. U. T ) )
46	2	adantr 452	. . . . 5 |- ( ( ph /\ a e. S ) -> S e. U. ran sigAlgebra )
47	3	adantr 452	. . . . 5 |- ( ( ph /\ a e. S ) -> T e. U. ran sigAlgebra )
48		simpr 448	. . . . 5 |- ( ( ph /\ a e. S ) -> a e. S )
49		eqid 2404	. . . . . . . 8 |- U. T = U. T
50		issgon 24459	. . . . . . . . 9 |- ( T e. (sigAlgebra ` U. T ) <-> ( T e. U. ran sigAlgebra /\ U. T = U. T ) )
51	50	biimpri 198	. . . . . . . 8 |- ( ( T e. U. ran sigAlgebra /\ U. T = U. T ) -> T e. (sigAlgebra ` U. T ) )
52	3, 49, 51	sylancl 644	. . . . . . 7 |- ( ph -> T e. (sigAlgebra ` U. T ) )
53		baselsiga 24451	. . . . . . 7 |- ( T e. (sigAlgebra ` U. T ) -> U. T e. T )
54	52, 53	syl 16	. . . . . 6 |- ( ph -> U. T e. T )
55	54	adantr 452	. . . . 5 |- ( ( ph /\ a e. S ) -> U. T e. T )
56		elsx 24501	. . . . 5 |- ( ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) /\ ( a e. S /\ U. T e. T ) ) -> ( a X. U. T ) e. ( S ×s T ) )
57	46, 47, 48, 55, 56	syl22anc 1185	. . . 4 |- ( ( ph /\ a e. S ) -> ( a X. U. T ) e. ( S ×s T ) )
58	45, 57	eqeltrd 2478	. . 3 |- ( ( ph /\ a e. S ) -> ( `' ( 1st |` ( U. S X. U. T ) ) " a ) e. ( S ×s T ) )
59	58	ralrimiva 2749	. 2 |- ( ph -> A. a e. S ( `' ( 1st |` ( U. S X. U. T ) ) " a ) e. ( S ×s T ) )
60	11, 2	ismbfm 24555	. 2 |- ( ph -> ( ( 1st |` ( U. S X. U. T ) ) e. ( ( S ×s T )MblFnM S ) <-> ( ( 1st |` ( U. S X. U. T ) ) e. ( U. S ^m U. ( S ×s T ) ) /\ A. a e. S ( `' ( 1st |` ( U. S X. U. T ) ) " a ) e. ( S ×s T ) ) ) )
61	16, 59, 60	mpbir2and 889	1 |- ( ph -> ( 1st |` ( U. S X. U. T ) ) e. ( ( S ×s T )MblFnM S ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   A.wral 2666   C_ wss 3280   ~Pcpw 3759   <.cop 3777   U.cuni 3975   X. cxp 4835   `'ccnv 4836   ran crn 4838   |` cres 4839   "cima 4840   Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040   1stc1st 6306   2ndc2nd 6307   ^m cmap 6977  sigAlgebracsiga 24443   ×_s csx 24495  MblFnMcmbfm 24553

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-map 6979  df-siga 24444  df-sigagen 24475  df-sx 24496  df-mbfm 24554