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

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

Proof of Theorem 1stmbfm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1stres 6143 . . . . 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
92, 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
182, 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 xpss1 4797 . . . . . . . . . 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 xp2nd 6152 . . . . . . . . . . 11
35 elxp6 6153 . . . . . . . . . . . . 13
36 anass 630 . . . . . . . . . . . . 13
37 an32 773 . . . . . . . . . . . . 13
3835, 36, 373bitr2i 264 . . . . . . . . . . . 12
3938baib 871 . . . . . . . . . . 11
4033, 34, 39syl2anc 642 . . . . . . . . . 10
4132, 40bitr4d 247 . . . . . . . . 9
4241pm5.32i 618 . . . . . . . 8
4330, 42bitri 240 . . . . . . 7
4427, 43syl6rbbr 255 . . . . . 6
4544eqrdv 2283 . . . . 5
462adantr 451 . . . . . . 7 sigAlgebra
473adantr 451 . . . . . . 7 sigAlgebra
4846, 47jca 518 . . . . . 6 sigAlgebra sigAlgebra
49 simpr 447 . . . . . . 7
50 eqid 2285 . . . . . . . . . 10
51 issgon 23486 . . . . . . . . . . 11 sigAlgebra sigAlgebra
5251biimpri 197 . . . . . . . . . 10 sigAlgebra sigAlgebra
533, 50, 52sylancl 643 . . . . . . . . 9 sigAlgebra
54 baselsiga 23478 . . . . . . . . 9 sigAlgebra
5553, 54syl 15 . . . . . . . 8
5655adantr 451 . . . . . . 7
5749, 56jca 518 . . . . . 6
58 elsx 23527 . . . . . 6 sigAlgebra sigAlgebra ×s
5948, 57, 58syl2anc 642 . . . . 5 ×s
6045, 59eqeltrd 2359 . . . 4 ×s
6160ralrimiva 2628 . . 3 ×s
6216, 61jca 518 . 2 ×s ×s
6311, 2ismbfm 23559 . 2 MblFnM ×s ×s ×s
6462, 63mpbird 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