Theorem cofmpt2

Description: Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 15-Jul-2023)

	Ref	Expression
Hypotheses	cofmpt2.1	|- ( ( ph /\ y = ( F ` x ) ) -> C = D )
	cofmpt2.2	|- ( ( ph /\ y e. B ) -> C e. E )
	cofmpt2.3	|- ( ph -> F : A --> B )
	cofmpt2.4	|- ( ph -> D e. V )
Assertion	cofmpt2	|- ( ph -> ( ( y e. B |-> C ) o. F ) = ( x e. A |-> D ) )

Proof

Step	Hyp	Ref	Expression
1		cofmpt2.1	|- ( ( ph /\ y = ( F ` x ) ) -> C = D )
2		cofmpt2.2	|- ( ( ph /\ y e. B ) -> C e. E )
3		cofmpt2.3	|- ( ph -> F : A --> B )
4		cofmpt2.4	|- ( ph -> D e. V )
5	2	fmpttd	|- ( ph -> ( y e. B |-> C ) : B --> E )
6		fcompt	|- ( ( ( y e. B |-> C ) : B --> E /\ F : A --> B ) -> ( ( y e. B |-> C ) o. F ) = ( x e. A |-> ( ( y e. B |-> C ) ` ( F ` x ) ) ) )
7	5 3 6	syl2anc	|- ( ph -> ( ( y e. B |-> C ) o. F ) = ( x e. A |-> ( ( y e. B |-> C ) ` ( F ` x ) ) ) )
8		eqid	|- ( y e. B |-> C ) = ( y e. B |-> C )
9	1	adantlr	|- ( ( ( ph /\ x e. A ) /\ y = ( F ` x ) ) -> C = D )
10	3	ffvelrnda	|- ( ( ph /\ x e. A ) -> ( F ` x ) e. B )
11	4	adantr	|- ( ( ph /\ x e. A ) -> D e. V )
12	8 9 10 11	fvmptd2	|- ( ( ph /\ x e. A ) -> ( ( y e. B |-> C ) ` ( F ` x ) ) = D )
13	12	mpteq2dva	|- ( ph -> ( x e. A |-> ( ( y e. B |-> C ) ` ( F ` x ) ) ) = ( x e. A |-> D ) )
14	7 13	eqtrd	|- ( ph -> ( ( y e. B |-> C ) o. F ) = ( x e. A |-> D ) )