Theorem caragenuni

Description: The base set of the sigma-algebra generated by the Caratheodory's construction is the whole base set of the original outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	caragenuni.o	|- ( ph -> O e. OutMeas )
	caragenuni.s	|- S = ( CaraGen ` O )
Assertion	caragenuni	|- ( ph -> U. S = U. dom O )

Proof

Step	Hyp	Ref	Expression
1		caragenuni.o	|- ( ph -> O e. OutMeas )
2		caragenuni.s	|- S = ( CaraGen ` O )
3	2	caragenss	|- ( O e. OutMeas -> S C_ dom O )
4	1 3	syl	|- ( ph -> S C_ dom O )
5	4	unissd	|- ( ph -> U. S C_ U. dom O )
6		eqid	|- U. dom O = U. dom O
7	1 6 2	caragenunidm	|- ( ph -> U. dom O e. S )
8		elssuni	|- ( U. dom O e. S -> U. dom O C_ U. S )
9	7 8	syl	|- ( ph -> U. dom O C_ U. S )
10	5 9	eqssd	|- ( ph -> U. S = U. dom O )