Definition df-fae 31506

Description: Define a builder for an 'almost everywhere' relation between functions, from relations between function values. In this definition, the range of 𝑓 and 𝑔 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. = (𝑟 ∈ V, 𝑚 ∈ ∪ ran measures ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)) ∧ {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚)})

Distinct variable group:   𝑚,𝑟,𝑓,𝑔,𝑥

Detailed syntax breakdown of Definition df-fae

Step	Hyp	Ref	Expression
1		cfae 31499	. 2 class ~ a.e.
2		vr	. . 3 setvar 𝑟
3		vm	. . 3 setvar 𝑚
4		cvv 3496	. . 3 class V
5		cmeas 31456	. . . . 5 class measures
6	5	crn 5558	. . . 4 class ran measures
7	6	cuni 4840	. . 3 class ∪ ran measures
8		vf	. . . . . . . 8 setvar 𝑓
9	8	cv 1536	. . . . . . 7 class 𝑓
10	2	cv 1536	. . . . . . . . 9 class 𝑟
11	10	cdm 5557	. . . . . . . 8 class dom 𝑟
12	3	cv 1536	. . . . . . . . . 10 class 𝑚
13	12	cdm 5557	. . . . . . . . 9 class dom 𝑚
14	13	cuni 4840	. . . . . . . 8 class ∪ dom 𝑚
15		cmap 8408	. . . . . . . 8 class ↑m
16	11, 14, 15	co 7158	. . . . . . 7 class (dom 𝑟 ↑m ∪ dom 𝑚)
17	9, 16	wcel 2114	. . . . . 6 wff 𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)
18		vg	. . . . . . . 8 setvar 𝑔
19	18	cv 1536	. . . . . . 7 class 𝑔
20	19, 16	wcel 2114	. . . . . 6 wff 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)
21	17, 20	wa 398	. . . . 5 wff (𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚))
22		vx	. . . . . . . . . 10 setvar 𝑥
23	22	cv 1536	. . . . . . . . 9 class 𝑥
24	23, 9	cfv 6357	. . . . . . . 8 class (𝑓‘𝑥)
25	23, 19	cfv 6357	. . . . . . . 8 class (𝑔‘𝑥)
26	24, 25, 10	wbr 5068	. . . . . . 7 wff (𝑓‘𝑥)𝑟(𝑔‘𝑥)
27	26, 22, 14	crab 3144	. . . . . 6 class {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}
28		cae 31498	. . . . . 6 class a.e.
29	27, 12, 28	wbr 5068	. . . . 5 wff {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚
30	21, 29	wa 398	. . . 4 wff ((𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)) ∧ {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚)
31	30, 8, 18	copab 5130	. . 3 class {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)) ∧ {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚)}
32	2, 3, 4, 7, 31	cmpo 7160	. 2 class (𝑟 ∈ V, 𝑚 ∈ ∪ ran measures ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)) ∧ {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚)})
33	1, 32	wceq 1537	1 wff ~ a.e. = (𝑟 ∈ V, 𝑚 ∈ ∪ ran measures ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)) ∧ {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚)})

This definition is referenced by:  faeval  31507