Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fae Structured version   Visualization version   GIF version

Definition df-fae 31578
 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
StepHypRef Expression
1 cfae 31571 . 2 class ~ a.e.
2 vr . . 3 setvar 𝑟
3 vm . . 3 setvar 𝑚
4 cvv 3469 . . 3 class V
5 cmeas 31528 . . . . 5 class measures
65crn 5533 . . . 4 class ran measures
76cuni 4813 . . 3 class ran measures
8 vf . . . . . . . 8 setvar 𝑓
98cv 1537 . . . . . . 7 class 𝑓
102cv 1537 . . . . . . . . 9 class 𝑟
1110cdm 5532 . . . . . . . 8 class dom 𝑟
123cv 1537 . . . . . . . . . 10 class 𝑚
1312cdm 5532 . . . . . . . . 9 class dom 𝑚
1413cuni 4813 . . . . . . . 8 class dom 𝑚
15 cmap 8393 . . . . . . . 8 class m
1611, 14, 15co 7140 . . . . . . 7 class (dom 𝑟m dom 𝑚)
179, 16wcel 2114 . . . . . 6 wff 𝑓 ∈ (dom 𝑟m dom 𝑚)
18 vg . . . . . . . 8 setvar 𝑔
1918cv 1537 . . . . . . 7 class 𝑔
2019, 16wcel 2114 . . . . . 6 wff 𝑔 ∈ (dom 𝑟m dom 𝑚)
2117, 20wa 399 . . . . 5 wff (𝑓 ∈ (dom 𝑟m dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟m dom 𝑚))
22 vx . . . . . . . . . 10 setvar 𝑥
2322cv 1537 . . . . . . . . 9 class 𝑥
2423, 9cfv 6334 . . . . . . . 8 class (𝑓𝑥)
2523, 19cfv 6334 . . . . . . . 8 class (𝑔𝑥)
2624, 25, 10wbr 5042 . . . . . . 7 wff (𝑓𝑥)𝑟(𝑔𝑥)
2726, 22, 14crab 3134 . . . . . 6 class {𝑥 dom 𝑚 ∣ (𝑓𝑥)𝑟(𝑔𝑥)}
28 cae 31570 . . . . . 6 class a.e.
2927, 12, 28wbr 5042 . . . . 5 wff {𝑥 dom 𝑚 ∣ (𝑓𝑥)𝑟(𝑔𝑥)}a.e.𝑚
3021, 29wa 399 . . . 4 wff ((𝑓 ∈ (dom 𝑟m dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟m dom 𝑚)) ∧ {𝑥 dom 𝑚 ∣ (𝑓𝑥)𝑟(𝑔𝑥)}a.e.𝑚)
3130, 8, 18copab 5104 . . 3 class {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟m dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟m dom 𝑚)) ∧ {𝑥 dom 𝑚 ∣ (𝑓𝑥)𝑟(𝑔𝑥)}a.e.𝑚)}
322, 3, 4, 7, 31cmpo 7142 . 2 class (𝑟 ∈ V, 𝑚 ran measures ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟m dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟m dom 𝑚)) ∧ {𝑥 dom 𝑚 ∣ (𝑓𝑥)𝑟(𝑔𝑥)}a.e.𝑚)})
331, 32wceq 1538 1 wff ~ a.e. = (𝑟 ∈ V, 𝑚 ran measures ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟m dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟m dom 𝑚)) ∧ {𝑥 dom 𝑚 ∣ (𝑓𝑥)𝑟(𝑔𝑥)}a.e.𝑚)})
 Colors of variables: wff setvar class This definition is referenced by:  faeval  31579
 Copyright terms: Public domain W3C validator