Metamath Proof Explorer

Theorem funcofd

Description: Composition of two functions as a function with domain and codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021) (Proof shortened by AV, 20-Sep-2024)

	Ref	Expression
Hypotheses	funcofd.1	$⊢ φ \to Fun F$
	funcofd.2	$⊢ φ \to Fun G$
Assertion	funcofd	$⊢ φ \to (F \circ G) : G^{-1} [dom F] ⟶ ran F$

Proof

Step	Hyp	Ref	Expression
1		funcofd.1	$⊢ φ \to Fun F$
2		funcofd.2	$⊢ φ \to Fun G$
3		fdmrn	$⊢ Fun F \leftrightarrow F : dom F ⟶ ran F$
4	1 3	sylib	$⊢ φ \to F : dom F ⟶ ran F$
5		fcof	$⊢ (F : dom F ⟶ ran F \land Fun G) \to (F \circ G) : G^{-1} [dom F] ⟶ ran F$
6	4 2 5	syl2anc	$⊢ φ \to (F \circ G) : G^{-1} [dom F] ⟶ ran F$