Definition df-caragen 40706

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

Assertion

Ref	Expression
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 ) } )

Distinct variable group:   e, a, o

Detailed syntax breakdown of Definition df-caragen

Step	Hyp	Ref	Expression
1		ccaragen 40705	. 2 class CaraGen
2		vo	. . 3 setvar o
3		come 40703	. . 3 class OutMeas
4		va	. . . . . . . . . 10 setvar a
5	4	cv 1482	. . . . . . . . 9 class a
6		ve	. . . . . . . . . 10 setvar e
7	6	cv 1482	. . . . . . . . 9 class e
8	5, 7	cin 3573	. . . . . . . 8 class ( a i^i e )
9	2	cv 1482	. . . . . . . 8 class o
10	8, 9	cfv 5888	. . . . . . 7 class ( o ` ( a i^i e ) )
11	5, 7	cdif 3571	. . . . . . . 8 class ( a \ e )
12	11, 9	cfv 5888	. . . . . . 7 class ( o ` ( a \ e ) )
13		cxad 11944	. . . . . . 7 class +e
14	10, 12, 13	co 6650	. . . . . 6 class ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) )
15	5, 9	cfv 5888	. . . . . 6 class ( o ` a )
16	14, 15	wceq 1483	. . . . 5 wff ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( o ` a )
17	9	cdm 5114	. . . . . . 7 class dom o
18	17	cuni 4436	. . . . . 6 class U. dom o
19	18	cpw 4158	. . . . 5 class ~P U. dom o
20	16, 4, 19	wral 2912	. . . 4 wff A. a e. ~P U. dom o ( ( o ` ( a i^i e ) ) +e ( o ` ( a \ e ) ) ) = ( o ` a )
21	20, 6, 19	crab 2916	. . 3 class { 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	2, 3, 21	cmpt 4729	. 2 class ( 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 ) } )
23	1, 22	wceq 1483	1 wff 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 ) } )

This definition is referenced by:  caragenval  40707