Metamath Proof Explorer

Theorem fcof

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

		Ref	Expression
	Assertion	fcof	$⊢ (F : A ⟶ B \land Fun G) \to (F \circ G) : G^{-1} [A] ⟶ B$

Proof

Step	Hyp	Ref	Expression
1		df-f	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B)$
2		fncofn	$⊢ (F Fn A \land Fun G) \to (F \circ G) Fn G^{-1} [A]$
3	2	ex	$⊢ F Fn A \to (Fun G \to (F \circ G) Fn G^{-1} [A])$
4	3	adantr	$⊢ (F Fn A \land ran F \subseteq B) \to (Fun G \to (F \circ G) Fn G^{-1} [A])$
5		rncoss	$⊢ ran (F \circ G) \subseteq ran F$
6		sstr	$⊢ (ran (F \circ G) \subseteq ran F \land ran F \subseteq B) \to ran (F \circ G) \subseteq B$
7	5 6	mpan	$⊢ ran F \subseteq B \to ran (F \circ G) \subseteq B$
8	7	adantl	$⊢ (F Fn A \land ran F \subseteq B) \to ran (F \circ G) \subseteq B$
9	4 8	jctird	$⊢ (F Fn A \land ran F \subseteq B) \to (Fun G \to ((F \circ G) Fn G^{-1} [A] \land ran (F \circ G) \subseteq B))$
10	9	imp	$⊢ ((F Fn A \land ran F \subseteq B) \land Fun G) \to ((F \circ G) Fn G^{-1} [A] \land ran (F \circ G) \subseteq B)$
11	1 10	sylanb	$⊢ (F : A ⟶ B \land Fun G) \to ((F \circ G) Fn G^{-1} [A] \land ran (F \circ G) \subseteq B)$
12		df-f	$⊢ (F \circ G) : G^{-1} [A] ⟶ B \leftrightarrow ((F \circ G) Fn G^{-1} [A] \land ran (F \circ G) \subseteq B)$
13	11 12	sylibr	$⊢ (F : A ⟶ B \land Fun G) \to (F \circ G) : G^{-1} [A] ⟶ B$