Metamath Proof Explorer

Theorem baselcarsg

Description: The universe set, O , is Caratheodory measurable. (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses carsgval.1 ⊢ φ → O ∈ V
carsgval.2 ⊢ φ → M : 𝒫 O ⟶ 0 +∞
baselcarsg.1 ⊢ φ → M ⁡ ∅ = 0
Assertion baselcarsg ⊢ φ → O ∈ toCaraSiga ⁡ M

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ φ → O ∈ V
2 carsgval.2 ⊢ φ → M : 𝒫 O ⟶ 0 +∞
3 baselcarsg.1 ⊢ φ → M ⁡ ∅ = 0
4 ssidd ⊢ φ → O ⊆ O
5 elpwi ⊢ e ∈ 𝒫 O → e ⊆ O
6 5 adantl ⊢ φ ∧ e ∈ 𝒫 O → e ⊆ O
7 df-ss ⊢ e ⊆ O ↔ e ∩ O = e
8 6 7 sylib ⊢ φ ∧ e ∈ 𝒫 O → e ∩ O = e
9 8 fveq2d ⊢ φ ∧ e ∈ 𝒫 O → M ⁡ e ∩ O = M ⁡ e
10 ssdif0 ⊢ e ⊆ O ↔ e ∖ O = ∅
11 6 10 sylib ⊢ φ ∧ e ∈ 𝒫 O → e ∖ O = ∅
12 11 fveq2d ⊢ φ ∧ e ∈ 𝒫 O → M ⁡ e ∖ O = M ⁡ ∅
13 3 adantr ⊢ φ ∧ e ∈ 𝒫 O → M ⁡ ∅ = 0
14 12 13 eqtrd ⊢ φ ∧ e ∈ 𝒫 O → M ⁡ e ∖ O = 0
15 9 14 oveq12d ⊢ φ ∧ e ∈ 𝒫 O → M ⁡ e ∩ O + 𝑒 M ⁡ e ∖ O = M ⁡ e + 𝑒 0
16 iccssxr ⊢ 0 +∞ ⊆ ℝ *
17 2 adantr ⊢ φ ∧ e ∈ 𝒫 O → M : 𝒫 O ⟶ 0 +∞
18 simpr ⊢ φ ∧ e ∈ 𝒫 O → e ∈ 𝒫 O
19 17 18 ffvelrnd ⊢ φ ∧ e ∈ 𝒫 O → M ⁡ e ∈ 0 +∞
20 16 19 sseldi ⊢ φ ∧ e ∈ 𝒫 O → M ⁡ e ∈ ℝ *
21 xaddid1 ⊢ M ⁡ e ∈ ℝ * → M ⁡ e + 𝑒 0 = M ⁡ e
22 20 21 syl ⊢ φ ∧ e ∈ 𝒫 O → M ⁡ e + 𝑒 0 = M ⁡ e
23 15 22 eqtrd ⊢ φ ∧ e ∈ 𝒫 O → M ⁡ e ∩ O + 𝑒 M ⁡ e ∖ O = M ⁡ e
24 23 ralrimiva ⊢ φ → ∀ e ∈ 𝒫 O M ⁡ e ∩ O + 𝑒 M ⁡ e ∖ O = M ⁡ e
25 4 24 jca ⊢ φ → O ⊆ O ∧ ∀ e ∈ 𝒫 O M ⁡ e ∩ O + 𝑒 M ⁡ e ∖ O = M ⁡ e
26 1 2 elcarsg ⊢ φ → O ∈ toCaraSiga ⁡ M ↔ O ⊆ O ∧ ∀ e ∈ 𝒫 O M ⁡ e ∩ O + 𝑒 M ⁡ e ∖ O = M ⁡ e
27 25 26 mpbird ⊢ φ → O ∈ toCaraSiga ⁡ M