f1co

Description: Composition of one-to-one functions. Exercise 30 of TakeutiZaring p. 25. (Contributed by NM, 28-May-1998)

		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$

Step	Hyp	Ref	Expression
1		df-f1	$⊢ F : B \underset{1-1}{⟶} C \leftrightarrow (F : B ⟶ C \land Fun F^{-1})$
2		df-f1	$⊢ G : A \underset{1-1}{⟶} B \leftrightarrow (G : A ⟶ B \land Fun G^{-1})$
3		fco	$⊢ (F : B ⟶ C \land G : A ⟶ B) \to (F \circ G) : A ⟶ C$
4		funco	$⊢ (Fun G^{-1} \land Fun F^{-1}) \to Fun (G^{-1} \circ F^{-1})$
5		cnvco	$⊢ {(F \circ G)}^{-1} = G^{-1} \circ F^{-1}$
6	5	funeqi	$⊢ Fun {(F \circ G)}^{-1} \leftrightarrow Fun (G^{-1} \circ F^{-1})$
7	4 6	sylibr	$⊢ (Fun G^{-1} \land Fun F^{-1}) \to Fun {(F \circ G)}^{-1}$
8	7	ancoms	$⊢ (Fun F^{-1} \land Fun G^{-1}) \to Fun {(F \circ G)}^{-1}$
9	3 8	anim12i	$⊢ ((F : B ⟶ C \land G : A ⟶ B) \land (Fun F^{-1} \land Fun G^{-1})) \to ((F \circ G) : A ⟶ C \land Fun {(F \circ G)}^{-1})$
10	9	an4s	$⊢ ((F : B ⟶ C \land Fun F^{-1}) \land (G : A ⟶ B \land Fun G^{-1})) \to ((F \circ G) : A ⟶ C \land Fun {(F \circ G)}^{-1})$
11	1 2 10	syl2anb	$⊢ (F : B \underset{1-1}{⟶} C \land G : A \underset{1-1}{⟶} B) \to ((F \circ G) : A ⟶ C \land Fun {(F \circ G)}^{-1})$
12		df-f1	$⊢ (F \circ G) : A \underset{1-1}{⟶} C \leftrightarrow ((F \circ G) : A ⟶ C \land Fun {(F \circ G)}^{-1})$
13	11 12	sylibr	$⊢ (F : B \underset{1-1}{⟶} C \land G : A \underset{1-1}{⟶} B) \to (F \circ G) : A \underset{1-1}{⟶} C$

Metamath Proof Explorer