Theorem fcomptf

Description: Express composition of two functions as a maps-to applying both in sequence. This version has one less distinct variable restriction compared to fcompt . (Contributed by Thierry Arnoux, 30-Jun-2017)

	Ref	Expression
Hypothesis	fcomptf.1	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	fcomptf	$$⊢\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		fcomptf.1	$$⊢\underset{\_}{Ⅎ}xB$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}xD$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xE$$
5	2 3 4	nff	$$⊢ℲxA:D⟶E$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}xC$$
7	1 6 3	nff	$$⊢ℲxB:C⟶D$$
8	5 7	nfan	$$⊢Ⅎx\left(A:D⟶E\wedge B:C⟶D\right)$$
9		ffvelcdm	$$⊢\left(B:C⟶D\wedge x\in C\right)\to B\left(x\right)\in D$$
10	9	adantll	$$⊢\left(\left(A:D⟶E\wedge B:C⟶D\right)\wedge x\in C\right)\to B\left(x\right)\in D$$
11	10	ex	$$⊢\left(A:D⟶E\wedge B:C⟶D\right)\to \left(x\in C\to B\left(x\right)\in D\right)$$
12	8 11	ralrimi	$$⊢\left(A:D⟶E\wedge B:C⟶D\right)\to \forall x\in CB\left(x\right)\in D$$
13		ffn	$$⊢B:C⟶D\to BFnC$$
14	13	adantl	$$⊢\left(A:D⟶E\wedge B:C⟶D\right)\to BFnC$$
15	1	dffn5f	$$⊢BFnC\leftrightarrow B=\left(x\in C⟼B\left(x\right)\right)$$
16	14 15	sylib	$$⊢\left(A:D⟶E\wedge B:C⟶D\right)\to B=\left(x\in C⟼B\left(x\right)\right)$$
17		ffn	$$⊢A:D⟶E\to AFnD$$
18	17	adantr	$$⊢\left(A:D⟶E\wedge B:C⟶D\right)\to AFnD$$
19		dffn5	$$⊢AFnD\leftrightarrow A=\left(y\in D⟼A\left(y\right)\right)$$
20	18 19	sylib	$$⊢\left(A:D⟶E\wedge B:C⟶D\right)\to A=\left(y\in D⟼A\left(y\right)\right)$$
21		fveq2	$$⊢y=B\left(x\right)\to A\left(y\right)=A\left(B\left(x\right)\right)$$
22	12 16 20 21	fmptcof	$$⊢\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)$$