Theorem omelesplit

Description: The outer measure of a set A is less than or equal to the extended addition of the outer measures of the decomposition induced on A by any E . Step (a) in the proof of Caratheodory's Method, Theorem 113C of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	omelesplit.1	$$⊢\phi \to O\in \mathrm{OutMeas}$$
	omelesplit.2	$$⊢X=\bigcup \mathrm{dom}O$$
	omelesplit.3	$$⊢\phi \to A\subseteq X$$
Assertion	omelesplit	$$⊢\phi \to O\left(A\right)\le O\left(A\cap E\right){+}_{𝑒}O\left(A\setminus E\right)$$

Proof

Step	Hyp	Ref	Expression
1		omelesplit.1	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		omelesplit.2	$$⊢X=\bigcup \mathrm{dom}O$$
3		omelesplit.3	$$⊢\phi \to A\subseteq X$$
4		inundif	$$⊢\left(A\cap E\right)\cup \left(A\setminus E\right)=A$$
5	4	eqcomi	$$⊢A=\left(A\cap E\right)\cup \left(A\setminus E\right)$$
6	5	a1i	$$⊢\phi \to A=\left(A\cap E\right)\cup \left(A\setminus E\right)$$
7	6	fveq2d	$$⊢\phi \to O\left(A\right)=O\left(\left(A\cap E\right)\cup \left(A\setminus E\right)\right)$$
8		ssinss1	$$⊢A\subseteq X\to A\cap E\subseteq X$$
9	3 8	syl	$$⊢\phi \to A\cap E\subseteq X$$
10	3	ssdifssd	$$⊢\phi \to A\setminus E\subseteq X$$
11	1 2 9 10	omeunle	$$⊢\phi \to O\left(\left(A\cap E\right)\cup \left(A\setminus E\right)\right)\le O\left(A\cap E\right){+}_{𝑒}O\left(A\setminus E\right)$$
12	7 11	eqbrtrd	$$⊢\phi \to O\left(A\right)\le O\left(A\cap E\right){+}_{𝑒}O\left(A\setminus E\right)$$