fco

Description: Composition of two functions with domain and codomain as a function with domain and codomain. (Contributed by NM, 29-Aug-1999) (Proof shortened by Andrew Salmon, 17-Sep-2011) (Proof shortened by AV, 20-Sep-2024)

		Ref	Expression
	Assertion	fco	$⊢ (F : B ⟶ C \land G : A ⟶ B) \to (F \circ G) : A ⟶ C$

Proof

Step	Hyp	Ref	Expression
1		ffun	$⊢ G : A ⟶ B \to Fun G$
2		fcof	$⊢ (F : B ⟶ C \land Fun G) \to (F \circ G) : G^{-1} [B] ⟶ C$
3	1 2	sylan2	$⊢ (F : B ⟶ C \land G : A ⟶ B) \to (F \circ G) : G^{-1} [B] ⟶ C$
4		fimacnv	$⊢ G : A ⟶ B \to G^{-1} [B] = A$
5	4	eqcomd	$⊢ G : A ⟶ B \to A = G^{-1} [B]$
6	5	adantl	$⊢ (F : B ⟶ C \land G : A ⟶ B) \to A = G^{-1} [B]$
7	6	feq2d	$⊢ (F : B ⟶ C \land G : A ⟶ B) \to ((F \circ G) : A ⟶ C \leftrightarrow (F \circ G) : G^{-1} [B] ⟶ C)$
8	3 7	mpbird	$⊢ (F : B ⟶ C \land G : A ⟶ B) \to (F \circ G) : A ⟶ C$

Metamath Proof Explorer

Theorem fco

Proof