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