relfae

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

		Ref	Expression
	Assertion	relfae	$⊢ (R \in V \land M \in ⋃ ran measures) \to Rel (R ~_{ae} M)$

Step	Hyp	Ref	Expression
1		relopabv	$⊢ Rel \{⟨f, g⟩ \| ((f \in ({dom R}^{⋃ dom M}) \land g \in ({dom R}^{⋃ dom M})) \land \{x \in ⋃ dom M \| f (x) R g (x)\} M -ae.)\}$
2		faeval	$⊢ (R \in V \land M \in ⋃ ran measures) \to R ~_{ae} M = \{⟨f, g⟩ \| ((f \in ({dom R}^{⋃ dom M}) \land g \in ({dom R}^{⋃ dom M})) \land \{x \in ⋃ dom M \| f (x) R g (x)\} M -ae.)\}$
3	2	releqd	$⊢ (R \in V \land M \in ⋃ ran measures) \to (Rel (R ~_{ae} M) \leftrightarrow Rel \{⟨f, g⟩ \| ((f \in ({dom R}^{⋃ dom M}) \land g \in ({dom R}^{⋃ dom M})) \land \{x \in ⋃ dom M \| f (x) R g (x)\} M -ae.)\})$
4	1 3	mpbiri	$⊢ (R \in V \land M \in ⋃ ran measures) \to Rel (R ~_{ae} M)$

Metamath Proof Explorer