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	bilanri	$$⊢\left(\phi \wedge a\in 𝒫\bigcup \mathrm{dom}O\right)\to a\in 𝒫X$$
11	8 10 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)$$
12	11	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)$$
13	7 12	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)$$
14	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)$$
15	13 14	mpbird	$$⊢\phi \to E\in S$$