unelcarsg

Description: The Caratheodory-measurable sets are closed under pairwise unions. (Contributed by Thierry Arnoux, 21-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	unelcarsg	$⊢ φ \to A \cup 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		dfss4	$⊢ A \subseteq O \leftrightarrow O ∖ (O ∖ A) = A$
8	6 7	sylib	$⊢ φ \to O ∖ (O ∖ A) = A$
9	1 2 5	elcarsgss	$⊢ φ \to B \subseteq O$
10		dfss4	$⊢ B \subseteq O \leftrightarrow O ∖ (O ∖ B) = B$
11	9 10	sylib	$⊢ φ \to O ∖ (O ∖ B) = B$
12	8 11	uneq12d	$⊢ φ \to (O ∖ (O ∖ A)) \cup (O ∖ (O ∖ B)) = A \cup B$
13		difindi	$⊢ O ∖ ((O ∖ A) \cap (O ∖ B)) = (O ∖ (O ∖ A)) \cup (O ∖ (O ∖ B))$
14	1 2 3	difelcarsg	$⊢ φ \to O ∖ A \in toCaraSiga (M)$
15	1 2 5	difelcarsg	$⊢ φ \to O ∖ B \in toCaraSiga (M)$
16	1 2 14 4 15	inelcarsg	$⊢ φ \to (O ∖ A) \cap (O ∖ B) \in toCaraSiga (M)$
17	1 2 16	difelcarsg	$⊢ φ \to O ∖ ((O ∖ A) \cap (O ∖ B)) \in toCaraSiga (M)$
18	13 17	eqeltrrid	$⊢ φ \to (O ∖ (O ∖ A)) \cup (O ∖ (O ∖ B)) \in toCaraSiga (M)$
19	12 18	eqeltrrd	$⊢ φ \to A \cup B \in toCaraSiga (M)$

Metamath Proof Explorer