Theorem caragenel

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

	Ref	Expression
Hypotheses	caragenel.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
	caragenel.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		caragenel.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		caragenel.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
3		caragenval	$$⊢O\in \mathrm{OutMeas}\to \mathrm{CaraGen}\left(O\right)=\left\{e\in 𝒫\bigcup \mathrm{dom}O|\forall a\in 𝒫\bigcup \mathrm{dom}OO\left(a\cap e\right){+}_{𝑒}O\left(a\setminus e\right)=O\left(a\right)\right\}$$
4	1 3	syl	$$⊢\phi \to \mathrm{CaraGen}\left(O\right)=\left\{e\in 𝒫\bigcup \mathrm{dom}O|\forall a\in 𝒫\bigcup \mathrm{dom}OO\left(a\cap e\right){+}_{𝑒}O\left(a\setminus e\right)=O\left(a\right)\right\}$$
5	2 4	eqtrid	$$⊢\phi \to S=\left\{e\in 𝒫\bigcup \mathrm{dom}O|\forall a\in 𝒫\bigcup \mathrm{dom}OO\left(a\cap e\right){+}_{𝑒}O\left(a\setminus e\right)=O\left(a\right)\right\}$$
6	5	eleq2d	$$⊢\phi \to \left(E\in S\leftrightarrow E\in \left\{e\in 𝒫\bigcup \mathrm{dom}O|\forall a\in 𝒫\bigcup \mathrm{dom}OO\left(a\cap e\right){+}_{𝑒}O\left(a\setminus e\right)=O\left(a\right)\right\}\right)$$
7		ineq2	$$⊢e=E\to a\cap e=a\cap E$$
8	7	fveq2d	$$⊢e=E\to O\left(a\cap e\right)=O\left(a\cap E\right)$$
9		difeq2	$$⊢e=E\to a\setminus e=a\setminus E$$
10	9	fveq2d	$$⊢e=E\to O\left(a\setminus e\right)=O\left(a\setminus E\right)$$
11	8 10	oveq12d	$$⊢e=E\to O\left(a\cap e\right){+}_{𝑒}O\left(a\setminus e\right)=O\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)$$
12	11	eqeq1d	$$⊢e=E\to \left(O\left(a\cap e\right){+}_{𝑒}O\left(a\setminus e\right)=O\left(a\right)\leftrightarrow O\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(a\right)\right)$$
13	12	ralbidv	$$⊢e=E\to \left(\forall a\in 𝒫\bigcup \mathrm{dom}OO\left(a\cap e\right){+}_{𝑒}O\left(a\setminus e\right)=O\left(a\right)\leftrightarrow \forall a\in 𝒫\bigcup \mathrm{dom}OO\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(a\right)\right)$$
14	13	elrab	$$⊢E\in \left\{e\in 𝒫\bigcup \mathrm{dom}O|\forall a\in 𝒫\bigcup \mathrm{dom}OO\left(a\cap e\right){+}_{𝑒}O\left(a\setminus e\right)=O\left(a\right)\right\}\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)$$
15	14	a1i	$$⊢\phi \to \left(E\in \left\{e\in 𝒫\bigcup \mathrm{dom}O|\forall a\in 𝒫\bigcup \mathrm{dom}OO\left(a\cap e\right){+}_{𝑒}O\left(a\setminus e\right)=O\left(a\right)\right\}\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)$$
16	6 15	bitrd	$$⊢\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)$$