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

Proof

Step	Hyp	Ref	Expression
1		caragensspw.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		caragensspw.x	$$⊢X=\bigcup \mathrm{dom}O$$
3		caragensspw.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
4	3	caragenss	$$⊢O\in \mathrm{OutMeas}\to S\subseteq \mathrm{dom}O$$
5	1 4	syl	$$⊢\phi \to S\subseteq \mathrm{dom}O$$
6		pwuni	$$⊢\mathrm{dom}O\subseteq 𝒫\bigcup \mathrm{dom}O$$
7	6	a1i	$$⊢\phi \to \mathrm{dom}O\subseteq 𝒫\bigcup \mathrm{dom}O$$
8	5 7	sstrd	$$⊢\phi \to S\subseteq 𝒫\bigcup \mathrm{dom}O$$
9	2	pweqi	$$⊢𝒫X=𝒫\bigcup \mathrm{dom}O$$
10	9	eqcomi	$$⊢𝒫\bigcup \mathrm{dom}O=𝒫X$$
11	10	a1i	$$⊢\phi \to 𝒫\bigcup \mathrm{dom}O=𝒫X$$
12	8 11	sseqtrd	$$⊢\phi \to S\subseteq 𝒫X$$