Metamath Proof Explorer

Theorem voncmpl

Description: The Lebesgue measure is complete. See Definition 112Df of Fremlin1 p. 19. This is an observation written after Definition 115E of Fremlin1 p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses voncmpl.x 
|- ( ph -> X e. Fin )
voncmpl.s 
|- S = dom ( voln ` X )
voncmpl.e 
|- ( ph -> E e. dom ( voln ` X ) )
voncmpl.z 
|- ( ph -> ( ( voln ` X ) ` E ) = 0 )
voncmpl.f 
|- ( ph -> F C_ E )
Assertion voncmpl 
|- ( ph -> F e. S )

Proof

Step Hyp Ref Expression
1 voncmpl.x 
 |-  ( ph -> X e. Fin )
2 voncmpl.s 
 |-  S = dom ( voln ` X )
3 voncmpl.e 
 |-  ( ph -> E e. dom ( voln ` X ) )
4 voncmpl.z 
 |-  ( ph -> ( ( voln ` X ) ` E ) = 0 )
5 voncmpl.f 
 |-  ( ph -> F C_ E )
6 1 ovnome 
 |-  ( ph -> ( voln* ` X ) e. OutMeas )
7 eqid 
 |-  U. dom ( voln* ` X ) = U. dom ( voln* ` X )
8 1 dmvon 
 |-  ( ph -> dom ( voln ` X ) = ( CaraGen ` ( voln* ` X ) ) )
9 eqid 
 |-  ( CaraGen ` ( voln* ` X ) ) = ( CaraGen ` ( voln* ` X ) )
10 9 caragenss 
 |-  ( ( voln* ` X ) e. OutMeas -> ( CaraGen ` ( voln* ` X ) ) C_ dom ( voln* ` X ) )
11 6 10 syl 
 |-  ( ph -> ( CaraGen ` ( voln* ` X ) ) C_ dom ( voln* ` X ) )
12 8 11 eqsstrd 
 |-  ( ph -> dom ( voln ` X ) C_ dom ( voln* ` X ) )
13 12 3 sseldd 
 |-  ( ph -> E e. dom ( voln* ` X ) )
14 elssuni 
 |-  ( E e. dom ( voln* ` X ) -> E C_ U. dom ( voln* ` X ) )
15 13 14 syl 
 |-  ( ph -> E C_ U. dom ( voln* ` X ) )
16 5 15 sstrd 
 |-  ( ph -> F C_ U. dom ( voln* ` X ) )
17 4 eqcomd 
 |-  ( ph -> 0 = ( ( voln ` X ) ` E ) )
18 1 vonval 
 |-  ( ph -> ( voln ` X ) = ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) )
19 18 fveq1d 
 |-  ( ph -> ( ( voln ` X ) ` E ) = ( ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) ` E ) )
20 17 19 eqtrd 
 |-  ( ph -> 0 = ( ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) ` E ) )
21 2 a1i 
 |-  ( ph -> S = dom ( voln ` X ) )
22 21 8 eqtr2d 
 |-  ( ph -> ( CaraGen ` ( voln* ` X ) ) = S )
23 22 reseq2d 
 |-  ( ph -> ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) = ( ( voln* ` X ) |` S ) )
24 23 fveq1d 
 |-  ( ph -> ( ( ( voln* ` X ) |` ( CaraGen ` ( voln* ` X ) ) ) ` E ) = ( ( ( voln* ` X ) |` S ) ` E ) )
25 3 2 eleqtrrdi 
 |-  ( ph -> E e. S )
26 fvres 
 |-  ( E e. S -> ( ( ( voln* ` X ) |` S ) ` E ) = ( ( voln* ` X ) ` E ) )
27 25 26 syl 
 |-  ( ph -> ( ( ( voln* ` X ) |` S ) ` E ) = ( ( voln* ` X ) ` E ) )
28 20 24 27 3eqtrrd 
 |-  ( ph -> ( ( voln* ` X ) ` E ) = 0 )
29 6 7 15 28 5 omess0 
 |-  ( ph -> ( ( voln* ` X ) ` F ) = 0 )
30 6 7 16 29 9 caragencmpl 
 |-  ( ph -> F e. ( CaraGen ` ( voln* ` X ) ) )
31 30 22 eleqtrd 
 |-  ( ph -> F e. S )