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