Metamath Proof Explorer


Theorem faeval

Description: Value of the 'almost everywhere' relation for a given relation and measure. (Contributed by Thierry Arnoux, 22-Oct-2017)

Ref Expression
Assertion faeval ( ( 𝑅 ∈ V ∧ 𝑀 ran measures ) → ( 𝑅 ~ a.e. 𝑀 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) } )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝑟 = 𝑅𝑚 = 𝑀 ) → 𝑟 = 𝑅 )
2 1 dmeqd ( ( 𝑟 = 𝑅𝑚 = 𝑀 ) → dom 𝑟 = dom 𝑅 )
3 simpr ( ( 𝑟 = 𝑅𝑚 = 𝑀 ) → 𝑚 = 𝑀 )
4 3 dmeqd ( ( 𝑟 = 𝑅𝑚 = 𝑀 ) → dom 𝑚 = dom 𝑀 )
5 4 unieqd ( ( 𝑟 = 𝑅𝑚 = 𝑀 ) → dom 𝑚 = dom 𝑀 )
6 2 5 oveq12d ( ( 𝑟 = 𝑅𝑚 = 𝑀 ) → ( dom 𝑟m dom 𝑚 ) = ( dom 𝑅m dom 𝑀 ) )
7 6 eleq2d ( ( 𝑟 = 𝑅𝑚 = 𝑀 ) → ( 𝑓 ∈ ( dom 𝑟m dom 𝑚 ) ↔ 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ) )
8 6 eleq2d ( ( 𝑟 = 𝑅𝑚 = 𝑀 ) → ( 𝑔 ∈ ( dom 𝑟m dom 𝑚 ) ↔ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) )
9 7 8 anbi12d ( ( 𝑟 = 𝑅𝑚 = 𝑀 ) → ( ( 𝑓 ∈ ( dom 𝑟m dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟m dom 𝑚 ) ) ↔ ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ) )
10 1 breqd ( ( 𝑟 = 𝑅𝑚 = 𝑀 ) → ( ( 𝑓𝑥 ) 𝑟 ( 𝑔𝑥 ) ↔ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) ) )
11 5 10 rabeqbidv ( ( 𝑟 = 𝑅𝑚 = 𝑀 ) → { 𝑥 dom 𝑚 ∣ ( 𝑓𝑥 ) 𝑟 ( 𝑔𝑥 ) } = { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } )
12 11 3 breq12d ( ( 𝑟 = 𝑅𝑚 = 𝑀 ) → ( { 𝑥 dom 𝑚 ∣ ( 𝑓𝑥 ) 𝑟 ( 𝑔𝑥 ) } a.e. 𝑚 ↔ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) )
13 9 12 anbi12d ( ( 𝑟 = 𝑅𝑚 = 𝑀 ) → ( ( ( 𝑓 ∈ ( dom 𝑟m dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟m dom 𝑚 ) ) ∧ { 𝑥 dom 𝑚 ∣ ( 𝑓𝑥 ) 𝑟 ( 𝑔𝑥 ) } a.e. 𝑚 ) ↔ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) ) )
14 13 opabbidv ( ( 𝑟 = 𝑅𝑚 = 𝑀 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑟m dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟m dom 𝑚 ) ) ∧ { 𝑥 dom 𝑚 ∣ ( 𝑓𝑥 ) 𝑟 ( 𝑔𝑥 ) } a.e. 𝑚 ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) } )
15 df-fae ~ a.e. = ( 𝑟 ∈ V , 𝑚 ran measures ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑟m dom 𝑚 ) ∧ 𝑔 ∈ ( dom 𝑟m dom 𝑚 ) ) ∧ { 𝑥 dom 𝑚 ∣ ( 𝑓𝑥 ) 𝑟 ( 𝑔𝑥 ) } a.e. 𝑚 ) } )
16 ovex ( dom 𝑅m dom 𝑀 ) ∈ V
17 16 16 xpex ( ( dom 𝑅m dom 𝑀 ) × ( dom 𝑅m dom 𝑀 ) ) ∈ V
18 opabssxp { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) } ⊆ ( ( dom 𝑅m dom 𝑀 ) × ( dom 𝑅m dom 𝑀 ) )
19 17 18 ssexi { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) } ∈ V
20 14 15 19 ovmpoa ( ( 𝑅 ∈ V ∧ 𝑀 ran measures ) → ( 𝑅 ~ a.e. 𝑀 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) } )