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 eqtrid ⊢φ→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 ffvelcdmda ⊢φ∧e∈𝒫O→M⁡e∈0+∞
16 14 15 sselid ⊢φ∧e∈𝒫O→M⁡e∈ℝ*
17 xaddlid ⊢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∈𝒫OM⁡e∩∅+𝑒M⁡e∖∅=M⁡e
21 1 2 elcarsg ⊢φ→∅∈toCaraSiga⁡M↔∅⊆O∧∀e∈𝒫OM⁡e∩∅+𝑒M⁡e∖∅=M⁡e
22 5 20 21 mpbir2and ⊢φ→∅∈toCaraSiga⁡M