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 φ X Fin
voncmpl.s S = dom voln X
voncmpl.e φ E dom voln X
voncmpl.z φ voln X E = 0
voncmpl.f φ F E
Assertion voncmpl φ F S

Proof

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