Metamath Proof Explorer

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