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 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐺 ‘ 𝑥 ) ) ) )