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. 𝑀 ) )