Metamath Proof Explorer


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 φy=FxC=D
cofmpt2.2 φyBCE
cofmpt2.3 φF:AB
cofmpt2.4 φDV
Assertion cofmpt2 φyBCF=xAD

Proof

Step Hyp Ref Expression
1 cofmpt2.1 φy=FxC=D
2 cofmpt2.2 φyBCE
3 cofmpt2.3 φF:AB
4 cofmpt2.4 φDV
5 2 fmpttd φyBC:BE
6 fcompt yBC:BEF:AByBCF=xAyBCFx
7 5 3 6 syl2anc φyBCF=xAyBCFx
8 eqid yBC=yBC
9 1 adantlr φxAy=FxC=D
10 3 ffvelrnda φxAFxB
11 4 adantr φxADV
12 8 9 10 11 fvmptd2 φxAyBCFx=D
13 12 mpteq2dva φxAyBCFx=xAD
14 7 13 eqtrd φyBCF=xAD