Theorem fcomptss

Description: Express composition of two functions as a maps-to applying both in sequence. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	fcomptss.a	$$⊢\phi \to F:A⟶B$$
	fcomptss.b	$$⊢\phi \to B\subseteq C$$
	fcomptss.g	$$⊢\phi \to G:C⟶D$$
Assertion	fcomptss	$$⊢\phi \to G\circ F=\left(x\in A⟼G\left(F\left(x\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fcomptss.a	$$⊢\phi \to F:A⟶B$$
2		fcomptss.b	$$⊢\phi \to B\subseteq C$$
3		fcomptss.g	$$⊢\phi \to G:C⟶D$$
4	1 2	fssd	$$⊢\phi \to F:A⟶C$$
5		fcompt	$$⊢\left(G:C⟶D\wedge F:A⟶C\right)\to G\circ F=\left(x\in A⟼G\left(F\left(x\right)\right)\right)$$
6	3 4 5	syl2anc	$$⊢\phi \to G\circ F=\left(x\in A⟼G\left(F\left(x\right)\right)\right)$$