Metamath Proof Explorer

Theorem fncofn

Description: Composition of a function with domain and a function as a function with domain. Generalization of fnco . (Contributed by AV, 17-Sep-2024)

		Ref	Expression
	Assertion	fncofn	$⊢ (F Fn A \land Fun G) \to (F \circ G) Fn G^{-1} [A]$

Proof

Step	Hyp	Ref	Expression
1		fnfun	$⊢ F Fn A \to Fun F$
2		funco	$⊢ (Fun F \land Fun G) \to Fun (F \circ G)$
3	1 2	sylan	$⊢ (F Fn A \land Fun G) \to Fun (F \circ G)$
4	3	funfnd	$⊢ (F Fn A \land Fun G) \to (F \circ G) Fn dom (F \circ G)$
5		fndm	$⊢ F Fn A \to dom F = A$
6	5	adantr	$⊢ (F Fn A \land Fun G) \to dom F = A$
7	6	eqcomd	$⊢ (F Fn A \land Fun G) \to A = dom F$
8	7	imaeq2d	$⊢ (F Fn A \land Fun G) \to G^{-1} [A] = G^{-1} [dom F]$
9		dmco	$⊢ dom (F \circ G) = G^{-1} [dom F]$
10	8 9	eqtr4di	$⊢ (F Fn A \land Fun G) \to G^{-1} [A] = dom (F \circ G)$
11	10	fneq2d	$⊢ (F Fn A \land Fun G) \to ((F \circ G) Fn G^{-1} [A] \leftrightarrow (F \circ G) Fn dom (F \circ G))$
12	4 11	mpbird	$⊢ (F Fn A \land Fun G) \to (F \circ G) Fn G^{-1} [A]$