Theorem brfae

Description: 'almost everywhere' relation for two functions F and G with regard to the measure M . (Contributed by Thierry Arnoux, 22-Oct-2017)

	Ref	Expression
Hypotheses	brfae.0	⊢ dom 𝑅 = 𝐷
	brfae.1	⊢ ( 𝜑 → 𝑅 ∈ V )
	brfae.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
	brfae.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 ↑m ∪ dom 𝑀 ) )
	brfae.4	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 ↑m ∪ dom 𝑀 ) )
Assertion	brfae	⊢ ( 𝜑 → ( 𝐹 ( 𝑅 ~ a.e. 𝑀 ) 𝐺 ↔ { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) } a.e. 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		brfae.0	⊢ dom 𝑅 = 𝐷
2		brfae.1	⊢ ( 𝜑 → 𝑅 ∈ V )
3		brfae.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
4		brfae.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 ↑m ∪ dom 𝑀 ) )
5		brfae.4	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 ↑m ∪ dom 𝑀 ) )
6		simpl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑓 = 𝐹 )
7	6	eleq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ↔ 𝐹 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) )
8		simpr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
9	8	eleq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑔 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ↔ 𝐺 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) )
10	7 9	anbi12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) ↔ ( 𝐹 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ∧ 𝐺 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) ) )
11	6	fveq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
12	8	fveq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
13	11 12	breq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) )
14	13	rabbidv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) } = { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) } )
15	14	breq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑀 ↔ { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) } a.e. 𝑀 ) )
16	10 15	anbi12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑓 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑀 ) ↔ ( ( 𝐹 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ∧ 𝐺 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) } a.e. 𝑀 ) ) )
17		eqid	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑀 ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑀 ) }
18	16 17	brabga	⊢ ( ( 𝐹 ∈ ( 𝐷 ↑m ∪ dom 𝑀 ) ∧ 𝐺 ∈ ( 𝐷 ↑m ∪ dom 𝑀 ) ) → ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑀 ) } 𝐺 ↔ ( ( 𝐹 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ∧ 𝐺 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) } a.e. 𝑀 ) ) )
19	4 5 18	syl2anc	⊢ ( 𝜑 → ( 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑀 ) } 𝐺 ↔ ( ( 𝐹 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ∧ 𝐺 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) } a.e. 𝑀 ) ) )
20		faeval	⊢ ( ( 𝑅 ∈ V ∧ 𝑀 ∈ ∪ ran measures ) → ( 𝑅 ~ a.e. 𝑀 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑀 ) } )
21	2 3 20	syl2anc	⊢ ( 𝜑 → ( 𝑅 ~ a.e. 𝑀 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑀 ) } )
22	21	breqd	⊢ ( 𝜑 → ( 𝐹 ( 𝑅 ~ a.e. 𝑀 ) 𝐺 ↔ 𝐹 { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ∧ 𝑔 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) } a.e. 𝑀 ) } 𝐺 ) )
23	1	oveq1i	⊢ ( dom 𝑅 ↑m ∪ dom 𝑀 ) = ( 𝐷 ↑m ∪ dom 𝑀 )
24	4 23	eleqtrrdi	⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) )
25	5 23	eleqtrrdi	⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) )
26	24 25	jca	⊢ ( 𝜑 → ( 𝐹 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ∧ 𝐺 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) )
27	26	biantrurd	⊢ ( 𝜑 → ( { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) } a.e. 𝑀 ↔ ( ( 𝐹 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ∧ 𝐺 ∈ ( dom 𝑅 ↑m ∪ dom 𝑀 ) ) ∧ { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) } a.e. 𝑀 ) ) )
28	19 22 27	3bitr4d	⊢ ( 𝜑 → ( 𝐹 ( 𝑅 ~ a.e. 𝑀 ) 𝐺 ↔ { 𝑥 ∈ ∪ dom 𝑀 ∣ ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) } a.e. 𝑀 ) )