Theorem caragenunidm

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

	Ref	Expression
Hypotheses	caragenunidm.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
	caragenunidm.x	$$⊢X=\bigcup \mathrm{dom}O$$
	caragenunidm.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
Assertion	caragenunidm	$$⊢\phi \to X\in S$$

Proof

Step	Hyp	Ref	Expression
1		caragenunidm.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		caragenunidm.x	$$⊢X=\bigcup \mathrm{dom}O$$
3		caragenunidm.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
4		dmexg	$$⊢O\in \mathrm{OutMeas}\to \mathrm{dom}O\in \mathrm{V}$$
5		uniexg	$$⊢\mathrm{dom}O\in \mathrm{V}\to \bigcup \mathrm{dom}O\in \mathrm{V}$$
6	1 4 5	3syl	$$⊢\phi \to \bigcup \mathrm{dom}O\in \mathrm{V}$$
7	2 6	eqeltrid	$$⊢\phi \to X\in \mathrm{V}$$
8		pwidg	$$⊢X\in \mathrm{V}\to X\in 𝒫X$$
9	7 8	syl	$$⊢\phi \to X\in 𝒫X$$
10		elpwi	$$⊢a\in 𝒫X\to a\subseteq X$$
11		df-ss	$$⊢a\subseteq X\leftrightarrow a\cap X=a$$
12	11	biimpi	$$⊢a\subseteq X\to a\cap X=a$$
13	10 12	syl	$$⊢a\in 𝒫X\to a\cap X=a$$
14	13	fveq2d	$$⊢a\in 𝒫X\to O\left(a\cap X\right)=O\left(a\right)$$
15	14	adantl	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\cap X\right)=O\left(a\right)$$
16		ssdif0	$$⊢a\subseteq X\leftrightarrow a\setminus X=\varnothing$$
17	10 16	sylib	$$⊢a\in 𝒫X\to a\setminus X=\varnothing$$
18	17	fveq2d	$$⊢a\in 𝒫X\to O\left(a\setminus X\right)=O\left(\varnothing \right)$$
19	18	adantl	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\setminus X\right)=O\left(\varnothing \right)$$
20	1	ome0	$$⊢\phi \to O\left(\varnothing \right)=0$$
21	20	adantr	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(\varnothing \right)=0$$
22	19 21	eqtrd	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\setminus X\right)=0$$
23	15 22	oveq12d	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\cap X\right){+}_{𝑒}O\left(a\setminus X\right)=O\left(a\right){+}_{𝑒}0$$
24		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
25	1	adantr	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\in \mathrm{OutMeas}$$
26	10	adantl	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to a\subseteq X$$
27	25 2 26	omecl	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\right)\in \left[0,\mathrm{+\infty }\right]$$
28	24 27	sseldi	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\right)\in {ℝ}^{*}$$
29	28	xaddid1d	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\right){+}_{𝑒}0=O\left(a\right)$$
30		eqidd	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\right)=O\left(a\right)$$
31	23 29 30	3eqtrd	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\cap X\right){+}_{𝑒}O\left(a\setminus X\right)=O\left(a\right)$$
32	1 2 3 9 31	carageneld	$$⊢\phi \to X\in S$$