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	$⊢ (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.)\}$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (r = R \land m = M) \to r = R$
2	1	dmeqd	$⊢ (r = R \land m = M) \to dom r = dom R$
3		simpr	$⊢ (r = R \land m = M) \to m = M$
4	3	dmeqd	$⊢ (r = R \land m = M) \to dom m = dom M$
5	4	unieqd	$⊢ (r = R \land m = M) \to ⋃ dom m = ⋃ dom M$
6	2 5	oveq12d	$⊢ (r = R \land m = M) \to {dom r}^{⋃ dom m} = {dom R}^{⋃ dom M}$
7	6	eleq2d	$⊢ (r = R \land m = M) \to (f \in ({dom r}^{⋃ dom m}) \leftrightarrow f \in ({dom R}^{⋃ dom M}))$
8	6	eleq2d	$⊢ (r = R \land m = M) \to (g \in ({dom r}^{⋃ dom m}) \leftrightarrow g \in ({dom R}^{⋃ dom M}))$
9	7 8	anbi12d	$⊢ (r = R \land m = M) \to ((f \in ({dom r}^{⋃ dom m}) \land g \in ({dom r}^{⋃ dom m})) \leftrightarrow (f \in ({dom R}^{⋃ dom M}) \land g \in ({dom R}^{⋃ dom M})))$
10	1	breqd	$⊢ (r = R \land m = M) \to (f (x) r g (x) \leftrightarrow f (x) R g (x))$
11	5 10	rabeqbidv	$⊢ (r = R \land m = M) \to \{x \in ⋃ dom m \| f (x) r g (x)\} = \{x \in ⋃ dom M \| f (x) R g (x)\}$
12	11 3	breq12d	$⊢ (r = R \land m = M) \to (\{x \in ⋃ dom m \| f (x) r g (x)\} m -ae. \leftrightarrow \{x \in ⋃ dom M \| f (x) R g (x)\} M -ae.)$
13	9 12	anbi12d	$⊢ (r = R \land m = M) \to (((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.) \leftrightarrow ((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.))$
14	13	opabbidv	$⊢ (r = R \land m = M) \to \{⟨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.)\} = \{⟨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.)\}$
15		df-fae	$⊢ ~_{ae} = (r \in V, m \in ⋃ ran measures ⟼ \{⟨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.)\})$
16		ovex	$⊢ {dom R}^{⋃ dom M} \in V$
17	16 16	xpex	$⊢ ({dom R}^{⋃ dom M}) \times ({dom R}^{⋃ dom M}) \in V$
18		opabssxp	$⊢ \{⟨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.)\} \subseteq ({dom R}^{⋃ dom M}) \times ({dom R}^{⋃ dom M})$
19	17 18	ssexi	$⊢ \{⟨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.)\} \in V$
20	14 15 19	ovmpoa	$⊢ (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.)\}$

Metamath Proof Explorer

Theorem faeval

Proof