Metamath Proof Explorer

Theorem isrnmeas

Description: The property of being a measure on an undefined base sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion isrnmeas 
|- ( M e. U. ran measures -> ( dom M e. U. ran sigAlgebra /\ ( M : dom M --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 df-meas 
 |-  measures = ( s e. U. ran sigAlgebra |-> { m | ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } )
2 vex 
 |-  s e. _V
3 ovex 
 |-  ( 0 [,] +oo ) e. _V
4 mapex 
 |-  ( ( s e. _V /\ ( 0 [,] +oo ) e. _V ) -> { m | m : s --> ( 0 [,] +oo ) } e. _V )
5 2 3 4 mp2an 
 |-  { m | m : s --> ( 0 [,] +oo ) } e. _V
6 simp1 
 |-  ( ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) -> m : s --> ( 0 [,] +oo ) )
7 6 ss2abi 
 |-  { m | ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } C_ { m | m : s --> ( 0 [,] +oo ) }
8 5 7 ssexi 
 |-  { m | ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } e. _V
9 feq1 
 |-  ( m = M -> ( m : s --> ( 0 [,] +oo ) <-> M : s --> ( 0 [,] +oo ) ) )
10 fveq1 
 |-  ( m = M -> ( m ` (/) ) = ( M ` (/) ) )
11 10 eqeq1d 
 |-  ( m = M -> ( ( m ` (/) ) = 0 <-> ( M ` (/) ) = 0 ) )
12 fveq1 
 |-  ( m = M -> ( m ` U. x ) = ( M ` U. x ) )
13 fveq1 
 |-  ( m = M -> ( m ` y ) = ( M ` y ) )
14 13 esumeq2sdv 
 |-  ( m = M -> sum* y e. x ( m ` y ) = sum* y e. x ( M ` y ) )
15 12 14 eqeq12d 
 |-  ( m = M -> ( ( m ` U. x ) = sum* y e. x ( m ` y ) <-> ( M ` U. x ) = sum* y e. x ( M ` y ) ) )
16 15 imbi2d 
 |-  ( m = M -> ( ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) <-> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) )
17 16 ralbidv 
 |-  ( m = M -> ( A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) <-> A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) )
18 9 11 17 3anbi123d 
 |-  ( m = M -> ( ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) <-> ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) ) )
19 1 8 18 abfmpunirn 
 |-  ( M e. U. ran measures <-> ( M e. _V /\ E. s e. U. ran sigAlgebra ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) ) )
20 19 simprbi 
 |-  ( M e. U. ran measures -> E. s e. U. ran sigAlgebra ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) )
21 fdm 
 |-  ( M : s --> ( 0 [,] +oo ) -> dom M = s )
22 21 3ad2ant1 
 |-  ( ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) -> dom M = s )
23 22 adantl 
 |-  ( ( s e. U. ran sigAlgebra /\ ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) ) -> dom M = s )
24 simpl 
 |-  ( ( s e. U. ran sigAlgebra /\ ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) ) -> s e. U. ran sigAlgebra )
25 23 24 eqeltrd 
 |-  ( ( s e. U. ran sigAlgebra /\ ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) ) -> dom M e. U. ran sigAlgebra )
26 simp1 
 |-  ( ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) -> M : s --> ( 0 [,] +oo ) )
27 feq2 
 |-  ( dom M = s -> ( M : dom M --> ( 0 [,] +oo ) <-> M : s --> ( 0 [,] +oo ) ) )
28 27 biimpar 
 |-  ( ( dom M = s /\ M : s --> ( 0 [,] +oo ) ) -> M : dom M --> ( 0 [,] +oo ) )
29 22 26 28 syl2anc 
 |-  ( ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) -> M : dom M --> ( 0 [,] +oo ) )
30 simp2 
 |-  ( ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) -> ( M ` (/) ) = 0 )
31 simp3 
 |-  ( ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) -> A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) )
32 pweq 
 |-  ( dom M = s -> ~P dom M = ~P s )
33 32 raleqdv 
 |-  ( dom M = s -> ( A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) <-> A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) )
34 33 biimpar 
 |-  ( ( dom M = s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) -> A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) )
35 22 31 34 syl2anc 
 |-  ( ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) -> A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) )
36 29 30 35 3jca 
 |-  ( ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) -> ( M : dom M --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) )
37 36 adantl 
 |-  ( ( s e. U. ran sigAlgebra /\ ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) ) -> ( M : dom M --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) )
38 25 37 jca 
 |-  ( ( s e. U. ran sigAlgebra /\ ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) ) -> ( dom M e. U. ran sigAlgebra /\ ( M : dom M --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) ) )
39 38 rexlimiva 
 |-  ( E. s e. U. ran sigAlgebra ( M : s --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) -> ( dom M e. U. ran sigAlgebra /\ ( M : dom M --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) ) )
40 20 39 syl 
 |-  ( M e. U. ran measures -> ( dom M e. U. ran sigAlgebra /\ ( M : dom M --> ( 0 [,] +oo ) /\ ( M ` (/) ) = 0 /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) ) )