Theorem vonmblss

Description: n-dimensional Lebesgue measurable sets are subsets of the n-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypothesis	vonmblss.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
Assertion	vonmblss	⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) ⊆ 𝒫 ( ℝ ↑m 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		vonmblss.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2	1	dmvon	⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
3	1	ovnome	⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) ∈ OutMeas )
4		eqid	⊢ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) )
5	4	caragenss	⊢ ( ( voln* ‘ 𝑋 ) ∈ OutMeas → ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ⊆ dom ( voln* ‘ 𝑋 ) )
6	3 5	syl	⊢ ( 𝜑 → ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ⊆ dom ( voln* ‘ 𝑋 ) )
7	1	dmovn	⊢ ( 𝜑 → dom ( voln* ‘ 𝑋 ) = 𝒫 ( ℝ ↑m 𝑋 ) )
8	6 7	sseqtrd	⊢ ( 𝜑 → ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ⊆ 𝒫 ( ℝ ↑m 𝑋 ) )
9	2 8	eqsstrd	⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) ⊆ 𝒫 ( ℝ ↑m 𝑋 ) )