Theorem meaf

Description: A measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	meaf.m	|- ( ph -> M e. Meas )
	meaf.s	|- S = dom M
Assertion	meaf	|- ( ph -> M : S --> ( 0 [,] +oo ) )

Proof

Step	Hyp	Ref	Expression
1		meaf.m	|- ( ph -> M e. Meas )
2		meaf.s	|- S = dom M
3		ismea	|- ( M e. Meas <-> ( ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) /\ ( M ` (/) ) = 0 ) /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) ) )
4	1 3	sylib	|- ( ph -> ( ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) /\ ( M ` (/) ) = 0 ) /\ A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) ) )
5	4	simpld	|- ( ph -> ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) /\ ( M ` (/) ) = 0 ) )
6	5	simplld	|- ( ph -> M : dom M --> ( 0 [,] +oo ) )
7	2	a1i	|- ( ph -> S = dom M )
8	7	feq2d	|- ( ph -> ( M : S --> ( 0 [,] +oo ) <-> M : dom M --> ( 0 [,] +oo ) ) )
9	6 8	mpbird	|- ( ph -> M : S --> ( 0 [,] +oo ) )