Metamath Proof Explorer

Theorem unelcarsg

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

Ref Expression
Hypotheses carsgval.1 ⊢ φ → O ∈ V
carsgval.2 ⊢ φ → M : 𝒫 O ⟶ 0 +∞
difelcarsg.1 ⊢ φ → A ∈ toCaraSiga ⁡ M
inelcarsg.1 ⊢ φ ∧ a ∈ 𝒫 O ∧ b ∈ 𝒫 O → M ⁡ a ∪ b ≤ M ⁡ a + 𝑒 M ⁡ b
inelcarsg.2 ⊢ φ → B ∈ toCaraSiga ⁡ M
Assertion unelcarsg ⊢ φ → A ∪ B ∈ toCaraSiga ⁡ M

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ φ → O ∈ V
2 carsgval.2 ⊢ φ → M : 𝒫 O ⟶ 0 +∞
3 difelcarsg.1 ⊢ φ → A ∈ toCaraSiga ⁡ M
4 inelcarsg.1 ⊢ φ ∧ a ∈ 𝒫 O ∧ b ∈ 𝒫 O → M ⁡ a ∪ b ≤ M ⁡ a + 𝑒 M ⁡ b
5 inelcarsg.2 ⊢ φ → B ∈ toCaraSiga ⁡ M
6 1 2 3 elcarsgss ⊢ φ → A ⊆ O
7 dfss4 ⊢ A ⊆ O ↔ O ∖ O ∖ A = A
8 6 7 sylib ⊢ φ → O ∖ O ∖ A = A
9 1 2 5 elcarsgss ⊢ φ → B ⊆ O
10 dfss4 ⊢ B ⊆ O ↔ O ∖ O ∖ B = B
11 9 10 sylib ⊢ φ → O ∖ O ∖ B = B
12 8 11 uneq12d ⊢ φ → O ∖ O ∖ A ∪ O ∖ O ∖ B = A ∪ B
13 difindi ⊢ O ∖ O ∖ A ∩ O ∖ B = O ∖ O ∖ A ∪ O ∖ O ∖ B
14 1 2 3 difelcarsg ⊢ φ → O ∖ A ∈ toCaraSiga ⁡ M
15 1 2 5 difelcarsg ⊢ φ → O ∖ B ∈ toCaraSiga ⁡ M
16 1 2 14 4 15 inelcarsg ⊢ φ → O ∖ A ∩ O ∖ B ∈ toCaraSiga ⁡ M
17 1 2 16 difelcarsg ⊢ φ → O ∖ O ∖ A ∩ O ∖ B ∈ toCaraSiga ⁡ M
18 13 17 eqeltrrid ⊢ φ → O ∖ O ∖ A ∪ O ∖ O ∖ B ∈ toCaraSiga ⁡ M
19 12 18 eqeltrrd ⊢ φ → A ∪ B ∈ toCaraSiga ⁡ M