Theorem difelcarsg2

Description: The Caratheodory-measurable sets are closed under class difference. (Contributed by Thierry Arnoux, 30-May-2020)

	Ref	Expression
Hypotheses	carsgval.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
	carsgval.2	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
	difelcarsg.1	⊢ ( 𝜑 → 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )
	inelcarsg.1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑂 ∧ 𝑏 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ 𝑎 ) +𝑒 ( 𝑀 ‘ 𝑏 ) ) )
	inelcarsg.2	⊢ ( 𝜑 → 𝐵 ∈ ( toCaraSiga ‘ 𝑀 ) )
Assertion	difelcarsg2	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ∈ ( toCaraSiga ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		carsgval.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2		carsgval.2	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3		difelcarsg.1	⊢ ( 𝜑 → 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )
4		inelcarsg.1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑂 ∧ 𝑏 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ 𝑎 ) +𝑒 ( 𝑀 ‘ 𝑏 ) ) )
5		inelcarsg.2	⊢ ( 𝜑 → 𝐵 ∈ ( toCaraSiga ‘ 𝑀 ) )
6	1 2 3	elcarsgss	⊢ ( 𝜑 → 𝐴 ⊆ 𝑂 )
7		difin2	⊢ ( 𝐴 ⊆ 𝑂 → ( 𝐴 ∖ 𝐵 ) = ( ( 𝑂 ∖ 𝐵 ) ∩ 𝐴 ) )
8	6 7	syl	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) = ( ( 𝑂 ∖ 𝐵 ) ∩ 𝐴 ) )
9	1 2 5	difelcarsg	⊢ ( 𝜑 → ( 𝑂 ∖ 𝐵 ) ∈ ( toCaraSiga ‘ 𝑀 ) )
10	1 2 9 4 3	inelcarsg	⊢ ( 𝜑 → ( ( 𝑂 ∖ 𝐵 ) ∩ 𝐴 ) ∈ ( toCaraSiga ‘ 𝑀 ) )
11	8 10	eqeltrd	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ∈ ( toCaraSiga ‘ 𝑀 ) )