This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem volres

Description: A self-referencing abbreviated definition of the Lebesgue measure. (Contributed by Mario Carneiro, 19-Mar-2014)

Ref Expression
Assertion volres 
|- vol = ( vol* |` dom vol )

Proof

Step Hyp Ref Expression
1 resdmres 
 |-  ( vol* |` dom ( vol* |` { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) } ) ) = ( vol* |` { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) } )
2 df-vol 
 |-  vol = ( vol* |` { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) } )
3 2 dmeqi 
 |-  dom vol = dom ( vol* |` { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) } )
4 3 reseq2i 
 |-  ( vol* |` dom vol ) = ( vol* |` dom ( vol* |` { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) } ) )
5 1 4 2 3eqtr4ri 
 |-  vol = ( vol* |` dom vol )