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

Theorem measvuni 28675
 Description: The measure of a countable disjoint union is the sum of the measures. This theorem uses a collection rather than a set of subsets of . (Contributed by Thierry Arnoux, 7-Mar-2017.)
Assertion
Ref Expression
measvuni measures Disj Σ*
Distinct variable groups:   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem measvuni
StepHypRef Expression
1 simp1 999 . . . 4 measures Disj measures
2 rabid 2986 . . . . . . . 8
32simprbi 464 . . . . . . 7
43adantl 466 . . . . . 6 measures
54ralrimiva 2820 . . . . 5 measures
653ad2ant1 1020 . . . 4 measures Disj
7 ssrab2 3526 . . . . . . 7
8 ssct 27991 . . . . . . 7
97, 8mpan 670 . . . . . 6
109adantr 465 . . . . 5 Disj
11103ad2ant3 1022 . . . 4 measures Disj
12 simp3r 1028 . . . . 5 measures Disj Disj
13 nfrab1 2990 . . . . . 6
14 nfcv 2566 . . . . . 6
1513, 14disjss1f 27878 . . . . 5 Disj Disj
167, 12, 15mpsyl 64 . . . 4 measures Disj Disj
1713measvunilem0 28674 . . . 4 measures Disj Σ*
181, 6, 11, 16, 17syl112anc 1236 . . 3 measures Disj Σ*
19 rabid 2986 . . . . . . . 8
2019simprbi 464 . . . . . . 7
2120adantl 466 . . . . . 6 measures
2221ralrimiva 2820 . . . . 5 measures
23223ad2ant1 1020 . . . 4 measures Disj
24 ssrab2 3526 . . . . . . 7
25 ssct 27991 . . . . . . 7
2624, 25mpan 670 . . . . . 6
2726adantr 465 . . . . 5 Disj
28273ad2ant3 1022 . . . 4 measures Disj
29 nfrab1 2990 . . . . . 6
3029, 14disjss1f 27878 . . . . 5 Disj Disj
3124, 12, 30mpsyl 64 . . . 4 measures Disj Disj
3229measvunilem 28673 . . . 4 measures Disj Σ*
331, 23, 28, 31, 32syl112anc 1236 . . 3 measures Disj Σ*
3418, 33oveq12d 6298 . 2 measures Disj Σ* Σ*
35 nfv 1730 . . . . . . 7 measures
36 nfra1 2787 . . . . . . 7
37 nfv 1730 . . . . . . . 8
38 nfdisj1 4381 . . . . . . . 8 Disj
3937, 38nfan 1958 . . . . . . 7 Disj
4035, 36, 39nf3an 1960 . . . . . 6 measures Disj
4113, 29nfun 3601 . . . . . 6
42 simp2 1000 . . . . . . . . 9 measures Disj
43 rabid2 2987 . . . . . . . . 9
4442, 43sylibr 214 . . . . . . . 8 measures Disj
45 elun 3586 . . . . . . . . . . 11
46 measbase 28658 . . . . . . . . . . . . . 14 measures sigAlgebra
47 0elsiga 28575 . . . . . . . . . . . . . 14 sigAlgebra
48 snssi 4118 . . . . . . . . . . . . . 14
4946, 47, 483syl 18 . . . . . . . . . . . . 13 measures
50 undif 3854 . . . . . . . . . . . . 13
5149, 50sylib 198 . . . . . . . . . . . 12 measures
5251eleq2d 2474 . . . . . . . . . . 11 measures
5345, 52syl5bbr 261 . . . . . . . . . 10 measures
5453rabbidv 3053 . . . . . . . . 9 measures
55543ad2ant1 1020 . . . . . . . 8 measures Disj
5644, 55eqtr4d 2448 . . . . . . 7 measures Disj
57 unrab 3723 . . . . . . 7
5856, 57syl6eqr 2463 . . . . . 6 measures Disj
59 eqidd 2405 . . . . . 6 measures Disj
6040, 14, 41, 58, 59iuneq12df 4297 . . . . 5 measures Disj
6160fveq2d 5855 . . . 4 measures Disj
62 iunxun 4358 . . . . 5
6362fveq2i 5854 . . . 4
6461, 63syl6eq 2461 . . 3 measures Disj
65463ad2ant1 1020 . . . . 5 measures Disj sigAlgebra
6647adantr 465 . . . . . . . . 9 sigAlgebra
67 elsni 3999 . . . . . . . . . . 11
6867eleq1d 2473 . . . . . . . . . 10
6968adantl 466 . . . . . . . . 9 sigAlgebra
7066, 69mpbird 234 . . . . . . . 8 sigAlgebra
7146, 3, 70syl2an 477 . . . . . . 7 measures
7271ralrimiva 2820 . . . . . 6 measures
73723ad2ant1 1020 . . . . 5 measures Disj
7413sigaclcuni 28579 . . . . 5 sigAlgebra
7565, 73, 11, 74syl3anc 1232 . . . 4 measures Disj
7621eldifad 3428 . . . . . . 7 measures
7776ralrimiva 2820 . . . . . 6 measures
78773ad2ant1 1020 . . . . 5 measures Disj
7929sigaclcuni 28579 . . . . 5 sigAlgebra
8065, 78, 28, 79syl3anc 1232 . . . 4 measures Disj
813, 67syl 17 . . . . . . 7
8281iuneq2i 4292 . . . . . 6
83 iun0 4329 . . . . . 6
8482, 83eqtri 2433 . . . . 5
85 ineq1 3636 . . . . . 6
86 incom 3634 . . . . . . 7
87 in0 3767 . . . . . . 7
8886, 87eqtr3i 2435 . . . . . 6
8985, 88syl6eq 2461 . . . . 5
9084, 89mp1i 13 . . . 4 measures Disj
91 measun 28672 . . . 4 measures
921, 75, 80, 90, 91syl121anc 1237 . . 3 measures Disj
9364, 92eqtrd 2445 . 2 measures Disj
9440, 58esumeq1d 28495 . . 3 measures Disj Σ* Σ*
95 ctex 27990 . . . . 5
9611, 95syl 17 . . . 4 measures Disj
97 ctex 27990 . . . . 5
9828, 97syl 17 . . . 4 measures Disj
99 inrab 3724 . . . . . 6
100 noel 3744 . . . . . . . . . 10
101 disjdif 3846 . . . . . . . . . . 11
102101eleq2i 2482 . . . . . . . . . 10
103100, 102mtbir 299 . . . . . . . . 9
104 elin 3628 . . . . . . . . 9
105103, 104mtbi 298 . . . . . . . 8
106105rgenw 2767 . . . . . . 7
107 rabeq0 3763 . . . . . . 7
108106, 107mpbir 211 . . . . . 6
10999, 108eqtri 2433 . . . . 5
110109a1i 11 . . . 4 measures Disj
1111adantr 465 . . . . 5 measures Disj measures
1121, 71sylan 471 . . . . 5 measures Disj
113 measvxrge0 28666 . . . . 5 measures
114111, 112, 113syl2anc 661 . . . 4 measures Disj
1151adantr 465 . . . . 5 measures Disj measures
11620adantl 466 . . . . . 6 measures Disj
117116eldifad 3428 . . . . 5 measures Disj
118115, 117, 113syl2anc 661 . . . 4 measures Disj
11940, 13, 29, 96, 98, 110, 114, 118esumsplit 28513 . . 3 measures Disj Σ* Σ* Σ*
12094, 119eqtrd 2445 . 2 measures Disj Σ* Σ* Σ*
12134, 93, 1203eqtr4d 2455 1 measures Disj Σ*
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 186   wo 368   wa 369   w3a 976   wceq 1407   wcel 1844  wral 2756  crab 2760  cvv 3061   cdif 3413   cun 3414   cin 3415   wss 3416  c0 3740  csn 3974  cuni 4193  ciun 4273  Disj wdisj 4368   class class class wbr 4397   crn 4826  cfv 5571  (class class class)co 6280  com 6685   cdom 7554  cc0 9524   cpnf 9657  cxad 11371  cicc 11587  Σ*cesum 28487  sigAlgebracsiga 28568  measurescmeas 28656 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-rep 4509  ax-sep 4519  ax-nul 4527  ax-pow 4574  ax-pr 4632  ax-un 6576  ax-inf2 8093  ax-ac2 8877  ax-cnex 9580  ax-resscn 9581  ax-1cn 9582  ax-icn 9583  ax-addcl 9584  ax-addrcl 9585  ax-mulcl 9586  ax-mulrcl 9587  ax-mulcom 9588  ax-addass 9589  ax-mulass 9590  ax-distr 9591  ax-i2m1 9592  ax-1ne0 9593  ax-1rid 9594  ax-rnegex 9595  ax-rrecex 9596  ax-cnre 9597  ax-pre-lttri 9598  ax-pre-lttrn 9599  ax-pre-ltadd 9600  ax-pre-mulgt0 9601  ax-pre-sup 9602  ax-addf 9603  ax-mulf 9604 This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3or 977  df-3an 978  df-tru 1410  df-fal 1413  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-nel 2603  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3063  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3741  df-if 3888  df-pw 3959  df-sn 3975  df-pr 3977  df-tp 3979  df-op 3981  df-uni 4194  df-int 4230  df-iun 4275  df-iin 4276  df-disj 4369  df-br 4398  df-opab 4456  df-mpt 4457  df-tr 4492  df-eprel 4736  df-id 4740  df-po 4746  df-so 4747  df-fr 4784  df-se 4785  df-we 4786  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-pred 5369  df-ord 5415  df-on 5416  df-lim 5417  df-suc 5418  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-f1 5576  df-fo 5577  df-f1o 5578  df-fv 5579  df-isom 5580  df-riota 6242  df-ov 6283  df-oprab 6284  df-mpt2 6285  df-of 6523  df-om 6686  df-1st 6786  df-2nd 6787  df-supp 6905  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-1o 7169  df-2o 7170  df-oadd 7173  df-er 7350  df-map 7461  df-pm 7462  df-ixp 7510  df-en 7557  df-dom 7558  df-sdom 7559  df-fin 7560  df-fsupp 7866  df-fi 7907  df-sup 7937  df-oi 7971  df-card 8354  df-acn 8357  df-ac 8531  df-cda 8582  df-pnf 9662  df-mnf 9663  df-xr 9664  df-ltxr 9665  df-le 9666  df-sub 9845  df-neg 9846  df-div 10250  df-nn 10579  df-2 10637  df-3 10638  df-4 10639  df-5 10640  df-6 10641  df-7 10642  df-8 10643  df-9 10644  df-10 10645  df-n0 10839  df-z 10908  df-dec 11022  df-uz 11130  df-q 11230  df-rp 11268  df-xneg 11373  df-xadd 11374  df-xmul 11375  df-ioo 11588  df-ioc 11589  df-ico 11590  df-icc 11591  df-fz 11729  df-fzo 11857  df-fl 11968  df-mod 12037  df-seq 12154  df-exp 12213  df-fac 12400  df-bc 12427  df-hash 12455  df-shft 13051  df-cj 13083  df-re 13084  df-im 13085  df-sqrt 13219  df-abs 13220  df-limsup 13445  df-clim 13462  df-rlim 13463  df-sum 13660  df-ef 14014  df-sin 14016  df-cos 14017  df-pi 14019  df-struct 14845  df-ndx 14846  df-slot 14847  df-base 14848  df-sets 14849  df-ress 14850  df-plusg 14924  df-mulr 14925  df-starv 14926  df-sca 14927  df-vsca 14928  df-ip 14929  df-tset 14930  df-ple 14931  df-ds 14933  df-unif 14934  df-hom 14935  df-cco 14936  df-rest 15039  df-topn 15040  df-0g 15058  df-gsum 15059  df-topgen 15060  df-pt 15061  df-prds 15064  df-ordt 15117  df-xrs 15118  df-qtop 15123  df-imas 15124  df-xps 15126  df-mre 15202  df-mrc 15203  df-acs 15205  df-ps 16156  df-tsr 16157  df-plusf 16197  df-mgm 16198  df-sgrp 16237  df-mnd 16247  df-mhm 16292  df-submnd 16293  df-grp 16383  df-minusg 16384  df-sbg 16385  df-mulg 16386  df-subg 16524  df-cntz 16681  df-cmn 17126  df-abl 17127  df-mgp 17464  df-ur 17476  df-ring 17522  df-cring 17523  df-subrg 17749  df-abv 17788  df-lmod 17836  df-scaf 17837  df-sra 18140  df-rgmod 18141  df-psmet 18733  df-xmet 18734  df-met 18735  df-bl 18736  df-mopn 18737  df-fbas 18738  df-fg 18739  df-cnfld 18743  df-top 19693  df-bases 19695  df-topon 19696  df-topsp 19697  df-cld 19814  df-ntr 19815  df-cls 19816  df-nei 19894  df-lp 19932  df-perf 19933  df-cn 20023  df-cnp 20024  df-haus 20111  df-tx 20357  df-hmeo 20550  df-fil 20641  df-fm 20733  df-flim 20734  df-flf 20735  df-tmd 20865  df-tgp 20866  df-tsms 20919  df-trg 20956  df-xms 21117  df-ms 21118  df-tms 21119  df-nm 21397  df-ngp 21398  df-nrg 21400  df-nlm 21401  df-ii 21675  df-cncf 21676  df-limc 22564  df-dv 22565  df-log 23238  df-esum 28488  df-siga 28569  df-meas 28657 This theorem is referenced by:  measiuns  28678  measinblem  28681  sibfof  28801  dstrvprob  28929
 Copyright terms: Public domain W3C validator