Definition df-fae 32113

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 32106	. 2 class ~ a.e.
2		vr	. . 3 setvar 𝑟
3		vm	. . 3 setvar 𝑚
4		cvv 3422	. . 3 class V
5		cmeas 32063	. . . . 5 class measures
6	5	crn 5581	. . . 4 class ran measures
7	6	cuni 4836	. . 3 class ∪ ran measures
8		vf	. . . . . . . 8 setvar 𝑓
9	8	cv 1538	. . . . . . 7 class 𝑓
10	2	cv 1538	. . . . . . . . 9 class 𝑟
11	10	cdm 5580	. . . . . . . 8 class dom 𝑟
12	3	cv 1538	. . . . . . . . . 10 class 𝑚
13	12	cdm 5580	. . . . . . . . 9 class dom 𝑚
14	13	cuni 4836	. . . . . . . 8 class ∪ dom 𝑚
15		cmap 8573	. . . . . . . 8 class ↑m
16	11, 14, 15	co 7255	. . . . . . 7 class (dom 𝑟 ↑m ∪ dom 𝑚)
17	9, 16	wcel 2108	. . . . . 6 wff 𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)
18		vg	. . . . . . . 8 setvar 𝑔
19	18	cv 1538	. . . . . . 7 class 𝑔
20	19, 16	wcel 2108	. . . . . 6 wff 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)
21	17, 20	wa 395	. . . . 5 wff (𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚))
22		vx	. . . . . . . . . 10 setvar 𝑥
23	22	cv 1538	. . . . . . . . 9 class 𝑥
24	23, 9	cfv 6418	. . . . . . . 8 class (𝑓‘𝑥)
25	23, 19	cfv 6418	. . . . . . . 8 class (𝑔‘𝑥)
26	24, 25, 10	wbr 5070	. . . . . . 7 wff (𝑓‘𝑥)𝑟(𝑔‘𝑥)
27	26, 22, 14	crab 3067	. . . . . 6 class {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}
28		cae 32105	. . . . . 6 class a.e.
29	27, 12, 28	wbr 5070	. . . . 5 wff {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚
30	21, 29	wa 395	. . . 4 wff ((𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)) ∧ {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚)
31	30, 8, 18	copab 5132	. . 3 class {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)) ∧ {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚)}
32	2, 3, 4, 7, 31	cmpo 7257	. 2 class (𝑟 ∈ V, 𝑚 ∈ ∪ ran measures ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)) ∧ {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚)})
33	1, 32	wceq 1539	1 wff ~ a.e. = (𝑟 ∈ V, 𝑚 ∈ ∪ ran measures ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟 ↑m ∪ dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟 ↑m ∪ dom 𝑚)) ∧ {𝑥 ∈ ∪ dom 𝑚 ∣ (𝑓‘𝑥)𝑟(𝑔‘𝑥)}a.e.𝑚)})

This definition is referenced by:  faeval  32114