Definition df-fae

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)

	Ref	Expression
Assertion	df-fae	|- ~ae = ( 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 ) } ae m ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfae	|- ~ae
1		vr	|- r
2		cvv	|- _V
3		vm	|- m
4		cmeas	|- measures
5	4	crn	|- ran measures
6	5	cuni	|- U. ran measures
7		vf	|- f
8		vg	|- g
9	7	cv	|- f
10	1	cv	|- r
11	10	cdm	|- dom r
12		cmap	|- ^m
13	3	cv	|- m
14	13	cdm	|- dom m
15	14	cuni	|- U. dom m
16	11 15 12	co	|- ( dom r ^m U. dom m )
17	9 16	wcel	|- f e. ( dom r ^m U. dom m )
18	8	cv	|- g
19	18 16	wcel	|- g e. ( dom r ^m U. dom m )
20	17 19	wa	|- ( f e. ( dom r ^m U. dom m ) /\ g e. ( dom r ^m U. dom m ) )
21		vx	|- x
22	21	cv	|- x
23	22 9	cfv	|- ( f ` x )
24	22 18	cfv	|- ( g ` x )
25	23 24 10	wbr	|- ( f ` x ) r ( g ` x )
26	25 21 15	crab	|- { x e. U. dom m | ( f ` x ) r ( g ` x ) }
27		cae	|- ae
28	26 13 27	wbr	|- { x e. U. dom m | ( f ` x ) r ( g ` x ) } ae m
29	20 28	wa	|- ( ( 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 ) } ae m )
30	29 7 8	copab	|- { <. 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 ) } ae m ) }
31	1 3 2 6 30	cmpo	|- ( 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 ) } ae m ) } )
32	0 31	wceq	|- ~ae = ( 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 ) } ae m ) } )