Metamath Proof Explorer

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∈V,m∈⋃ran⁡measures⟼fg|f∈dom⁡r⋃dom⁡m∧g∈dom⁡r⋃dom⁡m∧x∈⋃dom⁡m|f⁡xrg⁡xm-ae.

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfae class~ae
1 vr setvarr
2 cvv classV
3 vm setvarm
4 cmeas classmeasures
5 4 crn classran⁡measures
6 5 cuni class⋃ran⁡measures
7 vf setvarf
8 vg setvarg
9 7 cv setvarf
10 1 cv setvarr
11 10 cdm classdom⁡r
12 cmap class↑𝑚
13 3 cv setvarm
14 13 cdm classdom⁡m
15 14 cuni class⋃dom⁡m
16 11 15 12 co classdom⁡r⋃dom⁡m
17 9 16 wcel wfff∈dom⁡r⋃dom⁡m
18 8 cv setvarg
19 18 16 wcel wffg∈dom⁡r⋃dom⁡m
20 17 19 wa wfff∈dom⁡r⋃dom⁡m∧g∈dom⁡r⋃dom⁡m
21 vx setvarx
22 21 cv setvarx
23 22 9 cfv classf⁡x
24 22 18 cfv classg⁡x
25 23 24 10 wbr wfff⁡xrg⁡x
26 25 21 15 crab classx∈⋃dom⁡m|f⁡xrg⁡x
27 cae classae
28 26 13 27 wbr wffx∈⋃dom⁡m|f⁡xrg⁡xm-ae.
29 20 28 wa wfff∈dom⁡r⋃dom⁡m∧g∈dom⁡r⋃dom⁡m∧x∈⋃dom⁡m|f⁡xrg⁡xm-ae.
30 29 7 8 copab classfg|f∈dom⁡r⋃dom⁡m∧g∈dom⁡r⋃dom⁡m∧x∈⋃dom⁡m|f⁡xrg⁡xm-ae.
31 1 3 2 6 30 cmpo classr∈V,m∈⋃ran⁡measures⟼fg|f∈dom⁡r⋃dom⁡m∧g∈dom⁡r⋃dom⁡m∧x∈⋃dom⁡m|f⁡xrg⁡xm-ae.
32 0 31 wceq wff~ae=r∈V,m∈⋃ran⁡measures⟼fg|f∈dom⁡r⋃dom⁡m∧g∈dom⁡r⋃dom⁡m∧x∈⋃dom⁡m|f⁡xrg⁡xm-ae.