Metamath Proof Explorer

Theorem elcarsg

Description: Property of being a Caratheodory measurable set. (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses carsgval.1 ⊢φ→O∈V
carsgval.2 ⊢φ→M:𝒫O⟶0+∞
Assertion elcarsg ⊢φ→A∈toCaraSiga⁡M↔A⊆O∧∀e∈𝒫OM⁡e∩A+𝑒M⁡e∖A=M⁡e

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢φ→O∈V
2 carsgval.2 ⊢φ→M:𝒫O⟶0+∞
3 1 2 carsgval ⊢φ→toCaraSiga⁡M=a∈𝒫O|∀e∈𝒫OM⁡e∩a+𝑒M⁡e∖a=M⁡e
4 3 eleq2d ⊢φ→A∈toCaraSiga⁡M↔A∈a∈𝒫O|∀e∈𝒫OM⁡e∩a+𝑒M⁡e∖a=M⁡e
5 ineq2 ⊢a=A→e∩a=e∩A
6 5 fveq2d ⊢a=A→M⁡e∩a=M⁡e∩A
7 difeq2 ⊢a=A→e∖a=e∖A
8 7 fveq2d ⊢a=A→M⁡e∖a=M⁡e∖A
9 6 8 oveq12d ⊢a=A→M⁡e∩a+𝑒M⁡e∖a=M⁡e∩A+𝑒M⁡e∖A
10 9 eqeq1d ⊢a=A→M⁡e∩a+𝑒M⁡e∖a=M⁡e↔M⁡e∩A+𝑒M⁡e∖A=M⁡e
11 10 ralbidv ⊢a=A→∀e∈𝒫OM⁡e∩a+𝑒M⁡e∖a=M⁡e↔∀e∈𝒫OM⁡e∩A+𝑒M⁡e∖A=M⁡e
12 11 elrab ⊢A∈a∈𝒫O|∀e∈𝒫OM⁡e∩a+𝑒M⁡e∖a=M⁡e↔A∈𝒫O∧∀e∈𝒫OM⁡e∩A+𝑒M⁡e∖A=M⁡e
13 elex ⊢A∈𝒫O→A∈V
14 13 a1i ⊢φ→A∈𝒫O→A∈V
15 1 adantr ⊢φ∧A⊆O→O∈V
16 simpr ⊢φ∧A⊆O→A⊆O
17 15 16 ssexd ⊢φ∧A⊆O→A∈V
18 17 ex ⊢φ→A⊆O→A∈V
19 elpwg ⊢A∈V→A∈𝒫O↔A⊆O
20 19 a1i ⊢φ→A∈V→A∈𝒫O↔A⊆O
21 14 18 20 pm5.21ndd ⊢φ→A∈𝒫O↔A⊆O
22 21 anbi1d ⊢φ→A∈𝒫O∧∀e∈𝒫OM⁡e∩A+𝑒M⁡e∖A=M⁡e↔A⊆O∧∀e∈𝒫OM⁡e∩A+𝑒M⁡e∖A=M⁡e
23 12 22 bitrid ⊢φ→A∈a∈𝒫O|∀e∈𝒫OM⁡e∩a+𝑒M⁡e∖a=M⁡e↔A⊆O∧∀e∈𝒫OM⁡e∩A+𝑒M⁡e∖A=M⁡e
24 4 23 bitrd ⊢φ→A∈toCaraSiga⁡M↔A⊆O∧∀e∈𝒫OM⁡e∩A+𝑒M⁡e∖A=M⁡e