f1cof1

Description: Composition of two one-to-one functions. Generalization of f1co . (Contributed by AV, 18-Sep-2024)

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

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

Metamath Proof Explorer