Theorem caragenel2d

Description: Membership in the Caratheodory's construction. Similar to carageneld , but here "less than or equal to" is used, instead of equality. This is Remark 113D of Fremlin1 p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020)

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

Proof

Step	Hyp	Ref	Expression
1		caragenel2d.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		caragenel2d.x	$$⊢X=\bigcup \mathrm{dom}O$$
3		caragenel2d.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
4		caragenel2d.e	$$⊢\phi \to E\in 𝒫X$$
5		caragenel2d.a	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)\le O\left(a\right)$$
6	1	adantr	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\in \mathrm{OutMeas}$$
7		inss1	$$⊢a\cap E\subseteq a$$
8		elpwi	$$⊢a\in 𝒫X\to a\subseteq X$$
9	7 8	sstrid	$$⊢a\in 𝒫X\to a\cap E\subseteq X$$
10	9	adantl	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to a\cap E\subseteq X$$
11	6 2 10	omexrcl	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\cap E\right)\in {ℝ}^{*}$$
12	8	ssdifssd	$$⊢a\in 𝒫X\to a\setminus E\subseteq X$$
13	12	adantl	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to a\setminus E\subseteq X$$
14	6 2 13	omexrcl	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\setminus E\right)\in {ℝ}^{*}$$
15		xaddcl	$$⊢\left(O\left(a\cap E\right)\in {ℝ}^{*}\wedge O\left(a\setminus E\right)\in {ℝ}^{*}\right)\to O\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)\in {ℝ}^{*}$$
16	11 14 15	syl2anc	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)\in {ℝ}^{*}$$
17	8	adantl	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to a\subseteq X$$
18	6 2 17	omexrcl	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\right)\in {ℝ}^{*}$$
19	6 2 17	omelesplit	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\right)\le O\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)$$
20	16 18 5 19	xrletrid	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(a\right)$$
21	1 2 3 4 20	carageneld	$$⊢\phi \to E\in S$$