Theorem fvovco

Description: Value of the composition of an operator, with a given function. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	fvovco.1	|- ( ph -> F : X --> ( V X. W ) )
	fvovco.2	|- ( ph -> Y e. X )
Assertion	fvovco	|- ( ph -> ( ( O o. F ) ` Y ) = ( ( 1st ` ( F ` Y ) ) O ( 2nd ` ( F ` Y ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fvovco.1	|- ( ph -> F : X --> ( V X. W ) )
2		fvovco.2	|- ( ph -> Y e. X )
3	1 2	ffvelrnd	|- ( ph -> ( F ` Y ) e. ( V X. W ) )
4		1st2nd2	|- ( ( F ` Y ) e. ( V X. W ) -> ( F ` Y ) = <. ( 1st ` ( F ` Y ) ) , ( 2nd ` ( F ` Y ) ) >. )
5	3 4	syl	|- ( ph -> ( F ` Y ) = <. ( 1st ` ( F ` Y ) ) , ( 2nd ` ( F ` Y ) ) >. )
6	5	fveq2d	|- ( ph -> ( O ` ( F ` Y ) ) = ( O ` <. ( 1st ` ( F ` Y ) ) , ( 2nd ` ( F ` Y ) ) >. ) )
7		fvco3	|- ( ( F : X --> ( V X. W ) /\ Y e. X ) -> ( ( O o. F ) ` Y ) = ( O ` ( F ` Y ) ) )
8	1 2 7	syl2anc	|- ( ph -> ( ( O o. F ) ` Y ) = ( O ` ( F ` Y ) ) )
9		df-ov	|- ( ( 1st ` ( F ` Y ) ) O ( 2nd ` ( F ` Y ) ) ) = ( O ` <. ( 1st ` ( F ` Y ) ) , ( 2nd ` ( F ` Y ) ) >. )
10	9	a1i	|- ( ph -> ( ( 1st ` ( F ` Y ) ) O ( 2nd ` ( F ` Y ) ) ) = ( O ` <. ( 1st ` ( F ` Y ) ) , ( 2nd ` ( F ` Y ) ) >. ) )
11	6 8 10	3eqtr4d	|- ( ph -> ( ( O o. F ) ` Y ) = ( ( 1st ` ( F ` Y ) ) O ( 2nd ` ( F ` Y ) ) ) )