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 30617
 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 𝑟𝑚 dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟𝑚 dom 𝑚)) ∧ {𝑥 dom 𝑚 ∣ (𝑓𝑥)𝑟(𝑔𝑥)}a.e.𝑚)})
Distinct variable group:   𝑚,𝑟,𝑓,𝑔,𝑥

Detailed syntax breakdown of Definition df-fae
StepHypRef Expression
1 cfae 30610 . 2 class ~ a.e.
2 vr . . 3 setvar 𝑟
3 vm . . 3 setvar 𝑚
4 cvv 3340 . . 3 class V
5 cmeas 30567 . . . . 5 class measures
65crn 5267 . . . 4 class ran measures
76cuni 4588 . . 3 class ran measures
8 vf . . . . . . . 8 setvar 𝑓
98cv 1631 . . . . . . 7 class 𝑓
102cv 1631 . . . . . . . . 9 class 𝑟
1110cdm 5266 . . . . . . . 8 class dom 𝑟
123cv 1631 . . . . . . . . . 10 class 𝑚
1312cdm 5266 . . . . . . . . 9 class dom 𝑚
1413cuni 4588 . . . . . . . 8 class dom 𝑚
15 cmap 8023 . . . . . . . 8 class 𝑚
1611, 14, 15co 6813 . . . . . . 7 class (dom 𝑟𝑚 dom 𝑚)
179, 16wcel 2139 . . . . . 6 wff 𝑓 ∈ (dom 𝑟𝑚 dom 𝑚)
18 vg . . . . . . . 8 setvar 𝑔
1918cv 1631 . . . . . . 7 class 𝑔
2019, 16wcel 2139 . . . . . 6 wff 𝑔 ∈ (dom 𝑟𝑚 dom 𝑚)
2117, 20wa 383 . . . . 5 wff (𝑓 ∈ (dom 𝑟𝑚 dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟𝑚 dom 𝑚))
22 vx . . . . . . . . . 10 setvar 𝑥
2322cv 1631 . . . . . . . . 9 class 𝑥
2423, 9cfv 6049 . . . . . . . 8 class (𝑓𝑥)
2523, 19cfv 6049 . . . . . . . 8 class (𝑔𝑥)
2624, 25, 10wbr 4804 . . . . . . 7 wff (𝑓𝑥)𝑟(𝑔𝑥)
2726, 22, 14crab 3054 . . . . . 6 class {𝑥 dom 𝑚 ∣ (𝑓𝑥)𝑟(𝑔𝑥)}
28 cae 30609 . . . . . 6 class a.e.
2927, 12, 28wbr 4804 . . . . 5 wff {𝑥 dom 𝑚 ∣ (𝑓𝑥)𝑟(𝑔𝑥)}a.e.𝑚
3021, 29wa 383 . . . 4 wff ((𝑓 ∈ (dom 𝑟𝑚 dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟𝑚 dom 𝑚)) ∧ {𝑥 dom 𝑚 ∣ (𝑓𝑥)𝑟(𝑔𝑥)}a.e.𝑚)
3130, 8, 18copab 4864 . . 3 class {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟𝑚 dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟𝑚 dom 𝑚)) ∧ {𝑥 dom 𝑚 ∣ (𝑓𝑥)𝑟(𝑔𝑥)}a.e.𝑚)}
322, 3, 4, 7, 31cmpt2 6815 . 2 class (𝑟 ∈ V, 𝑚 ran measures ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟𝑚 dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟𝑚 dom 𝑚)) ∧ {𝑥 dom 𝑚 ∣ (𝑓𝑥)𝑟(𝑔𝑥)}a.e.𝑚)})
331, 32wceq 1632 1 wff ~ a.e. = (𝑟 ∈ V, 𝑚 ran measures ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (dom 𝑟𝑚 dom 𝑚) ∧ 𝑔 ∈ (dom 𝑟𝑚 dom 𝑚)) ∧ {𝑥 dom 𝑚 ∣ (𝑓𝑥)𝑟(𝑔𝑥)}a.e.𝑚)})
 Colors of variables: wff setvar class This definition is referenced by:  faeval  30618
 Copyright terms: Public domain W3C validator