Theorem caragencmpl

Description: A measure built with the Caratheodory's construction is complete. See Definition 112Df of Fremlin1 p. 19. This is Exercise 113Xa of Fremlin1 p. 21. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	caragencmpl.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
	caragencmpl.x	$$⊢X=\bigcup \mathrm{dom}O$$
	caragencmpl.e	$$⊢\phi \to E\subseteq X$$
	caragencmpl.z	$$⊢\phi \to O\left(E\right)=0$$
	caragencmpl.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
Assertion	caragencmpl	$$⊢\phi \to E\in S$$

Proof

Step	Hyp	Ref	Expression
1		caragencmpl.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		caragencmpl.x	$$⊢X=\bigcup \mathrm{dom}O$$
3		caragencmpl.e	$$⊢\phi \to E\subseteq X$$
4		caragencmpl.z	$$⊢\phi \to O\left(E\right)=0$$
5		caragencmpl.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
6	1 2	unidmex	$$⊢\phi \to X\in \mathrm{V}$$
7	6 3	ssexd	$$⊢\phi \to E\in \mathrm{V}$$
8		elpwg	$$⊢E\in \mathrm{V}\to \left(E\in 𝒫X\leftrightarrow E\subseteq X\right)$$
9	7 8	syl	$$⊢\phi \to \left(E\in 𝒫X\leftrightarrow E\subseteq X\right)$$
10	3 9	mpbird	$$⊢\phi \to E\in 𝒫X$$
11	1	adantr	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\in \mathrm{OutMeas}$$
12	3	adantr	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to E\subseteq X$$
13	4	adantr	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(E\right)=0$$
14		inss2	$$⊢a\cap E\subseteq E$$
15	14	a1i	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to a\cap E\subseteq E$$
16	11 2 12 13 15	omess0	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\cap E\right)=0$$
17	16	oveq1d	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=0{+}_{𝑒}O\left(a\setminus E\right)$$
18		difssd	$$⊢a\in 𝒫X\to a\setminus E\subseteq a$$
19		elpwi	$$⊢a\in 𝒫X\to a\subseteq X$$
20	18 19	sstrd	$$⊢a\in 𝒫X\to a\setminus E\subseteq X$$
21	20	adantl	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to a\setminus E\subseteq X$$
22	11 2 21	omexrcl	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\setminus E\right)\in {ℝ}^{*}$$
23		xaddlid	$$⊢O\left(a\setminus E\right)\in {ℝ}^{*}\to 0{+}_{𝑒}O\left(a\setminus E\right)=O\left(a\setminus E\right)$$
24	22 23	syl	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to 0{+}_{𝑒}O\left(a\setminus E\right)=O\left(a\setminus E\right)$$
25	17 24	eqtrd	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\cap E\right){+}_{𝑒}O\left(a\setminus E\right)=O\left(a\setminus E\right)$$
26	19	adantl	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to a\subseteq X$$
27	18	adantl	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to a\setminus E\subseteq a$$
28	11 2 26 27	omessle	$$⊢\left(\phi \wedge a\in 𝒫X\right)\to O\left(a\setminus E\right)\le O\left(a\right)$$
29	25 28	eqbrtrd	$$⊢\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)$$
30	1 2 5 10 29	caragenel2d	$$⊢\phi \to E\in S$$