Metamath Proof Explorer

Theorem dmvon

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

Ref Expression
Hypothesis dmvon.x ⊢ φ → X ∈ Fin
Assertion dmvon ⊢ φ → dom ⁡ voln ⁡ X = CaraGen ⁡ voln* ⁡ X

Proof

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