Theorem ofcfval3

Description: General value of ( F oFC R C ) with no assumptions on functionality of F . (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Assertion	ofcfval3	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝑥 ∈ 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		mptexg	⊢ ( dom 𝐹 ∈ V → ( 𝑥 ∈ dom 𝐹 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) ∈ V )
7	5 6	syl	⊢ ( 𝐹 ∈ 𝑉 → ( 𝑥 ∈ dom 𝐹 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) ∈ V )
8	7	adantr	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝑥 ∈ dom 𝐹 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) ∈ V )
9		simpl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑐 = 𝐶 ) → 𝑓 = 𝐹 )
10	9	dmeqd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑐 = 𝐶 ) → dom 𝑓 = dom 𝐹 )
11	9	fveq1d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑐 = 𝐶 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
12		simpr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑐 = 𝐶 ) → 𝑐 = 𝐶 )
13	11 12	oveq12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑐 = 𝐶 ) → ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) )
14	10 13	mpteq12dv	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑐 = 𝐶 ) → ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 ) ) = ( 𝑥 ∈ dom 𝐹 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) )
15		df-ofc	⊢ ∘f/c 𝑅 = ( 𝑓 ∈ V , 𝑐 ∈ V ↦ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 ) ) )
16	14 15	ovmpoga	⊢ ( ( 𝐹 ∈ V ∧ 𝐶 ∈ V ∧ ( 𝑥 ∈ dom 𝐹 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) ∈ V ) → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝑥 ∈ dom 𝐹 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) )
17	2 4 8 16	syl3anc	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝑥 ∈ dom 𝐹 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) )