f1oco

Description: Composition of one-to-one onto functions. (Contributed by NM, 19-Mar-1998)

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

Step	Hyp	Ref	Expression
1		df-f1o	$⊢ F : B \underset{1-1 onto}{⟶} C \leftrightarrow (F : B \underset{1-1}{⟶} C \land F : B \underset{onto}{⟶} C)$
2		df-f1o	$⊢ G : A \underset{1-1 onto}{⟶} B \leftrightarrow (G : A \underset{1-1}{⟶} B \land G : A \underset{onto}{⟶} B)$
3		f1co	$⊢ (F : B \underset{1-1}{⟶} C \land G : A \underset{1-1}{⟶} B) \to (F \circ G) : A \underset{1-1}{⟶} C$
4		foco	$⊢ (F : B \underset{onto}{⟶} C \land G : A \underset{onto}{⟶} B) \to (F \circ G) : A \underset{onto}{⟶} C$
5	3 4	anim12i	$⊢ ((F : B \underset{1-1}{⟶} C \land G : A \underset{1-1}{⟶} B) \land (F : B \underset{onto}{⟶} C \land G : A \underset{onto}{⟶} B)) \to ((F \circ G) : A \underset{1-1}{⟶} C \land (F \circ G) : A \underset{onto}{⟶} C)$
6	5	an4s	$⊢ ((F : B \underset{1-1}{⟶} C \land F : B \underset{onto}{⟶} C) \land (G : A \underset{1-1}{⟶} B \land G : A \underset{onto}{⟶} B)) \to ((F \circ G) : A \underset{1-1}{⟶} C \land (F \circ G) : A \underset{onto}{⟶} C)$
7	1 2 6	syl2anb	$⊢ (F : B \underset{1-1 onto}{⟶} C \land G : A \underset{1-1 onto}{⟶} B) \to ((F \circ G) : A \underset{1-1}{⟶} C \land (F \circ G) : A \underset{onto}{⟶} C)$
8		df-f1o	$⊢ (F \circ G) : A \underset{1-1 onto}{⟶} C \leftrightarrow ((F \circ G) : A \underset{1-1}{⟶} C \land (F \circ G) : A \underset{onto}{⟶} C)$
9	7 8	sylibr	$⊢ (F : B \underset{1-1 onto}{⟶} C \land G : A \underset{1-1 onto}{⟶} B) \to (F \circ G) : A \underset{1-1 onto}{⟶} C$

Metamath Proof Explorer