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	⊢ ~a.e. = ( 𝑟 ∈ V , 𝑚 ∈ ∪ ran measures ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑚 ∣ ( 𝑓 ‘ 𝑥 ) 𝑟 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑚 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfae	⊢ ~a.e.
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vm	⊢ 𝑚
4		cmeas	⊢ measures
5	4	crn	⊢ ran measures
6	5	cuni	⊢ ∪ ran measures
7		vf	⊢ 𝑓
8		vg	⊢ 𝑔
9	7	cv	⊢ 𝑓
10	1	cv	⊢ 𝑟
11	10	cdm	⊢ dom 𝑟
12		cmap	⊢ ↑m
13	3	cv	⊢ 𝑚
14	13	cdm	⊢ dom 𝑚
15	14	cuni	⊢ ∪ dom 𝑚
16	11 15 12	co	⊢ ( dom 𝑟 ↑m ∪ dom 𝑚 )
17	9 16	wcel	⊢ 𝑓 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 )
18	8	cv	⊢ 𝑔
19	18 16	wcel	⊢ 𝑔 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 )
20	17 19	wa	⊢ ( 𝑓 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) )
21		vx	⊢ 𝑥
22	21	cv	⊢ 𝑥
23	22 9	cfv	⊢ ( 𝑓 ‘ 𝑥 )
24	22 18	cfv	⊢ ( 𝑔 ‘ 𝑥 )
25	23 24 10	wbr	⊢ ( 𝑓 ‘ 𝑥 ) 𝑟 ( 𝑔 ‘ 𝑥 )
26	25 21 15	crab	⊢ { 𝑥 ∈ ∪ dom 𝑚 ∣ ( 𝑓 ‘ 𝑥 ) 𝑟 ( 𝑔 ‘ 𝑥 ) }
27		cae	⊢ a.e.
28	26 13 27	wbr	⊢ { 𝑥 ∈ ∪ dom 𝑚 ∣ ( 𝑓 ‘ 𝑥 ) 𝑟 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑚
29	20 28	wa	⊢ ( ( 𝑓 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑚 ∣ ( 𝑓 ‘ 𝑥 ) 𝑟 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑚 )
30	29 7 8	copab	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑚 ∣ ( 𝑓 ‘ 𝑥 ) 𝑟 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑚 ) }
31	1 3 2 6 30	cmpo	⊢ ( 𝑟 ∈ V , 𝑚 ∈ ∪ ran measures ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑚 ∣ ( 𝑓 ‘ 𝑥 ) 𝑟 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑚 ) } )
32	0 31	wceq	⊢ ~a.e. = ( 𝑟 ∈ V , 𝑚 ∈ ∪ ran measures ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟 ↑m ∪ dom 𝑚 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑚 ∣ ( 𝑓 ‘ 𝑥 ) 𝑟 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑚 ) } )