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 ⊢ ( 𝜑 → 𝑋 ∈ Fin )
voncmpl.s ⊢ 𝑆 = dom ( voln ‘ 𝑋 )
voncmpl.e ⊢ ( 𝜑 → 𝐸 ∈ dom ( voln ‘ 𝑋 ) )
voncmpl.z ⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐸 ) = 0 )
voncmpl.f ⊢ ( 𝜑 → 𝐹 ⊆ 𝐸 )
Assertion voncmpl ( 𝜑 → 𝐹 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 voncmpl.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 voncmpl.s ⊢ 𝑆 = dom ( voln ‘ 𝑋 )
3 voncmpl.e ⊢ ( 𝜑 → 𝐸 ∈ dom ( voln ‘ 𝑋 ) )
4 voncmpl.z ⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐸 ) = 0 )
5 voncmpl.f ⊢ ( 𝜑 → 𝐹 ⊆ 𝐸 )
6 1 ovnome ⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) ∈ OutMeas )
7 eqid ⊢ ∪ dom ( voln* ‘ 𝑋 ) = ∪ dom ( voln* ‘ 𝑋 )
8 1 dmvon ⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
9 eqid ⊢ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) = ( CaraGen ‘ ( voln* ‘ 𝑋 ) )
10 9 caragenss ⊢ ( ( voln* ‘ 𝑋 ) ∈ OutMeas → ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ⊆ dom ( voln* ‘ 𝑋 ) )
11 6 10 syl ⊢ ( 𝜑 → ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ⊆ dom ( voln* ‘ 𝑋 ) )
12 8 11 eqsstrd ⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) ⊆ dom ( voln* ‘ 𝑋 ) )
13 12 3 sseldd ⊢ ( 𝜑 → 𝐸 ∈ dom ( voln* ‘ 𝑋 ) )
14 elssuni ⊢ ( 𝐸 ∈ dom ( voln* ‘ 𝑋 ) → 𝐸 ⊆ ∪ dom ( voln* ‘ 𝑋 ) )
15 13 14 syl ⊢ ( 𝜑 → 𝐸 ⊆ ∪ dom ( voln* ‘ 𝑋 ) )
16 5 15 sstrd ⊢ ( 𝜑 → 𝐹 ⊆ ∪ dom ( voln* ‘ 𝑋 ) )
17 4 eqcomd ⊢ ( 𝜑 → 0 = ( ( voln ‘ 𝑋 ) ‘ 𝐸 ) )
18 1 vonval ⊢ ( 𝜑 → ( voln ‘ 𝑋 ) = ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) )
19 18 fveq1d ⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐸 ) = ( ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) ‘ 𝐸 ) )
20 17 19 eqtrd ⊢ ( 𝜑 → 0 = ( ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) ‘ 𝐸 ) )
21 2 a1i ⊢ ( 𝜑 → 𝑆 = dom ( voln ‘ 𝑋 ) )
22 21 8 eqtr2d ⊢ ( 𝜑 → ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) = 𝑆 )
23 22 reseq2d ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) = ( ( voln* ‘ 𝑋 ) ↾ 𝑆 ) )
24 23 fveq1d ⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ↾ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) ) ‘ 𝐸 ) = ( ( ( voln* ‘ 𝑋 ) ↾ 𝑆 ) ‘ 𝐸 ) )
25 3 2 eleqtrrdi ⊢ ( 𝜑 → 𝐸 ∈ 𝑆 )
26 fvres ⊢ ( 𝐸 ∈ 𝑆 → ( ( ( voln* ‘ 𝑋 ) ↾ 𝑆 ) ‘ 𝐸 ) = ( ( voln* ‘ 𝑋 ) ‘ 𝐸 ) )
27 25 26 syl ⊢ ( 𝜑 → ( ( ( voln* ‘ 𝑋 ) ↾ 𝑆 ) ‘ 𝐸 ) = ( ( voln* ‘ 𝑋 ) ‘ 𝐸 ) )
28 20 24 27 3eqtrrd ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐸 ) = 0 )
29 6 7 15 28 5 omess0 ⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐹 ) = 0 )
30 6 7 16 29 9 caragencmpl ⊢ ( 𝜑 → 𝐹 ∈ ( CaraGen ‘ ( voln* ‘ 𝑋 ) ) )
31 30 22 eleqtrd ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )