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 = ( o e. OutMeas |-> { e e. ~P U. dom o | A. a e. ~P U. dom o ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( o ` a ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccaragen	|- CaraGen
1		vo	|- o
2		come	|- OutMeas
3		ve	|- e
4	1	cv	|- o
5	4	cdm	|- dom o
6	5	cuni	|- U. dom o
7	6	cpw	|- ~P U. dom o
8		va	|- a
9	8	cv	|- a
10	3	cv	|- e
11	9 10	cin	|- ( a i^i e )
12	11 4	cfv	|- ( o ` ( a i^i e ) )
13		cxad	|- +e
14	9 10	cdif	|- ( a \ e )
15	14 4	cfv	|- ( o ` ( a \ e ) )
16	12 15 13	co	|- ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) )
17	9 4	cfv	|- ( o ` a )
18	16 17	wceq	|- ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( o ` a )
19	18 8 7	wral	|- A. a e. ~P U. dom o ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( o ` a )
20	19 3 7	crab	|- { e e. ~P U. dom o | A. a e. ~P U. dom o ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( o ` a ) }
21	1 2 20	cmpt	|- ( o e. OutMeas |-> { e e. ~P U. dom o | A. a e. ~P U. dom o ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( o ` a ) } )
22	0 21	wceq	|- CaraGen = ( o e. OutMeas |-> { e e. ~P U. dom o | A. a e. ~P U. dom o ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( o ` a ) } )