Metamath Proof Explorer


Theorem relfae

Description: The 'almost everywhere' builder for functions produces relations. (Contributed by Thierry Arnoux, 22-Oct-2017)

Ref Expression
Assertion relfae ( ( 𝑅 ∈ V ∧ 𝑀 ran measures ) → Rel ( 𝑅 ~ a.e. 𝑀 ) )

Proof

Step Hyp Ref Expression
1 relopabv Rel { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) }
2 faeval ( ( 𝑅 ∈ V ∧ 𝑀 ran measures ) → ( 𝑅 ~ a.e. 𝑀 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) } )
3 2 releqd ( ( 𝑅 ∈ V ∧ 𝑀 ran measures ) → ( Rel ( 𝑅 ~ a.e. 𝑀 ) ↔ Rel { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅m dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅m dom 𝑀 ) ) ∧ { 𝑥 dom 𝑀 ∣ ( 𝑓𝑥 ) 𝑅 ( 𝑔𝑥 ) } a.e. 𝑀 ) } ) )
4 1 3 mpbiri ( ( 𝑅 ∈ V ∧ 𝑀 ran measures ) → Rel ( 𝑅 ~ a.e. 𝑀 ) )