Metamath Proof Explorer

Theorem fncoOLD

Description: Obsolete version of fnco as of 20-Sep-2024. (Contributed by NM, 22-May-2006) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	fncoOLD	$⊢ (F Fn A \land G Fn B \land ran G \subseteq A) \to (F \circ G) Fn B$

Proof

Step	Hyp	Ref	Expression
1		fnfun	$⊢ F Fn A \to Fun F$
2		fnfun	$⊢ G Fn B \to Fun G$
3		funco	$⊢ (Fun F \land Fun G) \to Fun (F \circ G)$
4	1 2 3	syl2an	$⊢ (F Fn A \land G Fn B) \to Fun (F \circ G)$
5	4	3adant3	$⊢ (F Fn A \land G Fn B \land ran G \subseteq A) \to Fun (F \circ G)$
6		fndm	$⊢ F Fn A \to dom F = A$
7	6	sseq2d	$⊢ F Fn A \to (ran G \subseteq dom F \leftrightarrow ran G \subseteq A)$
8	7	biimpar	$⊢ (F Fn A \land ran G \subseteq A) \to ran G \subseteq dom F$
9		dmcosseq	$⊢ ran G \subseteq dom F \to dom (F \circ G) = dom G$
10	8 9	syl	$⊢ (F Fn A \land ran G \subseteq A) \to dom (F \circ G) = dom G$
11	10	3adant2	$⊢ (F Fn A \land G Fn B \land ran G \subseteq A) \to dom (F \circ G) = dom G$
12		fndm	$⊢ G Fn B \to dom G = B$
13	12	3ad2ant2	$⊢ (F Fn A \land G Fn B \land ran G \subseteq A) \to dom G = B$
14	11 13	eqtrd	$⊢ (F Fn A \land G Fn B \land ran G \subseteq A) \to dom (F \circ G) = B$
15		df-fn	$⊢ (F \circ G) Fn B \leftrightarrow (Fun (F \circ G) \land dom (F \circ G) = B)$
16	5 14 15	sylanbrc	$⊢ (F Fn A \land G Fn B \land ran G \subseteq A) \to (F \circ G) Fn B$