Theorem carsgcl

Description: Closure of the Caratheodory measurable sets. (Contributed by Thierry Arnoux, 17-May-2020)

	Ref	Expression
Hypotheses	carsgval.1	$$⊢\phi \to O\in V$$
	carsgval.2	$$⊢\phi \to M:𝒫O⟶\left[0,\mathrm{+\infty }\right]$$
Assertion	carsgcl	$$⊢\phi \to \mathrm{toCaraSiga}\left(M\right)\subseteq 𝒫O$$

Proof

Step	Hyp	Ref	Expression
1		carsgval.1	$$⊢\phi \to O\in V$$
2		carsgval.2	$$⊢\phi \to M:𝒫O⟶\left[0,\mathrm{+\infty }\right]$$
3	1 2	carsgval	$$⊢\phi \to \mathrm{toCaraSiga}\left(M\right)=\left\{a\in 𝒫O|\forall e\in 𝒫OM\left(e\cap a\right){+}_{𝑒}M\left(e\setminus a\right)=M\left(e\right)\right\}$$
4		ssrab2	$$⊢\left\{a\in 𝒫O|\forall e\in 𝒫OM\left(e\cap a\right){+}_{𝑒}M\left(e\setminus a\right)=M\left(e\right)\right\}\subseteq 𝒫O$$
5	3 4	eqsstrdi	$$⊢\phi \to \mathrm{toCaraSiga}\left(M\right)\subseteq 𝒫O$$