Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Basic measure theory
Outer measures and Caratheodory's construction
caragensspw
Metamath Proof Explorer
Description: The sigma-algebra generated from an outer measure, by the Caratheodory's
construction, is a subset of the power set of the base set of the outer
measure. (Contributed by Glauco Siliprandi , 17-Aug-2020)
Ref
Expression
Hypotheses
caragensspw.o
⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
caragensspw.x
⊢ 𝑋 = ∪ dom 𝑂
caragensspw.s
⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
Assertion
caragensspw
⊢ ( 𝜑 → 𝑆 ⊆ 𝒫 𝑋 )
Proof
Step
Hyp
Ref
Expression
1
caragensspw.o
⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2
caragensspw.x
⊢ 𝑋 = ∪ dom 𝑂
3
caragensspw.s
⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
4
3
caragenss
⊢ ( 𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂 )
5
1 4
syl
⊢ ( 𝜑 → 𝑆 ⊆ dom 𝑂 )
6
pwuni
⊢ dom 𝑂 ⊆ 𝒫 ∪ dom 𝑂
7
6
a1i
⊢ ( 𝜑 → dom 𝑂 ⊆ 𝒫 ∪ dom 𝑂 )
8
5 7
sstrd
⊢ ( 𝜑 → 𝑆 ⊆ 𝒫 ∪ dom 𝑂 )
9
2
pweqi
⊢ 𝒫 𝑋 = 𝒫 ∪ dom 𝑂
10
9
eqcomi
⊢ 𝒫 ∪ dom 𝑂 = 𝒫 𝑋
11
10
a1i
⊢ ( 𝜑 → 𝒫 ∪ dom 𝑂 = 𝒫 𝑋 )
12
8 11
sseqtrd
⊢ ( 𝜑 → 𝑆 ⊆ 𝒫 𝑋 )