Definition df-fae 30308

Description: Define a builder for an 'almost everywhere' relation between functions, from relations between function values. In this definition, the range of f and g is enforced in order to ensure the resulting relation is a set. (Contributed by Thierry Arnoux, 22-Oct-2017.)

Assertion

Ref	Expression
df-fae	|- ~ a.e. = ( r e. _V , m e. U. ran measures |-> { <. f , g >. | ( ( f e. ( dom r ^m U. dom m ) /\ g e. ( dom r ^m U. dom m ) ) /\ { x e. U. dom m | ( f ` x ) r ( g ` x ) }a.e. m ) } )

Distinct variable group:   m, r, f, g, x

Detailed syntax breakdown of Definition df-fae

Step	Hyp	Ref	Expression
1		cfae 30301	. 2 class ~ a.e.
2		vr	. . 3 setvar r
3		vm	. . 3 setvar m
4		cvv 3200	. . 3 class _V
5		cmeas 30258	. . . . 5 class measures
6	5	crn 5115	. . . 4 class ran measures
7	6	cuni 4436	. . 3 class U. ran measures
8		vf	. . . . . . . 8 setvar f
9	8	cv 1482	. . . . . . 7 class f
10	2	cv 1482	. . . . . . . . 9 class r
11	10	cdm 5114	. . . . . . . 8 class dom r
12	3	cv 1482	. . . . . . . . . 10 class m
13	12	cdm 5114	. . . . . . . . 9 class dom m
14	13	cuni 4436	. . . . . . . 8 class U. dom m
15		cmap 7857	. . . . . . . 8 class ^m
16	11, 14, 15	co 6650	. . . . . . 7 class ( dom r ^m U. dom m )
17	9, 16	wcel 1990	. . . . . 6 wff f e. ( dom r ^m U. dom m )
18		vg	. . . . . . . 8 setvar g
19	18	cv 1482	. . . . . . 7 class g
20	19, 16	wcel 1990	. . . . . 6 wff g e. ( dom r ^m U. dom m )
21	17, 20	wa 384	. . . . 5 wff ( f e. ( dom r ^m U. dom m ) /\ g e. ( dom r ^m U. dom m ) )
22		vx	. . . . . . . . . 10 setvar x
23	22	cv 1482	. . . . . . . . 9 class x
24	23, 9	cfv 5888	. . . . . . . 8 class ( f ` x )
25	23, 19	cfv 5888	. . . . . . . 8 class ( g ` x )
26	24, 25, 10	wbr 4653	. . . . . . 7 wff ( f ` x ) r ( g ` x )
27	26, 22, 14	crab 2916	. . . . . 6 class { x e. U. dom m | ( f ` x ) r ( g ` x ) }
28		cae 30300	. . . . . 6 class a.e.
29	27, 12, 28	wbr 4653	. . . . 5 wff { x e. U. dom m | ( f ` x ) r ( g ` x ) }a.e. m
30	21, 29	wa 384	. . . 4 wff ( ( f e. ( dom r ^m U. dom m ) /\ g e. ( dom r ^m U. dom m ) ) /\ { x e. U. dom m | ( f ` x ) r ( g ` x ) }a.e. m )
31	30, 8, 18	copab 4712	. . 3 class { <. f , g >. | ( ( f e. ( dom r ^m U. dom m ) /\ g e. ( dom r ^m U. dom m ) ) /\ { x e. U. dom m | ( f ` x ) r ( g ` x ) }a.e. m ) }
32	2, 3, 4, 7, 31	cmpt2 6652	. 2 class ( r e. _V , m e. U. ran measures |-> { <. f , g >. | ( ( f e. ( dom r ^m U. dom m ) /\ g e. ( dom r ^m U. dom m ) ) /\ { x e. U. dom m | ( f ` x ) r ( g ` x ) }a.e. m ) } )
33	1, 32	wceq 1483	1 wff ~ a.e. = ( r e. _V , m e. U. ran measures |-> { <. f , g >. | ( ( f e. ( dom r ^m U. dom m ) /\ g e. ( dom r ^m U. dom m ) ) /\ { x e. U. dom m | ( f ` x ) r ( g ` x ) }a.e. m ) } )

This definition is referenced by:  faeval  30309