Metamath Proof Explorer

Theorem fnco

Description: Composition of two functions with domains as a function with domain. (Contributed by NM, 22-May-2006) (Proof shortened by AV, 20-Sep-2024)

		Ref	Expression
	Assertion	fnco	$⊢ (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	$⊢ G Fn B \to Fun G$
2		fncofn	$⊢ (F Fn A \land Fun G) \to (F \circ G) Fn G^{-1} [A]$
3	1 2	sylan2	$⊢ (F Fn A \land G Fn B) \to (F \circ G) Fn G^{-1} [A]$
4	3	3adant3	$⊢ (F Fn A \land G Fn B \land ran G \subseteq A) \to (F \circ G) Fn G^{-1} [A]$
5		cnvimassrndm	$⊢ ran G \subseteq A \to G^{-1} [A] = dom G$
6	5	3ad2ant3	$⊢ (F Fn A \land G Fn B \land ran G \subseteq A) \to G^{-1} [A] = dom G$
7		fndm	$⊢ G Fn B \to dom G = B$
8	7	3ad2ant2	$⊢ (F Fn A \land G Fn B \land ran G \subseteq A) \to dom G = B$
9	6 8	eqtr2d	$⊢ (F Fn A \land G Fn B \land ran G \subseteq A) \to B = G^{-1} [A]$
10	9	fneq2d	$⊢ (F Fn A \land G Fn B \land ran G \subseteq A) \to ((F \circ G) Fn B \leftrightarrow (F \circ G) Fn G^{-1} [A])$
11	4 10	mpbird	$⊢ (F Fn A \land G Fn B \land ran G \subseteq A) \to (F \circ G) Fn B$