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 ⟼ f g | f ∈ dom ⁡ r ⋃ dom ⁡ m ∧ g ∈ dom ⁡ r ⋃ dom ⁡ m ∧ x ∈ ⋃ dom ⁡ m | f ⁡ x r g ⁡ x m-ae.

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfae class ~ae
1 vr setvar r
2 cvv class V
3 vm setvar m
4 cmeas class measures
5 4 crn class ran ⁡ measures
6 5 cuni class ⋃ ran ⁡ measures
7 vf setvar f
8 vg setvar g
9 7 cv setvar f
10 1 cv setvar r
11 10 cdm class dom ⁡ r
12 cmap class ↑ 𝑚
13 3 cv setvar m
14 13 cdm class dom ⁡ m
15 14 cuni class ⋃ dom ⁡ m
16 11 15 12 co class dom ⁡ r ⋃ dom ⁡ m
17 9 16 wcel wff f ∈ dom ⁡ r ⋃ dom ⁡ m
18 8 cv setvar g
19 18 16 wcel wff g ∈ dom ⁡ r ⋃ dom ⁡ m
20 17 19 wa wff f ∈ dom ⁡ r ⋃ dom ⁡ m ∧ g ∈ dom ⁡ r ⋃ dom ⁡ m
21 vx setvar x
22 21 cv setvar x
23 22 9 cfv class f ⁡ x
24 22 18 cfv class g ⁡ x
25 23 24 10 wbr wff f ⁡ x r g ⁡ x
26 25 21 15 crab class x ∈ ⋃ dom ⁡ m | f ⁡ x r g ⁡ x
27 cae class ae
28 26 13 27 wbr wff x ∈ ⋃ dom ⁡ m | f ⁡ x r g ⁡ x m-ae.
29 20 28 wa wff f ∈ dom ⁡ r ⋃ dom ⁡ m ∧ g ∈ dom ⁡ r ⋃ dom ⁡ m ∧ x ∈ ⋃ dom ⁡ m | f ⁡ x r g ⁡ x m-ae.
30 29 7 8 copab class f g | f ∈ dom ⁡ r ⋃ dom ⁡ m ∧ g ∈ dom ⁡ r ⋃ dom ⁡ m ∧ x ∈ ⋃ dom ⁡ m | f ⁡ x r g ⁡ x m-ae.
31 1 3 2 6 30 cmpo class r ∈ V , m ∈ ⋃ ran ⁡ measures ⟼ f g | f ∈ dom ⁡ r ⋃ dom ⁡ m ∧ g ∈ dom ⁡ r ⋃ dom ⁡ m ∧ x ∈ ⋃ dom ⁡ m | f ⁡ x r g ⁡ x m-ae.
32 0 31 wceq wff ~ae = r ∈ V , m ∈ ⋃ ran ⁡ measures ⟼ f g | f ∈ dom ⁡ r ⋃ dom ⁡ m ∧ g ∈ dom ⁡ r ⋃ dom ⁡ m ∧ x ∈ ⋃ dom ⁡ m | f ⁡ x r g ⁡ x m-ae.