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 ~ a.e. = ( 𝑟 ∈ V , 𝑚 ran measures ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑟m dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟m dom 𝑚 ) ) ∧ { 𝑥 dom 𝑚 ∣ ( 𝑓𝑥 ) 𝑟 ( 𝑔𝑥 ) } a.e. 𝑚 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfae ~ a.e.
1 vr 𝑟
2 cvv V
3 vm 𝑚
4 cmeas measures
5 4 crn ran measures
6 5 cuni ran measures
7 vf 𝑓
8 vg 𝑔
9 7 cv 𝑓
10 1 cv 𝑟
11 10 cdm dom 𝑟
12 cmap m
13 3 cv 𝑚
14 13 cdm dom 𝑚
15 14 cuni dom 𝑚
16 11 15 12 co ( dom 𝑟m dom 𝑚 )
17 9 16 wcel 𝑓 ∈ ( dom 𝑟m dom 𝑚 )
18 8 cv 𝑔
19 18 16 wcel 𝑔 ∈ ( dom 𝑟m dom 𝑚 )
20 17 19 wa ( 𝑓 ∈ ( dom 𝑟m dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟m dom 𝑚 ) )
21 vx 𝑥
22 21 cv 𝑥
23 22 9 cfv ( 𝑓𝑥 )
24 22 18 cfv ( 𝑔𝑥 )
25 23 24 10 wbr ( 𝑓𝑥 ) 𝑟 ( 𝑔𝑥 )
26 25 21 15 crab { 𝑥 dom 𝑚 ∣ ( 𝑓𝑥 ) 𝑟 ( 𝑔𝑥 ) }
27 cae a.e.
28 26 13 27 wbr { 𝑥 dom 𝑚 ∣ ( 𝑓𝑥 ) 𝑟 ( 𝑔𝑥 ) } a.e. 𝑚
29 20 28 wa ( ( 𝑓 ∈ ( dom 𝑟m dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟m dom 𝑚 ) ) ∧ { 𝑥 dom 𝑚 ∣ ( 𝑓𝑥 ) 𝑟 ( 𝑔𝑥 ) } a.e. 𝑚 )
30 29 7 8 copab { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑟m dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟m dom 𝑚 ) ) ∧ { 𝑥 dom 𝑚 ∣ ( 𝑓𝑥 ) 𝑟 ( 𝑔𝑥 ) } a.e. 𝑚 ) }
31 1 3 2 6 30 cmpo ( 𝑟 ∈ V , 𝑚 ran measures ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑟m dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟m dom 𝑚 ) ) ∧ { 𝑥 dom 𝑚 ∣ ( 𝑓𝑥 ) 𝑟 ( 𝑔𝑥 ) } a.e. 𝑚 ) } )
32 0 31 wceq ~ a.e. = ( 𝑟 ∈ V , 𝑚 ran measures ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑟m dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟m dom 𝑚 ) ) ∧ { 𝑥 dom 𝑚 ∣ ( 𝑓𝑥 ) 𝑟 ( 𝑔𝑥 ) } a.e. 𝑚 ) } )