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 φ O OutMeas
caragensspw.x X = dom O
caragensspw.s S = CaraGen O
Assertion caragensspw φ S 𝒫 X

Proof

Step Hyp Ref Expression
1 caragensspw.o φ O OutMeas
2 caragensspw.x X = dom O
3 caragensspw.s S = CaraGen O
4 3 caragenss O OutMeas S dom O
5 1 4 syl φ S dom O
6 pwuni dom O 𝒫 dom O
7 6 a1i φ dom O 𝒫 dom O
8 5 7 sstrd φ S 𝒫 dom O
9 2 pweqi 𝒫 X = 𝒫 dom O
10 9 eqcomi 𝒫 dom O = 𝒫 X
11 10 a1i φ 𝒫 dom O = 𝒫 X
12 8 11 sseqtrd φ S 𝒫 X