This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem offval3

Description: General value of ( F oF R G ) with no assumptions on functionality of F and G . (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Assertion offval3 ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ V )
2 1 adantr ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → 𝐹 ∈ V )
3 elex ⊢ ( 𝐺 ∈ 𝑊 → 𝐺 ∈ V )
4 3 adantl ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → 𝐺 ∈ V )
5 dmexg ⊢ ( 𝐹 ∈ 𝑉 → dom 𝐹 ∈ V )
6 inex1g ⊢ ( dom 𝐹 ∈ V → ( dom 𝐹 ∩ dom 𝐺 ) ∈ V )
7 mptexg ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) ∈ V → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ∈ V )
8 5 6 7 3syl ⊢ ( 𝐹 ∈ 𝑉 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ∈ V )
9 8 adantr ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ∈ V )
10 dmeq ⊢ ( 𝑎 = 𝐹 → dom 𝑎 = dom 𝐹 )
11 dmeq ⊢ ( 𝑏 = 𝐺 → dom 𝑏 = dom 𝐺 )
12 10 11 ineqan12d ⊢ ( ( 𝑎 = 𝐹 ∧ 𝑏 = 𝐺 ) → ( dom 𝑎 ∩ dom 𝑏 ) = ( dom 𝐹 ∩ dom 𝐺 ) )
13 fveq1 ⊢ ( 𝑎 = 𝐹 → ( 𝑎 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
14 fveq1 ⊢ ( 𝑏 = 𝐺 → ( 𝑏 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
15 13 14 oveqan12d ⊢ ( ( 𝑎 = 𝐹 ∧ 𝑏 = 𝐺 ) → ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) )
16 12 15 mpteq12dv ⊢ ( ( 𝑎 = 𝐹 ∧ 𝑏 = 𝐺 ) → ( 𝑥 ∈ ( dom 𝑎 ∩ dom 𝑏 ) ↦ ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
17 df-of ⊢ ∘f 𝑅 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑎 ∩ dom 𝑏 ) ↦ ( ( 𝑎 ‘ 𝑥 ) 𝑅 ( 𝑏 ‘ 𝑥 ) ) ) )
18 16 17 ovmpoga ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ∧ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) ∈ V ) → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )
19 2 4 9 18 syl3anc ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )