difelcarsg2

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

	Ref	Expression
Hypotheses	carsgval.1	$⊢ φ \to O \in V$
	carsgval.2	$⊢ φ \to M : 𝒫 O ⟶ [0, +∞]$
	difelcarsg.1	$⊢ φ \to A \in toCaraSiga (M)$
	inelcarsg.1	$⊢ (φ \land a \in 𝒫 O \land b \in 𝒫 O) \to M (a \cup b) \leq M (a) +_{𝑒} M (b)$
	inelcarsg.2	$⊢ φ \to B \in toCaraSiga (M)$
Assertion	difelcarsg2	$⊢ φ \to A ∖ B \in toCaraSiga (M)$

Step	Hyp	Ref	Expression
1		carsgval.1	$⊢ φ \to O \in V$
2		carsgval.2	$⊢ φ \to M : 𝒫 O ⟶ [0, +∞]$
3		difelcarsg.1	$⊢ φ \to A \in toCaraSiga (M)$
4		inelcarsg.1	$⊢ (φ \land a \in 𝒫 O \land b \in 𝒫 O) \to M (a \cup b) \leq M (a) +_{𝑒} M (b)$
5		inelcarsg.2	$⊢ φ \to B \in toCaraSiga (M)$
6	1 2 3	elcarsgss	$⊢ φ \to A \subseteq O$
7		difin2	$⊢ A \subseteq O \to A ∖ B = (O ∖ B) \cap A$
8	6 7	syl	$⊢ φ \to A ∖ B = (O ∖ B) \cap A$
9	1 2 5	difelcarsg	$⊢ φ \to O ∖ B \in toCaraSiga (M)$
10	1 2 9 4 3	inelcarsg	$⊢ φ \to (O ∖ B) \cap A \in toCaraSiga (M)$
11	8 10	eqeltrd	$⊢ φ \to A ∖ B \in toCaraSiga (M)$

Metamath Proof Explorer