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}^{*}\upharpoonright }_{\mathrm{dom}vol}$$

Proof

Step	Hyp	Ref	Expression
1		resdmres	$$⊢{{vol}^{*}\upharpoonright }_{\mathrm{dom}\left({{vol}^{*}\upharpoonright }_{\left\{x|\forall y\in {{vol}^{*}}^{-1}\left[ℝ\right]{vol}^{*}\left(y\right)={vol}^{*}\left(y\cap x\right)+{vol}^{*}\left(y\setminus x\right)\right\}}\right)}={{vol}^{*}\upharpoonright }_{\left\{x|\forall y\in {{vol}^{*}}^{-1}\left[ℝ\right]{vol}^{*}\left(y\right)={vol}^{*}\left(y\cap x\right)+{vol}^{*}\left(y\setminus x\right)\right\}}$$
2		df-vol	$$⊢vol={{vol}^{*}\upharpoonright }_{\left\{x|\forall y\in {{vol}^{*}}^{-1}\left[ℝ\right]{vol}^{*}\left(y\right)={vol}^{*}\left(y\cap x\right)+{vol}^{*}\left(y\setminus x\right)\right\}}$$
3	2	dmeqi	$$⊢\mathrm{dom}vol=\mathrm{dom}\left({{vol}^{*}\upharpoonright }_{\left\{x|\forall y\in {{vol}^{*}}^{-1}\left[ℝ\right]{vol}^{*}\left(y\right)={vol}^{*}\left(y\cap x\right)+{vol}^{*}\left(y\setminus x\right)\right\}}\right)$$
4	3	reseq2i	$$⊢{{vol}^{*}\upharpoonright }_{\mathrm{dom}vol}={{vol}^{*}\upharpoonright }_{\mathrm{dom}\left({{vol}^{*}\upharpoonright }_{\left\{x|\forall y\in {{vol}^{*}}^{-1}\left[ℝ\right]{vol}^{*}\left(y\right)={vol}^{*}\left(y\cap x\right)+{vol}^{*}\left(y\setminus x\right)\right\}}\right)}$$
5	1 4 2	3eqtr4ri	$$⊢vol={{vol}^{*}\upharpoonright }_{\mathrm{dom}vol}$$