Theorem caragenelss

Description: An element of the Caratheodory's construction is a subset of the base set of the outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		caragenelss.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		caragenelss.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
3		caragenelss.a	$$⊢\phi \to A\in S$$
4		caragenelss.x	$$⊢X=\bigcup \mathrm{dom}O$$
5	1 2	caragenel	$$⊢\phi \to \left(A\in S\leftrightarrow \left(A\in 𝒫\bigcup \mathrm{dom}O\wedge \forall x\in 𝒫\bigcup \mathrm{dom}OO\left(x\cap A\right){+}_{𝑒}O\left(x\setminus A\right)=O\left(x\right)\right)\right)$$
6	3 5	mpbid	$$⊢\phi \to \left(A\in 𝒫\bigcup \mathrm{dom}O\wedge \forall x\in 𝒫\bigcup \mathrm{dom}OO\left(x\cap A\right){+}_{𝑒}O\left(x\setminus A\right)=O\left(x\right)\right)$$
7	6	simpld	$$⊢\phi \to A\in 𝒫\bigcup \mathrm{dom}O$$
8	4	eqcomi	$$⊢\bigcup \mathrm{dom}O=X$$
9	8	pweqi	$$⊢𝒫\bigcup \mathrm{dom}O=𝒫X$$
10	9	a1i	$$⊢\phi \to 𝒫\bigcup \mathrm{dom}O=𝒫X$$
11	7 10	eleqtrd	$$⊢\phi \to A\in 𝒫X$$
12		elpwg	$$⊢A\in S\to \left(A\in 𝒫X\leftrightarrow A\subseteq X\right)$$
13	3 12	syl	$$⊢\phi \to \left(A\in 𝒫X\leftrightarrow A\subseteq X\right)$$
14	11 13	mpbid	$$⊢\phi \to A\subseteq X$$