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 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) } )

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	⊢ +e
14	9 10	cdif	⊢ ( 𝑎 ∖ 𝑒 )
15	14 4	cfv	⊢ ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) )
16	12 15 13	co	⊢ ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) )
17	9 4	cfv	⊢ ( 𝑜 ‘ 𝑎 )
18	16 17	wceq	⊢ ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 )
19	18 8 7	wral	⊢ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 )
20	19 3 7	crab	⊢ { 𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) }
21	1 2 20	cmpt	⊢ ( 𝑜 ∈ OutMeas ↦ { 𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) } )
22	0 21	wceq	⊢ CaraGen = ( 𝑜 ∈ OutMeas ↦ { 𝑒 ∈ 𝒫 ∪ dom 𝑜 ∣ ∀ 𝑎 ∈ 𝒫 ∪ dom 𝑜 ( ( 𝑜 ‘ ( 𝑎 ∩ 𝑒 ) ) +e ( 𝑜 ‘ ( 𝑎 ∖ 𝑒 ) ) ) = ( 𝑜 ‘ 𝑎 ) } )