# Metamath Proof Explorer

## Theorem fcompt

Description: Express composition of two functions as a maps-to applying both in sequence. (Contributed by Stefan O'Rear, 5-Oct-2014) (Proof shortened by Mario Carneiro, 27-Dec-2014)

Ref Expression
Assertion fcompt ${⊢}\left({A}:{D}⟶{E}\wedge {B}:{C}⟶{D}\right)\to {A}\circ {B}=\left({x}\in {C}⟼{A}\left({B}\left({x}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 ffvelrn ${⊢}\left({B}:{C}⟶{D}\wedge {x}\in {C}\right)\to {B}\left({x}\right)\in {D}$
2 1 adantll ${⊢}\left(\left({A}:{D}⟶{E}\wedge {B}:{C}⟶{D}\right)\wedge {x}\in {C}\right)\to {B}\left({x}\right)\in {D}$
3 ffn ${⊢}{B}:{C}⟶{D}\to {B}Fn{C}$
4 3 adantl ${⊢}\left({A}:{D}⟶{E}\wedge {B}:{C}⟶{D}\right)\to {B}Fn{C}$
5 dffn5 ${⊢}{B}Fn{C}↔{B}=\left({x}\in {C}⟼{B}\left({x}\right)\right)$
6 4 5 sylib ${⊢}\left({A}:{D}⟶{E}\wedge {B}:{C}⟶{D}\right)\to {B}=\left({x}\in {C}⟼{B}\left({x}\right)\right)$
7 ffn ${⊢}{A}:{D}⟶{E}\to {A}Fn{D}$
8 7 adantr ${⊢}\left({A}:{D}⟶{E}\wedge {B}:{C}⟶{D}\right)\to {A}Fn{D}$
9 dffn5 ${⊢}{A}Fn{D}↔{A}=\left({y}\in {D}⟼{A}\left({y}\right)\right)$
10 8 9 sylib ${⊢}\left({A}:{D}⟶{E}\wedge {B}:{C}⟶{D}\right)\to {A}=\left({y}\in {D}⟼{A}\left({y}\right)\right)$
11 fveq2 ${⊢}{y}={B}\left({x}\right)\to {A}\left({y}\right)={A}\left({B}\left({x}\right)\right)$
12 2 6 10 11 fmptco ${⊢}\left({A}:{D}⟶{E}\wedge {B}:{C}⟶{D}\right)\to {A}\circ {B}=\left({x}\in {C}⟼{A}\left({B}\left({x}\right)\right)\right)$