Metamath Proof Explorer

Theorem caragenval

Description: The sigma-algebra generated by an outer measure. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion caragenval ⊢ O ∈ OutMeas → CaraGen ⁡ O = e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a

Proof

Step Hyp Ref Expression
1 id ⊢ O ∈ OutMeas → O ∈ OutMeas
2 dmexg ⊢ O ∈ OutMeas → dom ⁡ O ∈ V
3 2 uniexd ⊢ O ∈ OutMeas → ⋃ dom ⁡ O ∈ V
4 3 pwexd ⊢ O ∈ OutMeas → 𝒫 ⋃ dom ⁡ O ∈ V
5 rabexg ⊢ 𝒫 ⋃ dom ⁡ O ∈ V → e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a ∈ V
6 4 5 syl ⊢ O ∈ OutMeas → e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a ∈ V
7 dmeq ⊢ o = O → dom ⁡ o = dom ⁡ O
8 7 unieqd ⊢ o = O → ⋃ dom ⁡ o = ⋃ dom ⁡ O
9 8 pweqd ⊢ o = O → 𝒫 ⋃ dom ⁡ o = 𝒫 ⋃ dom ⁡ O
10 9 raleqdv ⊢ o = O → ∀ a ∈ 𝒫 ⋃ dom ⁡ o o ⁡ a ∩ e + 𝑒 o ⁡ a ∖ e = o ⁡ a ↔ ∀ a ∈ 𝒫 ⋃ dom ⁡ O o ⁡ a ∩ e + 𝑒 o ⁡ a ∖ e = o ⁡ a
11 fveq1 ⊢ o = O → o ⁡ a ∩ e = O ⁡ a ∩ e
12 fveq1 ⊢ o = O → o ⁡ a ∖ e = O ⁡ a ∖ e
13 11 12 oveq12d ⊢ o = O → o ⁡ a ∩ e + 𝑒 o ⁡ a ∖ e = O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e
14 fveq1 ⊢ o = O → o ⁡ a = O ⁡ a
15 13 14 eqeq12d ⊢ o = O → o ⁡ a ∩ e + 𝑒 o ⁡ a ∖ e = o ⁡ a ↔ O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a
16 15 ralbidv ⊢ o = O → ∀ a ∈ 𝒫 ⋃ dom ⁡ O o ⁡ a ∩ e + 𝑒 o ⁡ a ∖ e = o ⁡ a ↔ ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a
17 10 16 bitrd ⊢ o = O → ∀ a ∈ 𝒫 ⋃ dom ⁡ o o ⁡ a ∩ e + 𝑒 o ⁡ a ∖ e = o ⁡ a ↔ ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a
18 9 17 rabeqbidv ⊢ o = O → e ∈ 𝒫 ⋃ dom ⁡ o | ∀ a ∈ 𝒫 ⋃ dom ⁡ o o ⁡ a ∩ e + 𝑒 o ⁡ a ∖ e = o ⁡ a = e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a
19 df-caragen ⊢ CaraGen = o ∈ OutMeas ⟼ e ∈ 𝒫 ⋃ dom ⁡ o | ∀ a ∈ 𝒫 ⋃ dom ⁡ o o ⁡ a ∩ e + 𝑒 o ⁡ a ∖ e = o ⁡ a
20 18 19 fvmptg ⊢ O ∈ OutMeas ∧ e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a ∈ V → CaraGen ⁡ O = e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a
21 1 6 20 syl2anc ⊢ O ∈ OutMeas → CaraGen ⁡ O = e ∈ 𝒫 ⋃ dom ⁡ O | ∀ a ∈ 𝒫 ⋃ dom ⁡ O O ⁡ a ∩ e + 𝑒 O ⁡ a ∖ e = O ⁡ a