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⁡OO⁡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⁡OO⁡a∩e+𝑒O⁡a∖e=O⁡a∈V
6 4 5 syl ⊢O∈OutMeas→e∈𝒫⋃dom⁡O|∀a∈𝒫⋃dom⁡OO⁡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⁡oo⁡a∩e+𝑒o⁡a∖e=o⁡a↔∀a∈𝒫⋃dom⁡Oo⁡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⁡Oo⁡a∩e+𝑒o⁡a∖e=o⁡a↔∀a∈𝒫⋃dom⁡OO⁡a∩e+𝑒O⁡a∖e=O⁡a
17 10 16 bitrd ⊢o=O→∀a∈𝒫⋃dom⁡oo⁡a∩e+𝑒o⁡a∖e=o⁡a↔∀a∈𝒫⋃dom⁡OO⁡a∩e+𝑒O⁡a∖e=O⁡a
18 9 17 rabeqbidv ⊢o=O→e∈𝒫⋃dom⁡o|∀a∈𝒫⋃dom⁡oo⁡a∩e+𝑒o⁡a∖e=o⁡a=e∈𝒫⋃dom⁡O|∀a∈𝒫⋃dom⁡OO⁡a∩e+𝑒O⁡a∖e=O⁡a
19 df-caragen ⊢CaraGen=o∈OutMeas⟼e∈𝒫⋃dom⁡o|∀a∈𝒫⋃dom⁡oo⁡a∩e+𝑒o⁡a∖e=o⁡a
20 18 19 fvmptg ⊢O∈OutMeas∧e∈𝒫⋃dom⁡O|∀a∈𝒫⋃dom⁡OO⁡a∩e+𝑒O⁡a∖e=O⁡a∈V→CaraGen⁡O=e∈𝒫⋃dom⁡O|∀a∈𝒫⋃dom⁡OO⁡a∩e+𝑒O⁡a∖e=O⁡a
21 1 6 20 syl2anc ⊢O∈OutMeas→CaraGen⁡O=e∈𝒫⋃dom⁡O|∀a∈𝒫⋃dom⁡OO⁡a∩e+𝑒O⁡a∖e=O⁡a