Metamath Proof Explorer

Theorem 0elcarsg

Description: The empty set is Caratheodory measurable. (Contributed by Thierry Arnoux, 30-May-2020)

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

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ φ → O ∈ V
2 carsgval.2 ⊢ φ → M : 𝒫 O ⟶ 0 +∞
3 baselcarsg.1 ⊢ φ → M ⁡ ∅ = 0
4 0ss ⊢ ∅ ⊆ O
5 4 a1i ⊢ φ → ∅ ⊆ O
6 in0 ⊢ e ∩ ∅ = ∅
7 6 fveq2i ⊢ M ⁡ e ∩ ∅ = M ⁡ ∅
8 7 3 syl5eq ⊢ φ → M ⁡ e ∩ ∅ = 0
9 dif0 ⊢ e ∖ ∅ = e
10 9 fveq2i ⊢ M ⁡ e ∖ ∅ = M ⁡ e
11 10 a1i ⊢ φ → M ⁡ e ∖ ∅ = M ⁡ e
12 8 11 oveq12d ⊢ φ → M ⁡ e ∩ ∅ + 𝑒 M ⁡ e ∖ ∅ = 0 + 𝑒 M ⁡ e
13 12 adantr ⊢ φ ∧ e ∈ 𝒫 O → M ⁡ e ∩ ∅ + 𝑒 M ⁡ e ∖ ∅ = 0 + 𝑒 M ⁡ e
14 iccssxr ⊢ 0 +∞ ⊆ ℝ *
15 2 ffvelrnda ⊢ φ ∧ e ∈ 𝒫 O → M ⁡ e ∈ 0 +∞
16 14 15 sselid ⊢ φ ∧ e ∈ 𝒫 O → M ⁡ e ∈ ℝ *
17 xaddid2 ⊢ M ⁡ e ∈ ℝ * → 0 + 𝑒 M ⁡ e = M ⁡ e
18 16 17 syl ⊢ φ ∧ e ∈ 𝒫 O → 0 + 𝑒 M ⁡ e = M ⁡ e
19 13 18 eqtrd ⊢ φ ∧ e ∈ 𝒫 O → M ⁡ e ∩ ∅ + 𝑒 M ⁡ e ∖ ∅ = M ⁡ e
20 19 ralrimiva ⊢ φ → ∀ e ∈ 𝒫 O M ⁡ e ∩ ∅ + 𝑒 M ⁡ e ∖ ∅ = M ⁡ e
21 1 2 elcarsg ⊢ φ → ∅ ∈ toCaraSiga ⁡ M ↔ ∅ ⊆ O ∧ ∀ e ∈ 𝒫 O M ⁡ e ∩ ∅ + 𝑒 M ⁡ e ∖ ∅ = M ⁡ e
22 5 20 21 mpbir2and ⊢ φ → ∅ ∈ toCaraSiga ⁡ M