fnresfnco

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

		Ref	Expression
	Assertion	fnresfnco	$⊢ (({F ↾}_{ran G}) Fn ran G \land G Fn B) \to (F \circ G) Fn B$

Step	Hyp	Ref	Expression
1		fnfun	$⊢ ({F ↾}_{ran G}) Fn ran G \to Fun ({F ↾}_{ran G})$
2		fnfun	$⊢ G Fn B \to Fun G$
3		funresfunco	$⊢ (Fun ({F ↾}_{ran G}) \land Fun G) \to Fun (F \circ G)$
4	1 2 3	syl2an	$⊢ (({F ↾}_{ran G}) Fn ran G \land G Fn B) \to Fun (F \circ G)$
5		fndm	$⊢ ({F ↾}_{ran G}) Fn ran G \to dom ({F ↾}_{ran G}) = ran G$
6		dmres	$⊢ dom ({F ↾}_{ran G}) = ran G \cap dom F$
7	6	eqeq1i	$⊢ dom ({F ↾}_{ran G}) = ran G \leftrightarrow ran G \cap dom F = ran G$
8		dfss2	$⊢ ran G \subseteq dom F \leftrightarrow ran G \cap dom F = ran G$
9	7 8	sylbb2	$⊢ dom ({F ↾}_{ran G}) = ran G \to ran G \subseteq dom F$
10	5 9	syl	$⊢ ({F ↾}_{ran G}) Fn ran G \to ran G \subseteq dom F$
11	10	adantr	$⊢ (({F ↾}_{ran G}) Fn ran G \land G Fn B) \to ran G \subseteq dom F$
12		dmcosseq	$⊢ ran G \subseteq dom F \to dom (F \circ G) = dom G$
13	11 12	syl	$⊢ (({F ↾}_{ran G}) Fn ran G \land G Fn B) \to dom (F \circ G) = dom G$
14		fndm	$⊢ G Fn B \to dom G = B$
15	14	adantl	$⊢ (({F ↾}_{ran G}) Fn ran G \land G Fn B) \to dom G = B$
16	13 15	eqtrd	$⊢ (({F ↾}_{ran G}) Fn ran G \land G Fn B) \to dom (F \circ G) = B$
17		df-fn	$⊢ (F \circ G) Fn B \leftrightarrow (Fun (F \circ G) \land dom (F \circ G) = B)$
18	4 16 17	sylanbrc	$⊢ (({F ↾}_{ran G}) Fn ran G \land G Fn B) \to (F \circ G) Fn B$

Metamath Proof Explorer