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

Theorem measun 29029
 Description: The measure the union of two disjoint sets is the sum of their measures. (Contributed by Thierry Arnoux, 10-Mar-2017.)
Assertion
Ref Expression
measun measures

Proof of Theorem measun
StepHypRef Expression
1 simp1 1005 . . 3 measures measures
2 measbase 29015 . . . . 5 measures sigAlgebra
323ad2ant1 1026 . . . 4 measures sigAlgebra
4 simp2l 1031 . . . 4 measures
5 simp2r 1032 . . . 4 measures
6 unelsiga 28952 . . . 4 sigAlgebra
73, 4, 5, 6syl3anc 1264 . . 3 measures
8 ssun2 3630 . . . 4
98a1i 11 . . 3 measures
10 measxun2 29028 . . 3 measures
111, 7, 5, 9, 10syl121anc 1269 . 2 measures
12 difun2 3875 . . . . . 6
13 inundif 3873 . . . . . . 7
14 uneq1 3613 . . . . . . . 8
15 uncom 3610 . . . . . . . . 9
16 un0 3787 . . . . . . . . 9
1715, 16eqtri 2451 . . . . . . . 8
1814, 17syl6eq 2479 . . . . . . 7
1913, 18syl5reqr 2478 . . . . . 6
2012, 19syl5eq 2475 . . . . 5
2120fveq2d 5882 . . . 4
2221oveq2d 6318 . . 3