Metamath Proof Explorer

Theorem ismea

Description: Express the predicate " M is a measure." Definition 112A of Fremlin1 p. 14. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( M e. Meas -> M e. Meas )
2 fex 
 |-  ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) -> M e. _V )
3 id 
 |-  ( z = M -> z = M )
4 dmeq 
 |-  ( z = M -> dom z = dom M )
5 3 4 feq12d 
 |-  ( z = M -> ( z : dom z --> ( 0 [,] +oo ) <-> M : dom M --> ( 0 [,] +oo ) ) )
6 4 eleq1d 
 |-  ( z = M -> ( dom z e. SAlg <-> dom M e. SAlg ) )
7 5 6 anbi12d 
 |-  ( z = M -> ( ( z : dom z --> ( 0 [,] +oo ) /\ dom z e. SAlg ) <-> ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) ) )
8 fveq1 
 |-  ( z = M -> ( z ` (/) ) = ( M ` (/) ) )
9 8 eqeq1d 
 |-  ( z = M -> ( ( z ` (/) ) = 0 <-> ( M ` (/) ) = 0 ) )
10 7 9 anbi12d 
 |-  ( z = M -> ( ( ( z : dom z --> ( 0 [,] +oo ) /\ dom z e. SAlg ) /\ ( z ` (/) ) = 0 ) <-> ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) /\ ( M ` (/) ) = 0 ) ) )
11 4 pweqd 
 |-  ( z = M -> ~P dom z = ~P dom M )
12 fveq1 
 |-  ( z = M -> ( z ` U. x ) = ( M ` U. x ) )
13 reseq1 
 |-  ( z = M -> ( z |` x ) = ( M |` x ) )
14 13 fveq2d 
 |-  ( z = M -> ( sum^ ` ( z |` x ) ) = ( sum^ ` ( M |` x ) ) )
15 12 14 eqeq12d 
 |-  ( z = M -> ( ( z ` U. x ) = ( sum^ ` ( z |` x ) ) <-> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) )
16 15 imbi2d 
 |-  ( z = M -> ( ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( z ` U. x ) = ( sum^ ` ( z |` x ) ) ) <-> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) ) )
17 11 16 raleqbidv 
 |-  ( z = M -> ( A. x e. ~P dom z ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( z ` U. x ) = ( sum^ ` ( z |` x ) ) ) <-> A. x e. ~P dom M ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = ( sum^ ` ( M |` x ) ) ) ) )
18 10 17 anbi12d 
 |-  ( z = M -> ( ( ( ( z : dom z --> ( 0 [,] +oo ) /\ dom z e. SAlg ) /\ ( z ` (/) ) = 0 ) /\ A. x e. ~P dom z ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( z ` U. x ) = ( sum^ ` ( z |` x ) ) ) ) <-> ( ( ( 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 ) ) ) ) ) )
19 df-mea 
 |-  Meas = { z | ( ( ( z : dom z --> ( 0 [,] +oo ) /\ dom z e. SAlg ) /\ ( z ` (/) ) = 0 ) /\ A. x e. ~P dom z ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( z ` U. x ) = ( sum^ ` ( z |` x ) ) ) ) }
20 18 19 elab2g 
 |-  ( M e. _V -> ( 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 ) ) ) ) ) )
21 2 20 syl 
 |-  ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) -> ( 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 ) ) ) ) ) )
22 21 ad2antrr 
 |-  ( ( ( ( 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 ) ) ) ) -> ( 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 ) ) ) ) ) )
23 22 ibir 
 |-  ( ( ( ( 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 ) ) ) ) -> M e. Meas )
24 18 19 elab2g 
 |-  ( M e. Meas -> ( 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 ) ) ) ) ) )
25 1 23 24 pm5.21nii 
 |-  ( 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 ) ) ) ) )