Theorem 2ndmbfm 26676

Description: The second 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
2ndmbfm	|- ( ph -> ( 2nd |` ( U. S X. U. T ) ) e. ( ( S ×s T )MblFnM T ) )

Proof of Theorem 2ndmbfm

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

Step	Hyp	Ref	Expression
1		f2ndres 6599	. . . 4 |- ( 2nd |` ( U. S X. U. T ) ) : ( U. S X. U. T ) --> U. T
2		1stmbfm.1	. . . . . 6 |- ( ph -> S e. U. ran sigAlgebra )
3		1stmbfm.2	. . . . . 6 |- ( ph -> T e. U. ran sigAlgebra )
4		sxuni 26607	. . . . . 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 661	. . . . 5 |- ( ph -> ( U. S X. U. T ) = U. ( S ×s T ) )
6	5	feq2d 5547	. . . 4 |- ( ph -> ( ( 2nd |` ( U. S X. U. T ) ) : ( U. S X. U. T ) --> U. T <-> ( 2nd |` ( U. S X. U. T ) ) : U. ( S ×s T ) --> U. T ) )
7	1, 6	mpbii 211	. . 3 |- ( ph -> ( 2nd |` ( U. S X. U. T ) ) : U. ( S ×s T ) --> U. T )
8		unielsiga 26571	. . . . 5 |- ( T e. U. ran sigAlgebra -> U. T e. T )
9	3, 8	syl 16	. . . 4 |- ( ph -> U. T e. T )
10		sxsiga 26605	. . . . . 6 |- ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( S ×s T ) e. U. ran sigAlgebra )
11	2, 3, 10	syl2anc 661	. . . . 5 |- ( ph -> ( S ×s T ) e. U. ran sigAlgebra )
12		unielsiga 26571	. . . . 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 7227	. . . 4 |- ( ( U. T e. T /\ U. ( S ×s T ) e. ( S ×s T ) ) -> ( ( 2nd |` ( U. S X. U. T ) ) e. ( U. T ^m U. ( S ×s T ) ) <-> ( 2nd |` ( U. S X. U. T ) ) : U. ( S ×s T ) --> U. T ) )
15	9, 13, 14	syl2anc 661	. . 3 |- ( ph -> ( ( 2nd |` ( U. S X. U. T ) ) e. ( U. T ^m U. ( S ×s T ) ) <-> ( 2nd |` ( U. S X. U. T ) ) : U. ( S ×s T ) --> U. T ) )
16	7, 15	mpbird 232	. 2 |- ( ph -> ( 2nd |` ( U. S X. U. T ) ) e. ( U. T ^m U. ( S ×s T ) ) )
17		sgon 26567	. . . . . . . . . . 11 |- ( T e. U. ran sigAlgebra -> T e. (sigAlgebra ` U. T ) )
18		sigasspw 26559	. . . . . . . . . . 11 |- ( T e. (sigAlgebra ` U. T ) -> T C_ ~P U. T )
19		pwssb 4257	. . . . . . . . . . . 12 |- ( T C_ ~P U. T <-> A. a e. T a C_ U. T )
20	19	biimpi 194	. . . . . . . . . . 11 |- ( T C_ ~P U. T -> A. a e. T a C_ U. T )
21	3, 17, 18, 20	4syl 21	. . . . . . . . . 10 |- ( ph -> A. a e. T a C_ U. T )
22	21	r19.21bi 2814	. . . . . . . . 9 |- ( ( ph /\ a e. T ) -> a C_ U. T )
23		xpss2 4949	. . . . . . . . 9 |- ( a C_ U. T -> ( U. S X. a ) C_ ( U. S X. U. T ) )
24	22, 23	syl 16	. . . . . . . 8 |- ( ( ph /\ a e. T ) -> ( U. S X. a ) C_ ( U. S X. U. T ) )
25	24	sseld 3355	. . . . . . 7 |- ( ( ph /\ a e. T ) -> ( z e. ( U. S X. a ) -> z e. ( U. S X. U. T ) ) )
26	25	pm4.71rd 635	. . . . . 6 |- ( ( ph /\ a e. T ) -> ( z e. ( U. S X. a ) <-> ( z e. ( U. S X. U. T ) /\ z e. ( U. S X. a ) ) ) )
27		ffn 5559	. . . . . . . 8 |- ( ( 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 ) )
28		elpreima 5823	. . . . . . . 8 |- ( ( 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 ) ) )
29	1, 27, 28	mp2b 10	. . . . . . 7 |- ( 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 ) )
30		fvres 5704	. . . . . . . . . 10 |- ( z e. ( U. S X. U. T ) -> ( ( 2nd |` ( U. S X. U. T ) ) ` z ) = ( 2nd ` z ) )
31	30	eleq1d 2509	. . . . . . . . 9 |- ( z e. ( U. S X. U. T ) -> ( ( ( 2nd |` ( U. S X. U. T ) ) ` z ) e. a <-> ( 2nd ` z ) e. a ) )
32		1st2nd2 6613	. . . . . . . . . 10 |- ( z e. ( U. S X. U. T ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
33		xp1st 6606	. . . . . . . . . 10 |- ( z e. ( U. S X. U. T ) -> ( 1st ` z ) e. U. S )
34		elxp6 6608	. . . . . . . . . . . 12 |- ( z e. ( U. S X. a ) <-> ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( ( 1st ` z ) e. U. S /\ ( 2nd ` z ) e. a ) ) )
35		anass 649	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
36	34, 35	bitr4i 252	. . . . . . . . . . 11 |- ( z e. ( U. S X. a ) <-> ( ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( 1st ` z ) e. U. S ) /\ ( 2nd ` z ) e. a ) )
37	36	baib 896	. . . . . . . . . 10 |- ( ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( 1st ` z ) e. U. S ) -> ( z e. ( U. S X. a ) <-> ( 2nd ` z ) e. a ) )
38	32, 33, 37	syl2anc 661	. . . . . . . . 9 |- ( z e. ( U. S X. U. T ) -> ( z e. ( U. S X. a ) <-> ( 2nd ` z ) e. a ) )
39	31, 38	bitr4d 256	. . . . . . . 8 |- ( z e. ( U. S X. U. T ) -> ( ( ( 2nd |` ( U. S X. U. T ) ) ` z ) e. a <-> z e. ( U. S X. a ) ) )
40	39	pm5.32i 637	. . . . . . 7 |- ( ( 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 ) ) )
41	29, 40	bitri 249	. . . . . 6 |- ( z e. ( `' ( 2nd |` ( U. S X. U. T ) ) " a ) <-> ( z e. ( U. S X. U. T ) /\ z e. ( U. S X. a ) ) )
42	26, 41	syl6rbbr 264	. . . . 5 |- ( ( ph /\ a e. T ) -> ( z e. ( `' ( 2nd |` ( U. S X. U. T ) ) " a ) <-> z e. ( U. S X. a ) ) )
43	42	eqrdv 2441	. . . 4 |- ( ( ph /\ a e. T ) -> ( `' ( 2nd |` ( U. S X. U. T ) ) " a ) = ( U. S X. a ) )
44	2	adantr 465	. . . . 5 |- ( ( ph /\ a e. T ) -> S e. U. ran sigAlgebra )
45	3	adantr 465	. . . . 5 |- ( ( ph /\ a e. T ) -> T e. U. ran sigAlgebra )
46		eqid 2443	. . . . . . . 8 |- U. S = U. S
47		issgon 26566	. . . . . . . . 9 |- ( S e. (sigAlgebra ` U. S ) <-> ( S e. U. ran sigAlgebra /\ U. S = U. S ) )
48	47	biimpri 206	. . . . . . . 8 |- ( ( S e. U. ran sigAlgebra /\ U. S = U. S ) -> S e. (sigAlgebra ` U. S ) )
49	2, 46, 48	sylancl 662	. . . . . . 7 |- ( ph -> S e. (sigAlgebra ` U. S ) )
50		baselsiga 26558	. . . . . . 7 |- ( S e. (sigAlgebra ` U. S ) -> U. S e. S )
51	49, 50	syl 16	. . . . . 6 |- ( ph -> U. S e. S )
52	51	adantr 465	. . . . 5 |- ( ( ph /\ a e. T ) -> U. S e. S )
53		simpr 461	. . . . 5 |- ( ( ph /\ a e. T ) -> a e. T )
54		elsx 26608	. . . . 5 |- ( ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) /\ ( U. S e. S /\ a e. T ) ) -> ( U. S X. a ) e. ( S ×s T ) )
55	44, 45, 52, 53, 54	syl22anc 1219	. . . 4 |- ( ( ph /\ a e. T ) -> ( U. S X. a ) e. ( S ×s T ) )
56	43, 55	eqeltrd 2517	. . 3 |- ( ( ph /\ a e. T ) -> ( `' ( 2nd |` ( U. S X. U. T ) ) " a ) e. ( S ×s T ) )
57	56	ralrimiva 2799	. 2 |- ( ph -> A. a e. T ( `' ( 2nd |` ( U. S X. U. T ) ) " a ) e. ( S ×s T ) )
58	11, 3	ismbfm 26667	. 2 |- ( ph -> ( ( 2nd |` ( U. S X. U. T ) ) e. ( ( S ×s T )MblFnM T ) <-> ( ( 2nd |` ( U. S X. U. T ) ) e. ( U. T ^m U. ( S ×s T ) ) /\ A. a e. T ( `' ( 2nd |` ( U. S X. U. T ) ) " a ) e. ( S ×s T ) ) ) )
59	16, 57, 58	mpbir2and 913	1 |- ( ph -> ( 2nd |` ( U. S X. U. T ) ) e. ( ( S ×s T )MblFnM T ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   e. wcel 1756   A.wral 2715   C_ wss 3328   ~Pcpw 3860   <.cop 3883   U.cuni 4091   X. cxp 4838   `'ccnv 4839   ran crn 4841   |` cres 4842   "cima 4843   Fn wfn 5413   -->wf 5414   ` cfv 5418  (class class class)co 6091   1stc1st 6575   2ndc2nd 6576   ^m cmap 7214  sigAlgebracsiga 26550   ×_s csx 26602  MblFnMcmbfm 26665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-int 4129  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-1st 6577  df-2nd 6578  df-map 7216  df-siga 26551  df-sigagen 26582  df-sx 26603  df-mbfm 26666

This theorem is referenced by: (None)