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

Theorem imambfm 23569
 Description: If the sigma-algebra in the range of a given function is generated by a collection of basic sets , then to check the measurability of that function, we need only consider inverse images of basic sets . (Contributed by Thierry Arnoux, 4-Jun-2017.)
Hypotheses
Ref Expression
imambfm.1
imambfm.2 sigAlgebra
imambfm.3 sigaGen
Assertion
Ref Expression
imambfm MblFnM
Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem imambfm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imambfm.2 . . . . . 6 sigAlgebra
21adantr 451 . . . . 5 MblFnM sigAlgebra
3 imambfm.3 . . . . . . 7 sigaGen
4 imambfm.1 . . . . . . . 8
54sgsiga 23505 . . . . . . 7 sigaGen sigAlgebra
63, 5eqeltrd 2359 . . . . . 6 sigAlgebra
76adantr 451 . . . . 5 MblFnM sigAlgebra
8 simpr 447 . . . . 5 MblFnM MblFnM
92, 7, 8mbfmf 23562 . . . 4 MblFnM
101ad2antrr 706 . . . . . 6 MblFnM sigAlgebra
116ad2antrr 706 . . . . . 6 MblFnM sigAlgebra
12 simplr 731 . . . . . 6 MblFnM MblFnM
13 sssigagen 23508 . . . . . . . . . 10 sigaGen
144, 13syl 15 . . . . . . . . 9 sigaGen
1514, 3sseqtr4d 3217 . . . . . . . 8
1615ad2antrr 706 . . . . . . 7 MblFnM
17 simpr 447 . . . . . . 7 MblFnM
1816, 17sseldd 3183 . . . . . 6 MblFnM
1910, 11, 12, 18mbfmcnvima 23564 . . . . 5 MblFnM
2019ralrimiva 2628 . . . 4 MblFnM
219, 20jca 518 . . 3 MblFnM
2221ex 423 . 2 MblFnM
23 unielsiga 23491 . . . . . . 7 sigAlgebra
246, 23syl 15 . . . . . 6
2524adantr 451 . . . . 5
26 unielsiga 23491 . . . . . . 7 sigAlgebra
271, 26syl 15 . . . . . 6
2827adantr 451 . . . . 5
29 simprl 732 . . . . 5
30 elmapg 6787 . . . . . 6
3130biimpar 471 . . . . 5
3225, 28, 29, 31syl21anc 1181 . . . 4
33 simpl 443 . . . . . . . 8
3433, 3syl 15 . . . . . . 7 sigaGen
35 ssrab2 3260 . . . . . . . . . . . 12
36 pwuni 4208 . . . . . . . . . . . 12
3735, 36sstri 3190 . . . . . . . . . . 11
3837a1i 10 . . . . . . . . . 10
39 fimacnv 5659 . . . . . . . . . . . . . . 15
4039ad2antrl 708 . . . . . . . . . . . . . 14
4140, 28eqeltrd 2359 . . . . . . . . . . . . 13
4225, 41jca 518 . . . . . . . . . . . 12
43 imaeq2 5010 . . . . . . . . . . . . . 14
4443eleq1d 2351 . . . . . . . . . . . . 13
4544elrab 2925 . . . . . . . . . . . 12
4642, 45sylibr 203 . . . . . . . . . . 11
476ad2antrr 706 . . . . . . . . . . . . . 14 sigAlgebra
4847, 23syl 15 . . . . . . . . . . . . . 14
49 imaeq2 5010 . . . . . . . . . . . . . . . . . 18
5049eleq1d 2351 . . . . . . . . . . . . . . . . 17
5150elrab 2925 . . . . . . . . . . . . . . . 16
5251simplbi 446 . . . . . . . . . . . . . . 15
5352adantl 452 . . . . . . . . . . . . . 14
54 difelsiga 23496 . . . . . . . . . . . . . 14 sigAlgebra
5547, 48, 53, 54syl3anc 1182 . . . . . . . . . . . . 13
56 simplrl 736 . . . . . . . . . . . . . . 15
57 ffun 5393 . . . . . . . . . . . . . . 15
58 difpreima 5655 . . . . . . . . . . . . . . 15
5956, 57, 583syl 18 . . . . . . . . . . . . . 14
6040difeq1d 3295 . . . . . . . . . . . . . . . . 17
6160ralrimivw 2629 . . . . . . . . . . . . . . . 16
6261r19.21bi 2643 . . . . . . . . . . . . . . 15
631ad2antrr 706 . . . . . . . . . . . . . . . 16 sigAlgebra
6463, 26syl 15 . . . . . . . . . . . . . . . 16
6551simprbi 450 . . . . . . . . . . . . . . . . 17
6665adantl 452 . . . . . . . . . . . . . . . 16
67 difelsiga 23496 . . . . . . . . . . . . . . . 16 sigAlgebra
6863, 64, 66, 67syl3anc 1182 . . . . . . . . . . . . . . 15
6962, 68eqeltrd 2359 . . . . . . . . . . . . . 14
7059, 69eqeltrd 2359 . . . . . . . . . . . . 13
71 imaeq2 5010 . . . . . . . . . . . . . . . 16
7271eleq1d 2351 . . . . . . . . . . . . . . 15
7372elrab 2925 . . . . . . . . . . . . . 14
7473biimpri 197 . . . . . . . . . . . . 13
7555, 70, 74syl2anc 642 . . . . . . . . . . . 12
7675ralrimiva 2628 . . . . . . . . . . 11
776ad3antrrr 710 . . . . . . . . . . . . . . 15 sigAlgebra
78 sspwb 4225 . . . . . . . . . . . . . . . . . 18
7935, 78mpbi 199 . . . . . . . . . . . . . . . . 17
8079sseli 3178 . . . . . . . . . . . . . . . 16
8180ad2antlr 707 . . . . . . . . . . . . . . 15
82 simpr 447 . . . . . . . . . . . . . . 15
83 sigaclcu 23480 . . . . . . . . . . . . . . 15 sigAlgebra
8477, 81, 82, 83syl3anc 1182 . . . . . . . . . . . . . 14
85 simpllr 735 . . . . . . . . . . . . . . . . . 18
8685simpld 445 . . . . . . . . . . . . . . . . 17
8786, 57syl 15 . . . . . . . . . . . . . . . 16
88 unipreima 23211 . . . . . . . . . . . . . . . 16
8987, 88syl 15 . . . . . . . . . . . . . . 15
901ad3antrrr 710 . . . . . . . . . . . . . . . 16 sigAlgebra
91 simpr 447 . . . . . . . . . . . . . . . . . . 19
92 simpllr 735 . . . . . . . . . . . . . . . . . . 19
93 elelpwi 3637 . . . . . . . . . . . . . . . . . . 19
9491, 92, 93syl2anc 642 . . . . . . . . . . . . . . . . . 18
95 imaeq2 5010 . . . . . . . . . . . . . . . . . . . . 21
9695eleq1d 2351 . . . . . . . . . . . . . . . . . . . 20
9796elrab 2925 . . . . . . . . . . . . . . . . . . 19
9897simprbi 450 . . . . . . . . . . . . . . . . . 18
9994, 98syl 15 . . . . . . . . . . . . . . . . 17
10099ralrimiva 2628 . . . . . . . . . . . . . . . 16
101 nfcv 2421 . . . . . . . . . . . . . . . . 17
102101sigaclcuni 23481 . . . . . . . . . . . . . . . 16 sigAlgebra
10390, 100, 82, 102syl3anc 1182 . . . . . . . . . . . . . . 15
10489, 103eqeltrd 2359 . . . . . . . . . . . . . 14
105 imaeq2 5010 . . . . . . . . . . . . . . . . 17
106105eleq1d 2351 . . . . . . . . . . . . . . . 16
107106elrab 2925 . . . . . . . . . . . . . . 15
108107biimpri 197 . . . . . . . . . . . . . 14
10984, 104, 108syl2anc 642 . . . . . . . . . . . . 13
110109ex 423 . . . . . . . . . . . 12
111110ralrimiva 2628 . . . . . . . . . . 11
11246, 76, 1113jca 1132 . . . . . . . . . 10
113 rabexg 4166 . . . . . . . . . . . . 13 sigAlgebra
114 issiga 23474 . . . . . . . . . . . . 13 sigAlgebra
1156, 113, 1143syl 18 . . . . . . . . . . . 12 sigAlgebra
116115biimprd 214 . . . . . . . . . . 11 sigAlgebra
117116imp 418 . . . . . . . . . 10 sigAlgebra
11833, 38, 112, 117syl12anc 1180 . . . . . . . . 9 sigAlgebra
1193unieqd 3840 . . . . . . . . . . . . 13 sigaGen
120 unisg 23506 . . . . . . . . . . . . . 14 sigaGen
1214, 120syl 15 . . . . . . . . . . . . 13 sigaGen
122119, 121eqtrd 2317 . . . . . . . . . . . 12
123122fveq2d 5531 . . . . . . . . . . 11 sigAlgebra sigAlgebra
124123eleq2d 2352 . . . . . . . . . 10 sigAlgebra sigAlgebra
125124adantr 451 . . . . . . . . 9 sigAlgebra sigAlgebra
126118, 125mpbid 201 . . . . . . . 8 sigAlgebra
12733, 15syl 15 . . . . . . . . 9
128 simprr 733 . . . . . . . . 9
129 ssrab 3253 . . . . . . . . . 10
130129biimpri 197 . . . . . . . . 9
131127, 128, 130syl2anc 642 . . . . . . . 8
132 sigagenss 23512 . . . . . . . 8 sigAlgebra sigaGen
133126, 131, 132syl2anc 642 . . . . . . 7 sigaGen
13434, 133eqsstrd 3214 . . . . . 6
13535a1i 10 . . . . . 6
136134, 135eqssd 3198 . . . . 5
137 rabid2 2719 . . . . 5
138136, 137sylib 188 . . . 4
13933, 1syl 15 . . . . 5 sigAlgebra
14033, 6syl 15 . . . . 5 sigAlgebra
141139, 140ismbfm 23559 . . . 4 MblFnM
14232, 138, 141mpbir2and 888 . . 3 MblFnM
143142ex 423 . 2 MblFnM
14422, 143impbid 183 1 MblFnM
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wceq 1625   wcel 1686  wral 2545  crab 2549  cvv 2790   cdif 3151   wss 3154  cpw 3627  cop 3645  cuni 3829  ciun 3907   class class class wbr 4025  com 4658  ccnv 4690   crn 4692  cima 4694   wfun 5251  wf 5253  cfv 5257  (class class class)co 5860   cmap 6774   cdom 6863  sigAlgebracsiga 23470  sigaGencsigagen 23501  MblFnMcmbfm 23557 This theorem is referenced by:  cnmbfm  23570  mbfmco2  23572 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  ax-inf2 7344  ax-ac2 8091 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  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-rmo 2553  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-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-int 3865  df-iun 3909  df-iin 3910  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-se 4355  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  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-isom 5266  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-1st 6124  df-2nd 6125  df-riota 6306  df-recs 6390  df-rdg 6425  df-1o 6481  df-2o 6482  df-oadd 6485  df-er 6662  df-map 6776  df-en 6866  df-dom 6867  df-sdom 6868  df-fin 6869  df-oi 7227  df-card 7574  df-acn 7577  df-ac 7745  df-cda 7796  df-siga 23471  df-sigagen 23502  df-mbfm 23558
 Copyright terms: Public domain W3C validator