Theorem ofcfn

Description: The function operation produces a function. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Hypotheses	ofcfval.1	|- ( ph -> F Fn A )
	ofcfval.2	|- ( ph -> A e. V )
	ofcfval.3	|- ( ph -> C e. W )
Assertion	ofcfn	|- ( ph -> ( F oFC R C ) Fn A )

Proof

Step	Hyp	Ref	Expression
1		ofcfval.1	|- ( ph -> F Fn A )
2		ofcfval.2	|- ( ph -> A e. V )
3		ofcfval.3	|- ( ph -> C e. W )
4		ovex	|- ( ( F ` x ) R C ) e. _V
5		eqid	|- ( x e. A |-> ( ( F ` x ) R C ) ) = ( x e. A |-> ( ( F ` x ) R C ) )
6	4 5	fnmpti	|- ( x e. A |-> ( ( F ` x ) R C ) ) Fn A
7		eqidd	|- ( ( ph /\ x e. A ) -> ( F ` x ) = ( F ` x ) )
8	1 2 3 7	ofcfval	|- ( ph -> ( F oFC R C ) = ( x e. A |-> ( ( F ` x ) R C ) ) )
9	8	fneq1d	|- ( ph -> ( ( F oFC R C ) Fn A <-> ( x e. A |-> ( ( F ` x ) R C ) ) Fn A ) )
10	6 9	mpbiri	|- ( ph -> ( F oFC R C ) Fn A )