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 eqtrdi ⊢ φ ∧ 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 2 21 fexd ⊢ φ → M ∈ V
23 pwexg ⊢ O ∈ V → 𝒫 O ∈ V
24 rabexg ⊢ 𝒫 O ∈ V → a ∈ 𝒫 O | ∀ e ∈ 𝒫 O M ⁡ e ∩ a + 𝑒 M ⁡ e ∖ a = M ⁡ e ∈ V
25 1 23 24 3syl ⊢ φ → a ∈ 𝒫 O | ∀ e ∈ 𝒫 O M ⁡ e ∩ a + 𝑒 M ⁡ e ∖ a = M ⁡ e ∈ V
26 3 20 22 25 fvmptd2 ⊢ φ → toCaraSiga ⁡ M = a ∈ 𝒫 O | ∀ e ∈ 𝒫 O M ⁡ e ∩ a + 𝑒 M ⁡ e ∖ a = M ⁡ e