Metamath Proof Explorer


Theorem caragensspw

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 ( 𝜑𝑆 ⊆ 𝒫 𝑋 )