Theorem dmvon

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

	Ref	Expression
Hypothesis	dmvon.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
Assertion	dmvon	⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dmvon.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2	1	vonval	⊢ ( 𝜑 → ( voln ‘ 𝑋 ) = ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) )
3	2	dmeqd	⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) = dom ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) )
4	1	ovnome	⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) ∈ OutMeas )
5		eqid	⊢ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) )
6	5	caragenss	⊢ ( ( voln* ‘ 𝑋 ) ∈ OutMeas → ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ⊆ dom ( voln* ‘ 𝑋 ) )
7	4 6	syl	⊢ ( 𝜑 → ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ⊆ dom ( voln* ‘ 𝑋 ) )
8		ssdmres	⊢ ( ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ⊆ dom ( voln* ‘ 𝑋 ) ↔ dom ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
9	7 8	sylib	⊢ ( 𝜑 → dom ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
10		eqidd	⊢ ( 𝜑 → ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
11	3 9 10	3eqtrd	⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )