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

Theorem imambfm 24604
 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 . . . . 5 sigAlgebra
21adantr 452 . . . 4 MblFnM sigAlgebra
3 imambfm.3 . . . . . 6 sigaGen
4 imambfm.1 . . . . . . 7
54sgsiga 24517 . . . . . 6 sigaGen sigAlgebra
63, 5eqeltrd 2509 . . . . 5 sigAlgebra
76adantr 452 . . . 4 MblFnM sigAlgebra
8 simpr 448 . . . 4 MblFnM MblFnM
92, 7, 8mbfmf 24597 . . 3 MblFnM
101ad2antrr 707 . . . . 5 MblFnM sigAlgebra
116ad2antrr 707 . . . . 5 MblFnM sigAlgebra
12 simplr 732 . . . . 5 MblFnM MblFnM
13 sssigagen 24520 . . . . . . . . 9 sigaGen
144, 13syl 16 . . . . . . . 8 sigaGen
1514, 3sseqtr4d 3377 . . . . . . 7
1615ad2antrr 707 . . . . . 6 MblFnM
17 simpr 448 . . . . . 6 MblFnM
1816, 17sseldd 3341 . . . . 5 MblFnM
1910, 11, 12, 18mbfmcnvima 24599 . . . 4 MblFnM
2019ralrimiva 2781 . . 3 MblFnM
219, 20jca 519 . 2 MblFnM
22 unielsiga 24503 . . . . . 6 sigAlgebra
236, 22syl 16 . . . . 5
2423adantr 452 . . . 4
25 unielsiga 24503 . . . . . 6 sigAlgebra
261, 25syl 16 . . . . 5
2726adantr 452 . . . 4
28 simprl 733 . . . 4
29 elmapg 7023 . . . . 5
3029biimpar 472 . . . 4
3124, 27, 28, 30syl21anc 1183 . . 3
323adantr 452 . . . . . 6 sigaGen
33 simpl 444 . . . . . . . . 9
34 ssrab2 3420 . . . . . . . . . . 11
35 pwuni 4387 . . . . . . . . . . 11
3634, 35sstri 3349 . . . . . . . . . 10
3736a1i 11 . . . . . . . . 9
38 fimacnv 5854 . . . . . . . . . . . . 13
3938ad2antrl 709 . . . . . . . . . . . 12
4039, 27eqeltrd 2509 . . . . . . . . . . 11
41 imaeq2 5191 . . . . . . . . . . . . 13
4241eleq1d 2501 . . . . . . . . . . . 12
4342elrab 3084 . . . . . . . . . . 11
4424, 40, 43sylanbrc 646 . . . . . . . . . 10
456ad2antrr 707 . . . . . . . . . . . . 13 sigAlgebra
4645, 22syl 16 . . . . . . . . . . . . 13
47 elrabi 3082 . . . . . . . . . . . . . 14
4847adantl 453 . . . . . . . . . . . . 13
49 difelsiga 24508 . . . . . . . . . . . . 13 sigAlgebra
5045, 46, 48, 49syl3anc 1184 . . . . . . . . . . . 12
51 simplrl 737 . . . . . . . . . . . . . 14
52 ffun 5585 . . . . . . . . . . . . . 14
53 difpreima 5850 . . . . . . . . . . . . . 14
5451, 52, 533syl 19 . . . . . . . . . . . . 13
5539difeq1d 3456 . . . . . . . . . . . . . . 15
5655adantr 452 . . . . . . . . . . . . . 14
571ad2antrr 707 . . . . . . . . . . . . . . 15 sigAlgebra
5857, 25syl 16 . . . . . . . . . . . . . . 15
59 imaeq2 5191 . . . . . . . . . . . . . . . . . . 19
6059eleq1d 2501 . . . . . . . . . . . . . . . . . 18
6160elrab 3084 . . . . . . . . . . . . . . . . 17
6261simprbi 451 . . . . . . . . . . . . . . . 16
6362adantl 453 . . . . . . . . . . . . . . 15
64 difelsiga 24508 . . . . . . . . . . . . . . 15 sigAlgebra
6557, 58, 63, 64syl3anc 1184 . . . . . . . . . . . . . 14
6656, 65eqeltrd 2509 . . . . . . . . . . . . 13
6754, 66eqeltrd 2509 . . . . . . . . . . . 12
68 imaeq2 5191 . . . . . . . . . . . . . 14
6968eleq1d 2501 . . . . . . . . . . . . 13
7069elrab 3084 . . . . . . . . . . . 12
7150, 67, 70sylanbrc 646 . . . . . . . . . . 11
7271ralrimiva 2781 . . . . . . . . . 10
736ad3antrrr 711 . . . . . . . . . . . . . 14 sigAlgebra
74 sspwb 4405 . . . . . . . . . . . . . . . . 17
7534, 74mpbi 200 . . . . . . . . . . . . . . . 16
7675sseli 3336 . . . . . . . . . . . . . . 15
7776ad2antlr 708 . . . . . . . . . . . . . 14
78 simpr 448 . . . . . . . . . . . . . 14
79 sigaclcu 24492 . . . . . . . . . . . . . 14 sigAlgebra
8073, 77, 78, 79syl3anc 1184 . . . . . . . . . . . . 13
81 simpllr 736 . . . . . . . . . . . . . . . 16
8281simpld 446 . . . . . . . . . . . . . . 15
83 unipreima 24048 . . . . . . . . . . . . . . 15
8482, 52, 833syl 19 . . . . . . . . . . . . . 14
851ad3antrrr 711 . . . . . . . . . . . . . . 15 sigAlgebra
86 simpr 448 . . . . . . . . . . . . . . . . . 18
87 simpllr 736 . . . . . . . . . . . . . . . . . 18
88 elelpwi 3801 . . . . . . . . . . . . . . . . . 18
8986, 87, 88syl2anc 643 . . . . . . . . . . . . . . . . 17
90 imaeq2 5191 . . . . . . . . . . . . . . . . . . . 20
9190eleq1d 2501 . . . . . . . . . . . . . . . . . . 19
9291elrab 3084 . . . . . . . . . . . . . . . . . 18
9392simprbi 451 . . . . . . . . . . . . . . . . 17
9489, 93syl 16 . . . . . . . . . . . . . . . 16
9594ralrimiva 2781 . . . . . . . . . . . . . . 15
96 nfcv 2571 . . . . . . . . . . . . . . . 16
9796sigaclcuni 24493 . . . . . . . . . . . . . . 15 sigAlgebra
9885, 95, 78, 97syl3anc 1184 . . . . . . . . . . . . . 14
9984, 98eqeltrd 2509 . . . . . . . . . . . . 13
100 imaeq2 5191 . . . . . . . . . . . . . . 15
101100eleq1d 2501 . . . . . . . . . . . . . 14
102101elrab 3084 . . . . . . . . . . . . 13
10380, 99, 102sylanbrc 646 . . . . . . . . . . . 12
104103ex 424 . . . . . . . . . . 11
105104ralrimiva 2781 . . . . . . . . . 10
10644, 72, 1053jca 1134 . . . . . . . . 9
107 rabexg 4345 . . . . . . . . . . 11 sigAlgebra
108 issiga 24486 . . . . . . . . . . 11 sigAlgebra
1096, 107, 1083syl 19 . . . . . . . . . 10 sigAlgebra
110109biimpar 472 . . . . . . . . 9 sigAlgebra
11133, 37, 106, 110syl12anc 1182 . . . . . . . 8 sigAlgebra
1123unieqd 4018 . . . . . . . . . . . 12 sigaGen
113 unisg 24518 . . . . . . . . . . . . 13 sigaGen
1144, 113syl 16 . . . . . . . . . . . 12 sigaGen
115112, 114eqtrd 2467 . . . . . . . . . . 11
116115fveq2d 5724 . . . . . . . . . 10 sigAlgebra sigAlgebra
117116eleq2d 2502 . . . . . . . . 9 sigAlgebra sigAlgebra
118117adantr 452 . . . . . . . 8 sigAlgebra sigAlgebra
119111, 118mpbid 202 . . . . . . 7 sigAlgebra
12015adantr 452 . . . . . . . 8
121 simprr 734 . . . . . . . 8
122 ssrab 3413 . . . . . . . 8
123120, 121, 122sylanbrc 646 . . . . . . 7
124 sigagenss 24524 . . . . . . 7 sigAlgebra sigaGen
125119, 123, 124syl2anc 643 . . . . . 6 sigaGen
12632, 125eqsstrd 3374 . . . . 5
12734a1i 11 . . . . 5
128126, 127eqssd 3357 . . . 4
129 rabid2 2877 . . . 4
130128, 129sylib 189 . . 3
1311adantr 452 . . . 4 sigAlgebra
1326adantr 452 . . . 4 sigAlgebra
133131, 132ismbfm 24594 . . 3 MblFnM
13431, 130, 133mpbir2and 889 . 2 MblFnM
13521, 134impbida 806 1 MblFnM
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3a 936   wceq 1652   wcel 1725  wral 2697  crab 2701  cvv 2948   cdif 3309   wss 3312  cpw 3791  cuni 4007  ciun 4085   class class class wbr 4204  com 4837  ccnv 4869   crn 4871  cima 4873   wfun 5440  wf 5442  cfv 5446  (class class class)co 6073   cmap 7010   cdom 7099  sigAlgebracsiga 24482  sigaGencsigagen 24513  MblFnMcmbfm 24592 This theorem is referenced by:  cnmbfm  24605  mbfmco2  24607 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-inf2 7588  ax-ac2 8335 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-iin 4088  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-se 4534  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-isom 5455  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-1st 6341  df-2nd 6342  df-riota 6541  df-recs 6625  df-rdg 6660  df-1o 6716  df-2o 6717  df-oadd 6720  df-er 6897  df-map 7012  df-en 7102  df-dom 7103  df-sdom 7104  df-fin 7105  df-oi 7471  df-card 7818  df-acn 7821  df-ac 7989  df-cda 8040  df-siga 24483  df-sigagen 24514  df-mbfm 24593
 Copyright terms: Public domain W3C validator