Theorem rrnmbl

Description: The set of n-dimensional Real numbers is Lebesgue measurable. (Contributed by Glauco Siliprandi, 24-Dec-2020)

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

Proof

Step	Hyp	Ref	Expression
1		rrnmbl.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2	1	ovnome	⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) ∈ OutMeas )
3		eqid	⊢ ∪ dom ( voln* ‘ 𝑋 ) = ∪ dom ( voln* ‘ 𝑋 )
4		eqid	⊢ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) )
5	2 3 4	caragenunidm	⊢ ( 𝜑 → ∪ dom ( voln* ‘ 𝑋 ) ∈ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
6	1	dmovn	⊢ ( 𝜑 → dom ( voln* ‘ 𝑋 ) = 𝒫 ( ℝ ↑m 𝑋 ) )
7	6	unieqd	⊢ ( 𝜑 → ∪ dom ( voln* ‘ 𝑋 ) = ∪ 𝒫 ( ℝ ↑m 𝑋 ) )
8		unipw	⊢ ∪ 𝒫 ( ℝ ↑m 𝑋 ) = ( ℝ ↑m 𝑋 )
9	8	a1i	⊢ ( 𝜑 → ∪ 𝒫 ( ℝ ↑m 𝑋 ) = ( ℝ ↑m 𝑋 ) )
10	7 9	eqtr2d	⊢ ( 𝜑 → ( ℝ ↑m 𝑋 ) = ∪ dom ( voln* ‘ 𝑋 ) )
11	1	dmvon	⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
12	10 11	eleq12d	⊢ ( 𝜑 → ( ( ℝ ↑m 𝑋 ) ∈ dom ( voln ‘ 𝑋 ) ↔ ∪ dom ( voln* ‘ 𝑋 ) ∈ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) )
13	5 12	mpbird	⊢ ( 𝜑 → ( ℝ ↑m 𝑋 ) ∈ dom ( voln ‘ 𝑋 ) )