Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2ndmbfm Unicode version

Theorem 2ndmbfm 23568
 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 sigAlgebra
1stmbfm.2 sigAlgebra
Assertion
Ref Expression
2ndmbfm MblFnM ×s

Proof of Theorem 2ndmbfm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f2ndres 6144 . . . . 5
2 1stmbfm.1 . . . . . . 7 sigAlgebra
3 1stmbfm.2 . . . . . . 7 sigAlgebra
4 sxuni 23526 . . . . . . 7 sigAlgebra sigAlgebra ×s
52, 3, 4syl2anc 642 . . . . . 6 ×s
65feq2d 5382 . . . . 5 ×s
71, 6mpbii 202 . . . 4 ×s
8 unielsiga 23491 . . . . . 6 sigAlgebra
93, 8syl 15 . . . . 5
10 sxsiga 23524 . . . . . . 7 sigAlgebra sigAlgebra ×s sigAlgebra
112, 3, 10syl2anc 642 . . . . . 6 ×s sigAlgebra
12 unielsiga 23491 . . . . . 6 ×s sigAlgebra ×s ×s
1311, 12syl 15 . . . . 5 ×s ×s
14 elmapg 6787 . . . . 5 ×s ×s ×s ×s
159, 13, 14syl2anc 642 . . . 4 ×s ×s
167, 15mpbird 223 . . 3 ×s
17 sgon 23487 . . . . . . . . . . . . 13 sigAlgebra sigAlgebra
183, 17syl 15 . . . . . . . . . . . 12 sigAlgebra
19 sigasspw 23479 . . . . . . . . . . . 12 sigAlgebra
20 pwssb 3990 . . . . . . . . . . . . 13
2120biimpi 186 . . . . . . . . . . . 12
2218, 19, 213syl 18 . . . . . . . . . . 11
2322r19.21bi 2643 . . . . . . . . . 10
24 xpss2 4798 . . . . . . . . . 10
2523, 24syl 15 . . . . . . . . 9
2625sseld 3181 . . . . . . . 8
2726pm4.71rd 616 . . . . . . 7
28 ffn 5391 . . . . . . . . 9
29 elpreima 5647 . . . . . . . . 9
301, 28, 29mp2b 9 . . . . . . . 8
31 fvres 5544 . . . . . . . . . . 11
3231eleq1d 2351 . . . . . . . . . 10
33 1st2nd2 6161 . . . . . . . . . . 11
34 xp1st 6151 . . . . . . . . . . 11
35 elxp6 6153 . . . . . . . . . . . . 13
36 anass 630 . . . . . . . . . . . . 13
3735, 36bitr4i 243 . . . . . . . . . . . 12
3837baib 871 . . . . . . . . . . 11
3933, 34, 38syl2anc 642 . . . . . . . . . 10
4032, 39bitr4d 247 . . . . . . . . 9
4140pm5.32i 618 . . . . . . . 8
4230, 41bitri 240 . . . . . . 7
4327, 42syl6rbbr 255 . . . . . 6
4443eqrdv 2283 . . . . 5
452adantr 451 . . . . . . 7 sigAlgebra
463adantr 451 . . . . . . 7 sigAlgebra
4745, 46jca 518 . . . . . 6 sigAlgebra sigAlgebra
48 eqid 2285 . . . . . . . . . 10
49 issgon 23486 . . . . . . . . . . 11 sigAlgebra sigAlgebra
5049biimpri 197 . . . . . . . . . 10 sigAlgebra sigAlgebra
512, 48, 50sylancl 643 . . . . . . . . 9 sigAlgebra
52 baselsiga 23478 . . . . . . . . 9 sigAlgebra
5351, 52syl 15 . . . . . . . 8
5453adantr 451 . . . . . . 7
55 simpr 447 . . . . . . 7
5654, 55jca 518 . . . . . 6
57 elsx 23527 . . . . . 6 sigAlgebra sigAlgebra ×s
5847, 56, 57syl2anc 642 . . . . 5 ×s
5944, 58eqeltrd 2359 . . . 4 ×s
6059ralrimiva 2628 . . 3 ×s
6116, 60jca 518 . 2 ×s ×s
6211, 3ismbfm 23559 . 2 MblFnM ×s ×s ×s
6361, 62mpbird 223 1 MblFnM ×s
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   wceq 1625   wcel 1686  wral 2545   wss 3154  cpw 3627  cop 3645  cuni 3829   cxp 4689  ccnv 4690   crn 4692   cres 4693  cima 4694   wfn 5252  wf 5253  cfv 5257  (class class class)co 5860  c1st 6122  c2nd 6123   cmap 6774  sigAlgebracsiga 23470   ×s csx 23521  MblFnMcmbfm 23557 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-int 3865  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-1st 6124  df-2nd 6125  df-map 6776  df-siga 23471  df-sigagen 23502  df-sx 23522  df-mbfm 23558
 Copyright terms: Public domain W3C validator