Metamath Proof Explorer

Theorem omsmeas

Description: The restriction of a constructed outer measure to Caratheodory measurable sets is a measure. This theorem allows to construct measures from pre-measures with the required characteristics, as for the Lebesgue measure. (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses omsmeas.m 
|- M = ( toOMeas ` R )
omsmeas.s 
|- S = ( toCaraSiga ` M )
omsmeas.o 
|- ( ph -> Q e. V )
omsmeas.r 
|- ( ph -> R : Q --> ( 0 [,] +oo ) )
omsmeas.d 
|- ( ph -> (/) e. dom R )
omsmeas.0 
|- ( ph -> ( R ` (/) ) = 0 )
Assertion omsmeas 
|- ( ph -> ( M |` S ) e. ( measures ` S ) )

Proof

Step Hyp Ref Expression
1 omsmeas.m 
 |-  M = ( toOMeas ` R )
2 omsmeas.s 
 |-  S = ( toCaraSiga ` M )
3 omsmeas.o 
 |-  ( ph -> Q e. V )
4 omsmeas.r 
 |-  ( ph -> R : Q --> ( 0 [,] +oo ) )
5 omsmeas.d 
 |-  ( ph -> (/) e. dom R )
6 omsmeas.0 
 |-  ( ph -> ( R ` (/) ) = 0 )
7 omsf 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> ( toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
8 3 4 7 syl2anc 
 |-  ( ph -> ( toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )
9 1 a1i 
 |-  ( ph -> M = ( toOMeas ` R ) )
10 4 fdmd 
 |-  ( ph -> dom R = Q )
11 10 eqcomd 
 |-  ( ph -> Q = dom R )
12 11 unieqd 
 |-  ( ph -> U. Q = U. dom R )
13 12 pweqd 
 |-  ( ph -> ~P U. Q = ~P U. dom R )
14 9 13 feq12d 
 |-  ( ph -> ( M : ~P U. Q --> ( 0 [,] +oo ) <-> ( toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) ) )
15 8 14 mpbird 
 |-  ( ph -> M : ~P U. Q --> ( 0 [,] +oo ) )
16 3 uniexd 
 |-  ( ph -> U. Q e. _V )
17 16 15 carsgcl 
 |-  ( ph -> ( toCaraSiga ` M ) C_ ~P U. Q )
18 2 17 eqsstrid 
 |-  ( ph -> S C_ ~P U. Q )
19 15 18 fssresd 
 |-  ( ph -> ( M |` S ) : S --> ( 0 [,] +oo ) )
20 1 3 4 5 6 oms0 
 |-  ( ph -> ( M ` (/) ) = 0 )
21 16 15 20 0elcarsg 
 |-  ( ph -> (/) e. ( toCaraSiga ` M ) )
22 21 2 eleqtrrdi 
 |-  ( ph -> (/) e. S )
23 fvres 
 |-  ( (/) e. S -> ( ( M |` S ) ` (/) ) = ( M ` (/) ) )
24 22 23 syl 
 |-  ( ph -> ( ( M |` S ) ` (/) ) = ( M ` (/) ) )
25 24 20 eqtrd 
 |-  ( ph -> ( ( M |` S ) ` (/) ) = 0 )
26 nfcv 
 |-  F/_ g f
27 nfcv 
 |-  F/_ f g
28 id 
 |-  ( f = g -> f = g )
29 26 27 28 cbvdisj 
 |-  ( Disj_ f e. e f <-> Disj_ g e. e g )
30 29 anbi2i 
 |-  ( ( e ~<_ _om /\ Disj_ f e. e f ) <-> ( e ~<_ _om /\ Disj_ g e. e g ) )
31 3 ad2antrr 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> Q e. V )
32 4 ad2antrr 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> R : Q --> ( 0 [,] +oo ) )
33 simplr 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> e e. ~P S )
34 33 elpwid 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> e C_ S )
35 18 ad2antrr 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> S C_ ~P U. Q )
36 34 35 sstrd 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> e C_ ~P U. Q )
37 36 sselda 
 |-  ( ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) /\ f e. e ) -> f e. ~P U. Q )
38 37 elpwid 
 |-  ( ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) /\ f e. e ) -> f C_ U. Q )
39 simprl 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> e ~<_ _om )
40 1 31 32 38 39 omssubadd 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> ( M ` U_ f e. e f ) <_ sum* f e. e ( M ` f ) )
41 16 ad2antrr 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> U. Q e. _V )
42 15 ad2antrr 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> M : ~P U. Q --> ( 0 [,] +oo ) )
43 20 ad2antrr 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> ( M ` (/) ) = 0 )
44 uniiun 
 |-  U. x = U_ y e. x y
45 44 fveq2i 
 |-  ( M ` U. x ) = ( M ` U_ y e. x y )
46 3 3ad2ant1 
 |-  ( ( ph /\ x ~<_ _om /\ x C_ ~P U. Q ) -> Q e. V )
47 4 3ad2ant1 
 |-  ( ( ph /\ x ~<_ _om /\ x C_ ~P U. Q ) -> R : Q --> ( 0 [,] +oo ) )
48 simpl3 
 |-  ( ( ( ph /\ x ~<_ _om /\ x C_ ~P U. Q ) /\ y e. x ) -> x C_ ~P U. Q )
49 simpr 
 |-  ( ( ( ph /\ x ~<_ _om /\ x C_ ~P U. Q ) /\ y e. x ) -> y e. x )
50 48 49 sseldd 
 |-  ( ( ( ph /\ x ~<_ _om /\ x C_ ~P U. Q ) /\ y e. x ) -> y e. ~P U. Q )
51 50 elpwid 
 |-  ( ( ( ph /\ x ~<_ _om /\ x C_ ~P U. Q ) /\ y e. x ) -> y C_ U. Q )
52 simp2 
 |-  ( ( ph /\ x ~<_ _om /\ x C_ ~P U. Q ) -> x ~<_ _om )
53 1 46 47 51 52 omssubadd 
 |-  ( ( ph /\ x ~<_ _om /\ x C_ ~P U. Q ) -> ( M ` U_ y e. x y ) <_ sum* y e. x ( M ` y ) )
54 45 53 eqbrtrid 
 |-  ( ( ph /\ x ~<_ _om /\ x C_ ~P U. Q ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
55 54 3adant1r 
 |-  ( ( ( ph /\ e e. ~P S ) /\ x ~<_ _om /\ x C_ ~P U. Q ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
56 55 3adant1r 
 |-  ( ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) /\ x ~<_ _om /\ x C_ ~P U. Q ) -> ( M ` U. x ) <_ sum* y e. x ( M ` y ) )
57 3 3ad2ant1 
 |-  ( ( ph /\ x C_ y /\ y e. ~P U. Q ) -> Q e. V )
58 4 3ad2ant1 
 |-  ( ( ph /\ x C_ y /\ y e. ~P U. Q ) -> R : Q --> ( 0 [,] +oo ) )
59 simp2 
 |-  ( ( ph /\ x C_ y /\ y e. ~P U. Q ) -> x C_ y )
60 elpwi 
 |-  ( y e. ~P U. Q -> y C_ U. Q )
61 60 3ad2ant3 
 |-  ( ( ph /\ x C_ y /\ y e. ~P U. Q ) -> y C_ U. Q )
62 1 57 58 59 61 omsmon 
 |-  ( ( ph /\ x C_ y /\ y e. ~P U. Q ) -> ( M ` x ) <_ ( M ` y ) )
63 62 3adant1r 
 |-  ( ( ( ph /\ e e. ~P S ) /\ x C_ y /\ y e. ~P U. Q ) -> ( M ` x ) <_ ( M ` y ) )
64 63 3adant1r 
 |-  ( ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) /\ x C_ y /\ y e. ~P U. Q ) -> ( M ` x ) <_ ( M ` y ) )
65 elpwi 
 |-  ( e e. ~P S -> e C_ S )
66 65 ad2antlr 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> e C_ S )
67 66 2 sseqtrdi 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> e C_ ( toCaraSiga ` M ) )
68 41 42 43 56 64 39 67 carsgclctun 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> U. e e. ( toCaraSiga ` M ) )
69 68 2 eleqtrrdi 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> U. e e. S )
70 fvres 
 |-  ( U. e e. S -> ( ( M |` S ) ` U. e ) = ( M ` U. e ) )
71 uniiun 
 |-  U. e = U_ f e. e f
72 71 fveq2i 
 |-  ( M ` U. e ) = ( M ` U_ f e. e f )
73 70 72 eqtrdi 
 |-  ( U. e e. S -> ( ( M |` S ) ` U. e ) = ( M ` U_ f e. e f ) )
74 69 73 syl 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> ( ( M |` S ) ` U. e ) = ( M ` U_ f e. e f ) )
75 nfv 
 |-  F/ f ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) )
76 66 sselda 
 |-  ( ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) /\ f e. e ) -> f e. S )
77 fvres 
 |-  ( f e. S -> ( ( M |` S ) ` f ) = ( M ` f ) )
78 76 77 syl 
 |-  ( ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) /\ f e. e ) -> ( ( M |` S ) ` f ) = ( M ` f ) )
79 78 ralrimiva 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> A. f e. e ( ( M |` S ) ` f ) = ( M ` f ) )
80 75 79 esumeq2d 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> sum* f e. e ( ( M |` S ) ` f ) = sum* f e. e ( M ` f ) )
81 40 74 80 3brtr4d 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> ( ( M |` S ) ` U. e ) <_ sum* f e. e ( ( M |` S ) ` f ) )
82 snex 
 |-  { (/) } e. _V
83 82 a1i 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> { (/) } e. _V )
84 42 adantr 
 |-  ( ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) /\ f e. e ) -> M : ~P U. Q --> ( 0 [,] +oo ) )
85 84 37 ffvelrnd 
 |-  ( ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) /\ f e. e ) -> ( M ` f ) e. ( 0 [,] +oo ) )
86 elsni 
 |-  ( f e. { (/) } -> f = (/) )
87 86 fveq2d 
 |-  ( f e. { (/) } -> ( M ` f ) = ( M ` (/) ) )
88 87 43 sylan9eqr 
 |-  ( ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) /\ f e. { (/) } ) -> ( M ` f ) = 0 )
89 33 83 85 88 esumpad2 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> sum* f e. ( e \ { (/) } ) ( M ` f ) = sum* f e. e ( M ` f ) )
90 neldifsnd 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> -. (/) e. ( e \ { (/) } ) )
91 difss 
 |-  ( e \ { (/) } ) C_ e
92 ssdomg 
 |-  ( e e. ~P S -> ( ( e \ { (/) } ) C_ e -> ( e \ { (/) } ) ~<_ e ) )
93 33 91 92 mpisyl 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> ( e \ { (/) } ) ~<_ e )
94 domtr 
 |-  ( ( ( e \ { (/) } ) ~<_ e /\ e ~<_ _om ) -> ( e \ { (/) } ) ~<_ _om )
95 93 39 94 syl2anc 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> ( e \ { (/) } ) ~<_ _om )
96 67 ssdifssd 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> ( e \ { (/) } ) C_ ( toCaraSiga ` M ) )
97 simprr 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> Disj_ g e. e g )
98 nfcv 
 |-  F/_ y g
99 nfcv 
 |-  F/_ g y
100 id 
 |-  ( g = y -> g = y )
101 98 99 100 cbvdisj 
 |-  ( Disj_ g e. e g <-> Disj_ y e. e y )
102 97 101 sylib 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> Disj_ y e. e y )
103 disjss1 
 |-  ( ( e \ { (/) } ) C_ e -> ( Disj_ y e. e y -> Disj_ y e. ( e \ { (/) } ) y ) )
104 91 102 103 mpsyl 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> Disj_ y e. ( e \ { (/) } ) y )
105 41 42 43 56 90 95 96 104 64 carsggect 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> sum* f e. ( e \ { (/) } ) ( M ` f ) <_ ( M ` U. ( e \ { (/) } ) ) )
106 89 105 eqbrtrrd 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> sum* f e. e ( M ` f ) <_ ( M ` U. ( e \ { (/) } ) ) )
107 unidif0 
 |-  U. ( e \ { (/) } ) = U. e
108 107 fveq2i 
 |-  ( M ` U. ( e \ { (/) } ) ) = ( M ` U. e )
109 106 108 breqtrdi 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> sum* f e. e ( M ` f ) <_ ( M ` U. e ) )
110 69 70 syl 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> ( ( M |` S ) ` U. e ) = ( M ` U. e ) )
111 109 80 110 3brtr4d 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> sum* f e. e ( ( M |` S ) ` f ) <_ ( ( M |` S ) ` U. e ) )
112 81 111 jca 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> ( ( ( M |` S ) ` U. e ) <_ sum* f e. e ( ( M |` S ) ` f ) /\ sum* f e. e ( ( M |` S ) ` f ) <_ ( ( M |` S ) ` U. e ) ) )
113 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
114 19 ad2antrr 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> ( M |` S ) : S --> ( 0 [,] +oo ) )
115 114 69 ffvelrnd 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> ( ( M |` S ) ` U. e ) e. ( 0 [,] +oo ) )
116 113 115 sselid 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> ( ( M |` S ) ` U. e ) e. RR* )
117 114 adantr 
 |-  ( ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) /\ f e. e ) -> ( M |` S ) : S --> ( 0 [,] +oo ) )
118 117 76 ffvelrnd 
 |-  ( ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) /\ f e. e ) -> ( ( M |` S ) ` f ) e. ( 0 [,] +oo ) )
119 118 ralrimiva 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> A. f e. e ( ( M |` S ) ` f ) e. ( 0 [,] +oo ) )
120 nfcv 
 |-  F/_ f e
121 120 esumcl 
 |-  ( ( e e. ~P S /\ A. f e. e ( ( M |` S ) ` f ) e. ( 0 [,] +oo ) ) -> sum* f e. e ( ( M |` S ) ` f ) e. ( 0 [,] +oo ) )
122 33 119 121 syl2anc 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> sum* f e. e ( ( M |` S ) ` f ) e. ( 0 [,] +oo ) )
123 113 122 sselid 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> sum* f e. e ( ( M |` S ) ` f ) e. RR* )
124 xrletri3 
 |-  ( ( ( ( M |` S ) ` U. e ) e. RR* /\ sum* f e. e ( ( M |` S ) ` f ) e. RR* ) -> ( ( ( M |` S ) ` U. e ) = sum* f e. e ( ( M |` S ) ` f ) <-> ( ( ( M |` S ) ` U. e ) <_ sum* f e. e ( ( M |` S ) ` f ) /\ sum* f e. e ( ( M |` S ) ` f ) <_ ( ( M |` S ) ` U. e ) ) ) )
125 116 123 124 syl2anc 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> ( ( ( M |` S ) ` U. e ) = sum* f e. e ( ( M |` S ) ` f ) <-> ( ( ( M |` S ) ` U. e ) <_ sum* f e. e ( ( M |` S ) ` f ) /\ sum* f e. e ( ( M |` S ) ` f ) <_ ( ( M |` S ) ` U. e ) ) ) )
126 112 125 mpbird 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ g e. e g ) ) -> ( ( M |` S ) ` U. e ) = sum* f e. e ( ( M |` S ) ` f ) )
127 30 126 sylan2b 
 |-  ( ( ( ph /\ e e. ~P S ) /\ ( e ~<_ _om /\ Disj_ f e. e f ) ) -> ( ( M |` S ) ` U. e ) = sum* f e. e ( ( M |` S ) ` f ) )
128 127 ex 
 |-  ( ( ph /\ e e. ~P S ) -> ( ( e ~<_ _om /\ Disj_ f e. e f ) -> ( ( M |` S ) ` U. e ) = sum* f e. e ( ( M |` S ) ` f ) ) )
129 128 ralrimiva 
 |-  ( ph -> A. e e. ~P S ( ( e ~<_ _om /\ Disj_ f e. e f ) -> ( ( M |` S ) ` U. e ) = sum* f e. e ( ( M |` S ) ` f ) ) )
130 19 25 129 3jca 
 |-  ( ph -> ( ( M |` S ) : S --> ( 0 [,] +oo ) /\ ( ( M |` S ) ` (/) ) = 0 /\ A. e e. ~P S ( ( e ~<_ _om /\ Disj_ f e. e f ) -> ( ( M |` S ) ` U. e ) = sum* f e. e ( ( M |` S ) ` f ) ) ) )
131 16 15 20 54 62 carsgsiga 
 |-  ( ph -> ( toCaraSiga ` M ) e. ( sigAlgebra ` U. Q ) )
132 2 131 eqeltrid 
 |-  ( ph -> S e. ( sigAlgebra ` U. Q ) )
133 elrnsiga 
 |-  ( S e. ( sigAlgebra ` U. Q ) -> S e. U. ran sigAlgebra )
134 ismeas 
 |-  ( S e. U. ran sigAlgebra -> ( ( M |` S ) e. ( measures ` S ) <-> ( ( M |` S ) : S --> ( 0 [,] +oo ) /\ ( ( M |` S ) ` (/) ) = 0 /\ A. e e. ~P S ( ( e ~<_ _om /\ Disj_ f e. e f ) -> ( ( M |` S ) ` U. e ) = sum* f e. e ( ( M |` S ) ` f ) ) ) ) )
135 132 133 134 3syl 
 |-  ( ph -> ( ( M |` S ) e. ( measures ` S ) <-> ( ( M |` S ) : S --> ( 0 [,] +oo ) /\ ( ( M |` S ) ` (/) ) = 0 /\ A. e e. ~P S ( ( e ~<_ _om /\ Disj_ f e. e f ) -> ( ( M |` S ) ` U. e ) = sum* f e. e ( ( M |` S ) ` f ) ) ) ) )
136 130 135 mpbird 
 |-  ( ph -> ( M |` S ) e. ( measures ` S ) )