Theorem carageneld

Description: Membership in the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	carageneld.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
	carageneld.x	$$⊢X=\bigcup \mathrm{dom}O$$
	carageneld.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
	carageneld.e	$$⊢\phi \to E\in 𝒫X$$
	carageneld.a	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(a\right)$$
Assertion	carageneld	$$⊢\phi \to E\in S$$

Proof

Step	Hyp	Ref	Expression
1		carageneld.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		carageneld.x	$$⊢X=\bigcup \mathrm{dom}O$$
3		carageneld.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
4		carageneld.e	$$⊢\phi \to E\in 𝒫X$$
5		carageneld.a	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(a\right)$$
6	2	pweqi	$$⊢𝒫X=𝒫\bigcup \mathrm{dom}O$$
7	4 6	eleqtrdi	$$⊢\phi \to E\in 𝒫\bigcup \mathrm{dom}O$$
8		simpl	$$⊢\left(\phi \wedge a\in 𝒫\bigcup \mathrm{dom}O\right)\to \phi$$
9	6	eleq2i	$$⊢a\in 𝒫X\leftrightarrow a\in 𝒫\bigcup \mathrm{dom}O$$
10	9	bicomi	$$⊢a\in 𝒫\bigcup \mathrm{dom}O\leftrightarrow a\in 𝒫X$$
11	10	biimpi	$$⊢a\in 𝒫\bigcup \mathrm{dom}O\to a\in 𝒫X$$
12	11	adantl	$$⊢\left(\phi \wedge a\in 𝒫\bigcup \mathrm{dom}O\right)\to a\in 𝒫X$$
13	8 12 5	syl2anc	$$⊢\left(\phi \wedge a\in 𝒫\bigcup \mathrm{dom}O\right)\to O\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(a\right)$$
14	13	ralrimiva	$$⊢\phi \to \forall a\in 𝒫\bigcup \mathrm{dom}OO\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(a\right)$$
15	7 14	jca	$$⊢\phi \to \left(E\in 𝒫\bigcup \mathrm{dom}O\wedge \forall a\in 𝒫\bigcup \mathrm{dom}OO\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(a\right)\right)$$
16	1 3	caragenel	$$⊢\phi \to \left(E\in S\leftrightarrow \left(E\in 𝒫\bigcup \mathrm{dom}O\wedge \forall a\in 𝒫\bigcup \mathrm{dom}OO\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(a\right)\right)\right)$$
17	15 16	mpbird	$$⊢\phi \to E\in S$$