Metamath Proof Explorer

Theorem carsgval

Description: Value of the Caratheodory sigma-Algebra construction function. (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses carsgval.1 ⊢ φ → O ∈ V
carsgval.2 ⊢ φ → M : 𝒫 O ⟶ 0 +∞
Assertion carsgval ⊢ φ → 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 df-carsg ⊢ toCaraSiga = m ∈ V ⟼ a ∈ 𝒫 ⋃ dom ⁡ m | ∀ e ∈ 𝒫 ⋃ dom ⁡ m m ⁡ e ∩ a + 𝑒 m ⁡ e ∖ a = m ⁡ e
4 simpr ⊢ φ ∧ m = M → m = M
5 4 dmeqd ⊢ φ ∧ m = M → dom ⁡ m = dom ⁡ M
6 2 fdmd ⊢ φ → dom ⁡ M = 𝒫 O
7 6 adantr ⊢ φ ∧ m = M → dom ⁡ M = 𝒫 O
8 5 7 eqtrd ⊢ φ ∧ m = M → dom ⁡ m = 𝒫 O
9 8 unieqd ⊢ φ ∧ m = M → ⋃ dom ⁡ m = ⋃ 𝒫 O
10 unipw ⊢ ⋃ 𝒫 O = O
11 9 10 syl6eq ⊢ φ ∧ m = M → ⋃ dom ⁡ m = O
12 11 pweqd ⊢ φ ∧ m = M → 𝒫 ⋃ dom ⁡ m = 𝒫 O
13 fveq1 ⊢ m = M → m ⁡ e ∩ a = M ⁡ e ∩ a
14 fveq1 ⊢ m = M → m ⁡ e ∖ a = M ⁡ e ∖ a
15 13 14 oveq12d ⊢ m = M → m ⁡ e ∩ a + 𝑒 m ⁡ e ∖ a = M ⁡ e ∩ a + 𝑒 M ⁡ e ∖ a
16 fveq1 ⊢ m = M → m ⁡ e = M ⁡ e
17 15 16 eqeq12d ⊢ m = M → m ⁡ e ∩ a + 𝑒 m ⁡ e ∖ a = m ⁡ e ↔ M ⁡ e ∩ a + 𝑒 M ⁡ e ∖ a = M ⁡ e
18 17 adantl ⊢ φ ∧ m = M → m ⁡ e ∩ a + 𝑒 m ⁡ e ∖ a = m ⁡ e ↔ M ⁡ e ∩ a + 𝑒 M ⁡ e ∖ a = M ⁡ e
19 12 18 raleqbidv ⊢ φ ∧ m = M → ∀ e ∈ 𝒫 ⋃ dom ⁡ m m ⁡ e ∩ a + 𝑒 m ⁡ e ∖ a = m ⁡ e ↔ ∀ e ∈ 𝒫 O M ⁡ e ∩ a + 𝑒 M ⁡ e ∖ a = M ⁡ e
20 12 19 rabeqbidv ⊢ φ ∧ m = M → a ∈ 𝒫 ⋃ dom ⁡ m | ∀ e ∈ 𝒫 ⋃ dom ⁡ m m ⁡ e ∩ a + 𝑒 m ⁡ e ∖ a = m ⁡ e = a ∈ 𝒫 O | ∀ e ∈ 𝒫 O M ⁡ e ∩ a + 𝑒 M ⁡ e ∖ a = M ⁡ e
21 1 pwexd ⊢ φ → 𝒫 O ∈ V
22 fex ⊢ M : 𝒫 O ⟶ 0 +∞ ∧ 𝒫 O ∈ V → M ∈ V
23 2 21 22 syl2anc ⊢ φ → M ∈ V
24 pwexg ⊢ O ∈ V → 𝒫 O ∈ V
25 rabexg ⊢ 𝒫 O ∈ V → a ∈ 𝒫 O | ∀ e ∈ 𝒫 O M ⁡ e ∩ a + 𝑒 M ⁡ e ∖ a = M ⁡ e ∈ V
26 1 24 25 3syl ⊢ φ → a ∈ 𝒫 O | ∀ e ∈ 𝒫 O M ⁡ e ∩ a + 𝑒 M ⁡ e ∖ a = M ⁡ e ∈ V
27 3 20 23 26 fvmptd2 ⊢ φ → toCaraSiga ⁡ M = a ∈ 𝒫 O | ∀ e ∈ 𝒫 O M ⁡ e ∩ a + 𝑒 M ⁡ e ∖ a = M ⁡ e