Theorem unelcarsg

Description: The Caratheodory-measurable sets are closed under pairwise unions. (Contributed by Thierry Arnoux, 21-May-2020)

	Ref	Expression
Hypotheses	carsgval.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
	carsgval.2	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
	difelcarsg.1	⊢ ( 𝜑 → 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )
	inelcarsg.1	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝒫 𝑂 ∧ 𝑏 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑎 ∪ 𝑏 ) ) ≤ ( ( 𝑀 ‘ 𝑎 ) +𝑒 ( 𝑀 ‘ 𝑏 ) ) )
	inelcarsg.2	⊢ ( 𝜑 → 𝐵 ∈ ( toCaraSiga ‘ 𝑀 ) )
Assertion	unelcarsg	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ ( 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		dfss4	⊢ ( 𝐴 ⊆ 𝑂 ↔ ( 𝑂 ∖ ( 𝑂 ∖ 𝐴 ) ) = 𝐴 )
8	6 7	sylib	⊢ ( 𝜑 → ( 𝑂 ∖ ( 𝑂 ∖ 𝐴 ) ) = 𝐴 )
9	1 2 5	elcarsgss	⊢ ( 𝜑 → 𝐵 ⊆ 𝑂 )
10		dfss4	⊢ ( 𝐵 ⊆ 𝑂 ↔ ( 𝑂 ∖ ( 𝑂 ∖ 𝐵 ) ) = 𝐵 )
11	9 10	sylib	⊢ ( 𝜑 → ( 𝑂 ∖ ( 𝑂 ∖ 𝐵 ) ) = 𝐵 )
12	8 11	uneq12d	⊢ ( 𝜑 → ( ( 𝑂 ∖ ( 𝑂 ∖ 𝐴 ) ) ∪ ( 𝑂 ∖ ( 𝑂 ∖ 𝐵 ) ) ) = ( 𝐴 ∪ 𝐵 ) )
13		difindi	⊢ ( 𝑂 ∖ ( ( 𝑂 ∖ 𝐴 ) ∩ ( 𝑂 ∖ 𝐵 ) ) ) = ( ( 𝑂 ∖ ( 𝑂 ∖ 𝐴 ) ) ∪ ( 𝑂 ∖ ( 𝑂 ∖ 𝐵 ) ) )
14	1 2 3	difelcarsg	⊢ ( 𝜑 → ( 𝑂 ∖ 𝐴 ) ∈ ( toCaraSiga ‘ 𝑀 ) )
15	1 2 5	difelcarsg	⊢ ( 𝜑 → ( 𝑂 ∖ 𝐵 ) ∈ ( toCaraSiga ‘ 𝑀 ) )
16	1 2 14 4 15	inelcarsg	⊢ ( 𝜑 → ( ( 𝑂 ∖ 𝐴 ) ∩ ( 𝑂 ∖ 𝐵 ) ) ∈ ( toCaraSiga ‘ 𝑀 ) )
17	1 2 16	difelcarsg	⊢ ( 𝜑 → ( 𝑂 ∖ ( ( 𝑂 ∖ 𝐴 ) ∩ ( 𝑂 ∖ 𝐵 ) ) ) ∈ ( toCaraSiga ‘ 𝑀 ) )
18	13 17	eqeltrrid	⊢ ( 𝜑 → ( ( 𝑂 ∖ ( 𝑂 ∖ 𝐴 ) ) ∪ ( 𝑂 ∖ ( 𝑂 ∖ 𝐵 ) ) ) ∈ ( toCaraSiga ‘ 𝑀 ) )
19	12 18	eqeltrrd	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ ( toCaraSiga ‘ 𝑀 ) )