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 BFnC$$
4	3	adantl	$$⊢\left(A:D⟶E\wedge B:C⟶D\right)\to BFnC$$
5		dffn5	$$⊢BFnC\leftrightarrow 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 AFnD$$
8	7	adantr	$$⊢\left(A:D⟶E\wedge B:C⟶D\right)\to AFnD$$
9		dffn5	$$⊢AFnD\leftrightarrow 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)$$