Theorem ofcf

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

	Ref	Expression
Hypotheses	ofcf.1	|- ( ( ph /\ ( x e. S /\ y e. T ) ) -> ( x R y ) e. U )
	ofcf.2	|- ( ph -> F : A --> S )
	ofcf.4	|- ( ph -> A e. V )
	ofcf.5	|- ( ph -> C e. T )
Assertion	ofcf	|- ( ph -> ( F oFC R C ) : A --> U )

Proof

Step	Hyp	Ref	Expression
1		ofcf.1	|- ( ( ph /\ ( x e. S /\ y e. T ) ) -> ( x R y ) e. U )
2		ofcf.2	|- ( ph -> F : A --> S )
3		ofcf.4	|- ( ph -> A e. V )
4		ofcf.5	|- ( ph -> C e. T )
5	2	ffnd	|- ( ph -> F Fn A )
6		eqidd	|- ( ( ph /\ z e. A ) -> ( F ` z ) = ( F ` z ) )
7	5 3 4 6	ofcfval	|- ( ph -> ( F oFC R C ) = ( z e. A |-> ( ( F ` z ) R C ) ) )
8	2	ffvelrnda	|- ( ( ph /\ z e. A ) -> ( F ` z ) e. S )
9	4	adantr	|- ( ( ph /\ z e. A ) -> C e. T )
10	1	ralrimivva	|- ( ph -> A. x e. S A. y e. T ( x R y ) e. U )
11	10	adantr	|- ( ( ph /\ z e. A ) -> A. x e. S A. y e. T ( x R y ) e. U )
12		ovrspc2v	|- ( ( ( ( F ` z ) e. S /\ C e. T ) /\ A. x e. S A. y e. T ( x R y ) e. U ) -> ( ( F ` z ) R C ) e. U )
13	8 9 11 12	syl21anc	|- ( ( ph /\ z e. A ) -> ( ( F ` z ) R C ) e. U )
14	7 13	fmpt3d	|- ( ph -> ( F oFC R C ) : A --> U )