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 
|- ( ph -> X e. Fin )
Assertion dmvon 
|- ( ph -> dom ( voln ` X ) = ( CaraGen ` ( voln* ` X ) ) )

Proof

Step Hyp Ref Expression
1 dmvon.x 
 |-  ( ph -> X e. Fin )
2 1 vonval 
 |-  ( ph -> ( voln ` X ) = ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) )
3 2 dmeqd 
 |-  ( ph -> dom ( voln ` X ) = dom ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) )
4 1 ovnome 
 |-  ( ph -> ( voln* ` X ) e. OutMeas )
5 eqid 
 |-  ( CaraGen ` ( voln* ` X ) ) = ( CaraGen ` ( voln* ` X ) )
6 5 caragenss 
 |-  ( ( voln* ` X ) e. OutMeas -> ( CaraGen ` ( voln* ` X ) ) C_ dom ( voln* ` X ) )
7 4 6 syl 
 |-  ( ph -> ( CaraGen ` ( voln* ` X ) ) C_ dom ( voln* ` X ) )
8 ssdmres 
 |-  ( ( CaraGen ` ( voln* ` X ) ) C_ dom ( voln* ` X ) <-> dom ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) = ( CaraGen ` ( voln* ` X ) ) )
9 7 8 sylib 
 |-  ( ph -> dom ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) = ( CaraGen ` ( voln* ` X ) ) )
10 eqidd 
 |-  ( ph -> ( CaraGen ` ( voln* ` X ) ) = ( CaraGen ` ( voln* ` X ) ) )
11 3 9 10 3eqtrd 
 |-  ( ph -> dom ( voln ` X ) = ( CaraGen ` ( voln* ` X ) ) )