dmvon

Description: Lebesgue measurable n-dimensional subsets of Reals. (Contributed by Glauco Siliprandi, 24-Dec-2020)

		Ref	Expression
	Hypothesis	dmvon.x	$⊢ φ \to X \in Fin$
	Assertion	dmvon	$⊢ φ \to dom voln (X) = CaraGen (voln* (X))$

Step	Hyp	Ref	Expression
1		dmvon.x	$⊢ φ \to X \in Fin$
2	1	vonval	$⊢ φ \to voln (X) = {voln* (X) ↾}_{CaraGen (voln* (X))}$
3	2	dmeqd	$⊢ φ \to dom voln (X) = dom ({voln* (X) ↾}_{CaraGen (voln* (X))})$
4	1	ovnome	$⊢ φ \to voln* (X) \in OutMeas$
5		eqid	$⊢ CaraGen (voln* (X)) = CaraGen (voln* (X))$
6	5	caragenss	$⊢ voln* (X) \in OutMeas \to CaraGen (voln* (X)) \subseteq dom voln* (X)$
7	4 6	syl	$⊢ φ \to CaraGen (voln* (X)) \subseteq dom voln* (X)$
8		ssdmres	$⊢ CaraGen (voln* (X)) \subseteq dom voln* (X) \leftrightarrow dom ({voln* (X) ↾}_{CaraGen (voln* (X))}) = CaraGen (voln* (X))$
9	7 8	sylib	$⊢ φ \to dom ({voln* (X) ↾}_{CaraGen (voln* (X))}) = CaraGen (voln* (X))$
10		eqidd	$⊢ φ \to CaraGen (voln* (X)) = CaraGen (voln* (X))$
11	3 9 10	3eqtrd	$⊢ φ \to dom voln (X) = CaraGen (voln* (X))$

Metamath Proof Explorer