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 ∈ 𝒫 O M ⁡ 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 ∈ 𝒫 O M ⁡ e ∩ a + 𝑒 M ⁡ e ∖ a = M ⁡ e
4 3 eleq2d ⊢ φ → A ∈ toCaraSiga ⁡ M ↔ A ∈ a ∈ 𝒫 O | ∀ e ∈ 𝒫 O M ⁡ 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 ∈ 𝒫 O M ⁡ e ∩ a + 𝑒 M ⁡ e ∖ a = M ⁡ e ↔ ∀ e ∈ 𝒫 O M ⁡ e ∩ A + 𝑒 M ⁡ e ∖ A = M ⁡ e
12 11 elrab ⊢ A ∈ a ∈ 𝒫 O | ∀ e ∈ 𝒫 O M ⁡ e ∩ a + 𝑒 M ⁡ e ∖ a = M ⁡ e ↔ A ∈ 𝒫 O ∧ ∀ e ∈ 𝒫 O M ⁡ 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 ∈ 𝒫 O M ⁡ e ∩ A + 𝑒 M ⁡ e ∖ A = M ⁡ e ↔ A ⊆ O ∧ ∀ e ∈ 𝒫 O M ⁡ e ∩ A + 𝑒 M ⁡ e ∖ A = M ⁡ e
23 12 22 syl5bb ⊢ φ → A ∈ a ∈ 𝒫 O | ∀ e ∈ 𝒫 O M ⁡ e ∩ a + 𝑒 M ⁡ e ∖ a = M ⁡ e ↔ A ⊆ O ∧ ∀ e ∈ 𝒫 O M ⁡ e ∩ A + 𝑒 M ⁡ e ∖ A = M ⁡ e
24 4 23 bitrd ⊢ φ → A ∈ toCaraSiga ⁡ M ↔ A ⊆ O ∧ ∀ e ∈ 𝒫 O M ⁡ e ∩ A + 𝑒 M ⁡ e ∖ A = M ⁡ e