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	$$⊢\phi \to O\in \mathrm{OutMeas}$$
	caragenuni.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
Assertion	caragenuni	$$⊢\phi \to \bigcup S=\bigcup \mathrm{dom}O$$

Proof

Step	Hyp	Ref	Expression
1		caragenuni.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		caragenuni.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
3	2	caragenss	$$⊢O\in \mathrm{OutMeas}\to S\subseteq \mathrm{dom}O$$
4	1 3	syl	$$⊢\phi \to S\subseteq \mathrm{dom}O$$
5	4	unissd	$$⊢\phi \to \bigcup S\subseteq \bigcup \mathrm{dom}O$$
6		eqid	$$⊢\bigcup \mathrm{dom}O=\bigcup \mathrm{dom}O$$
7	1 6 2	caragenunidm	$$⊢\phi \to \bigcup \mathrm{dom}O\in S$$
8		elssuni	$$⊢\bigcup \mathrm{dom}O\in S\to \bigcup \mathrm{dom}O\subseteq \bigcup S$$
9	7 8	syl	$$⊢\phi \to \bigcup \mathrm{dom}O\subseteq \bigcup S$$
10	5 9	eqssd	$$⊢\phi \to \bigcup S=\bigcup \mathrm{dom}O$$