Metamath Proof Explorer


Definition df-caragen

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

Ref Expression
Assertion df-caragen CaraGen = ( 𝑜 ∈ OutMeas ↦ { 𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀ 𝑎 ∈ 𝒫 dom 𝑜 ( ( 𝑜 ‘ ( 𝑎𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎𝑒 ) ) ) = ( 𝑜𝑎 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccaragen CaraGen
1 vo 𝑜
2 come OutMeas
3 ve 𝑒
4 1 cv 𝑜
5 4 cdm dom 𝑜
6 5 cuni dom 𝑜
7 6 cpw 𝒫 dom 𝑜
8 va 𝑎
9 8 cv 𝑎
10 3 cv 𝑒
11 9 10 cin ( 𝑎𝑒 )
12 11 4 cfv ( 𝑜 ‘ ( 𝑎𝑒 ) )
13 cxad +𝑒
14 9 10 cdif ( 𝑎𝑒 )
15 14 4 cfv ( 𝑜 ‘ ( 𝑎𝑒 ) )
16 12 15 13 co ( ( 𝑜 ‘ ( 𝑎𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎𝑒 ) ) )
17 9 4 cfv ( 𝑜𝑎 )
18 16 17 wceq ( ( 𝑜 ‘ ( 𝑎𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎𝑒 ) ) ) = ( 𝑜𝑎 )
19 18 8 7 wral 𝑎 ∈ 𝒫 dom 𝑜 ( ( 𝑜 ‘ ( 𝑎𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎𝑒 ) ) ) = ( 𝑜𝑎 )
20 19 3 7 crab { 𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀ 𝑎 ∈ 𝒫 dom 𝑜 ( ( 𝑜 ‘ ( 𝑎𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎𝑒 ) ) ) = ( 𝑜𝑎 ) }
21 1 2 20 cmpt ( 𝑜 ∈ OutMeas ↦ { 𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀ 𝑎 ∈ 𝒫 dom 𝑜 ( ( 𝑜 ‘ ( 𝑎𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎𝑒 ) ) ) = ( 𝑜𝑎 ) } )
22 0 21 wceq CaraGen = ( 𝑜 ∈ OutMeas ↦ { 𝑒 ∈ 𝒫 dom 𝑜 ∣ ∀ 𝑎 ∈ 𝒫 dom 𝑜 ( ( 𝑜 ‘ ( 𝑎𝑒 ) ) +𝑒 ( 𝑜 ‘ ( 𝑎𝑒 ) ) ) = ( 𝑜𝑎 ) } )