funresfunco

Description: Composition of two functions, generalization of funco . (Contributed by Alexander van der Vekens, 25-Jul-2017)

		Ref	Expression
	Assertion	funresfunco	$⊢ (Fun ({F ↾}_{ran G}) \land Fun G) \to Fun (F \circ G)$

Step	Hyp	Ref	Expression
1		funco	$⊢ (Fun ({F ↾}_{ran G}) \land Fun G) \to Fun (({F ↾}_{ran G}) \circ G)$
2		ssid	$⊢ ran G \subseteq ran G$
3		cores	$⊢ ran G \subseteq ran G \to ({F ↾}_{ran G}) \circ G = F \circ G$
4	2 3	ax-mp	$⊢ ({F ↾}_{ran G}) \circ G = F \circ G$
5	4	eqcomi	$⊢ F \circ G = ({F ↾}_{ran G}) \circ G$
6	5	funeqi	$⊢ Fun (F \circ G) \leftrightarrow Fun (({F ↾}_{ran G}) \circ G)$
7	1 6	sylibr	$⊢ (Fun ({F ↾}_{ran G}) \land Fun G) \to Fun (F \circ G)$

Metamath Proof Explorer