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* ↾ { 𝑥 ∣ ∀ 𝑦 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) ) } ) ) = ( vol* ↾ { 𝑥 ∣ ∀ 𝑦 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) ) } )
2 df-vol ⊢ vol = ( vol* ↾ { 𝑥 ∣ ∀ 𝑦 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) ) } )
3 2 dmeqi ⊢ dom vol = dom ( vol* ↾ { 𝑥 ∣ ∀ 𝑦 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) ) } )
4 3 reseq2i ⊢ ( vol* ↾ dom vol ) = ( vol* ↾ dom ( vol* ↾ { 𝑥 ∣ ∀ 𝑦 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑦 ) = ( ( vol* ‘ ( 𝑦 ∩ 𝑥 ) ) + ( vol* ‘ ( 𝑦 ∖ 𝑥 ) ) ) } ) )
5 1 4 2 3eqtr4ri ⊢ vol = ( vol* ↾ dom vol )