This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1co

Description: Composition of one-to-one functions when the codomain of the first matches the domain of the second. Exercise 30 of TakeutiZaring p. 25. (Contributed by NM, 28-May-1998) (Proof shortened by AV, 20-Sep-2024)

		Ref	Expression
	Assertion	f1co	$⊢ (F : B \underset{1-1}{⟶} C \land G : A \underset{1-1}{⟶} B) \to (F \circ G) : A \underset{1-1}{⟶} C$

Proof

Step	Hyp	Ref	Expression
1		f1cof1	$⊢ (F : B \underset{1-1}{⟶} C \land G : A \underset{1-1}{⟶} B) \to (F \circ G) : G^{-1} [B] \underset{1-1}{⟶} C$
2		f1f	$⊢ G : A \underset{1-1}{⟶} B \to G : A ⟶ B$
3		fimacnv	$⊢ G : A ⟶ B \to G^{-1} [B] = A$
4	2 3	syl	$⊢ G : A \underset{1-1}{⟶} B \to G^{-1} [B] = A$
5	4	adantl	$⊢ (F : B \underset{1-1}{⟶} C \land G : A \underset{1-1}{⟶} B) \to G^{-1} [B] = A$
6	5	eqcomd	$⊢ (F : B \underset{1-1}{⟶} C \land G : A \underset{1-1}{⟶} B) \to A = G^{-1} [B]$
7		f1eq2	$⊢ A = G^{-1} [B] \to ((F \circ G) : A \underset{1-1}{⟶} C \leftrightarrow (F \circ G) : G^{-1} [B] \underset{1-1}{⟶} C)$
8	6 7	syl	$⊢ (F : B \underset{1-1}{⟶} C \land G : A \underset{1-1}{⟶} B) \to ((F \circ G) : A \underset{1-1}{⟶} C \leftrightarrow (F \circ G) : G^{-1} [B] \underset{1-1}{⟶} C)$
9	1 8	mpbird	$⊢ (F : B \underset{1-1}{⟶} C \land G : A \underset{1-1}{⟶} B) \to (F \circ G) : A \underset{1-1}{⟶} C$