Theorem caragenss

Description: The sigma-algebra generated from an outer measure, by the Caratheodory's construction, is a subset of the domain of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	caragenss.1	|- S = ( CaraGen ` O )
Assertion	caragenss	|- ( O e. OutMeas -> S C_ dom O )

Proof

Step	Hyp	Ref	Expression
1		caragenss.1	|- S = ( CaraGen ` O )
2		ssrab2	|- { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } C_ ~P U. dom O
3	2	a1i	|- ( O e. OutMeas -> { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } C_ ~P U. dom O )
4	1	a1i	|- ( O e. OutMeas -> S = ( CaraGen ` O ) )
5		caragenval	|- ( O e. OutMeas -> ( CaraGen ` O ) = { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } )
6	4 5	eqtrd	|- ( O e. OutMeas -> S = { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } )
7		omedm	|- ( O e. OutMeas -> dom O = ~P U. dom O )
8	6 7	sseq12d	|- ( O e. OutMeas -> ( S C_ dom O <-> { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } C_ ~P U. dom O ) )
9	3 8	mpbird	|- ( O e. OutMeas -> S C_ dom O )