Theorem carsgcl

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

	Ref	Expression
Hypotheses	carsgval.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
	carsgval.2	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
Assertion	carsgcl	⊢ ( 𝜑 → ( toCaraSiga ‘ 𝑀 ) ⊆ 𝒫 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		carsgval.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2		carsgval.2	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3	1 2	carsgval	⊢ ( 𝜑 → ( toCaraSiga ‘ 𝑀 ) = { 𝑎 ∈ 𝒫 𝑂 ∣ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) } )
4		ssrab2	⊢ { 𝑎 ∈ 𝒫 𝑂 ∣ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ 𝑎 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ 𝑎 ) ) ) = ( 𝑀 ‘ 𝑒 ) } ⊆ 𝒫 𝑂
5	3 4	eqsstrdi	⊢ ( 𝜑 → ( toCaraSiga ‘ 𝑀 ) ⊆ 𝒫 𝑂 )