Theorem unidmvon

Description: Base set of the n-dimensional Lebesgue measure. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	unidmvon.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	unidmvon.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
Assertion	unidmvon	⊢ ( 𝜑 → ∪ 𝑆 = ( ℝ ↑m 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		unidmvon.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		unidmvon.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
3	2	a1i	⊢ ( 𝜑 → 𝑆 = dom ( voln ‘ 𝑋 ) )
4	1	dmvon	⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
5	3 4	eqtrd	⊢ ( 𝜑 → 𝑆 = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
6	5	unieqd	⊢ ( 𝜑 → ∪ 𝑆 = ∪ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
7	1	ovnome	⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) ∈ OutMeas )
8		eqid	⊢ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) )
9	7 8	caragenuni	⊢ ( 𝜑 → ∪ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) = ∪ dom ( voln* ‘ 𝑋 ) )
10	1	unidmovn	⊢ ( 𝜑 → ∪ dom ( voln* ‘ 𝑋 ) = ( ℝ ↑m 𝑋 ) )
11	6 9 10	3eqtrd	⊢ ( 𝜑 → ∪ 𝑆 = ( ℝ ↑m 𝑋 ) )