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	|- ( ph -> O e. OutMeas )
	caragensspw.x	|- X = U. dom O
	caragensspw.s	|- S = ( CaraGen ` O )
Assertion	caragensspw	|- ( ph -> S C_ ~P X )

Proof

Step	Hyp	Ref	Expression
1		caragensspw.o	|- ( ph -> O e. OutMeas )
2		caragensspw.x	|- X = U. dom O
3		caragensspw.s	|- S = ( CaraGen ` O )
4	3	caragenss	|- ( O e. OutMeas -> S C_ dom O )
5	1 4	syl	|- ( ph -> S C_ dom O )
6		pwuni	|- dom O C_ ~P U. dom O
7	6	a1i	|- ( ph -> dom O C_ ~P U. dom O )
8	5 7	sstrd	|- ( ph -> S C_ ~P U. dom O )
9	2	pweqi	|- ~P X = ~P U. dom O
10	9	eqcomi	|- ~P U. dom O = ~P X
11	10	a1i	|- ( ph -> ~P U. dom O = ~P X )
12	8 11	sseqtrd	|- ( ph -> S C_ ~P X )