foco

Description: Composition of onto functions. (Contributed by NM, 22-Mar-2006) (Proof shortened by AV, 29-Sep-2024)

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

Step	Hyp	Ref	Expression
1		simpl	$⊢ (F : B \underset{onto}{⟶} C \land G : A \underset{onto}{⟶} B) \to F : B \underset{onto}{⟶} C$
2		fofun	$⊢ G : A \underset{onto}{⟶} B \to Fun G$
3	2	adantl	$⊢ (F : B \underset{onto}{⟶} C \land G : A \underset{onto}{⟶} B) \to Fun G$
4		forn	$⊢ G : A \underset{onto}{⟶} B \to ran G = B$
5		eqimss2	$⊢ ran G = B \to B \subseteq ran G$
6	4 5	syl	$⊢ G : A \underset{onto}{⟶} B \to B \subseteq ran G$
7	6	adantl	$⊢ (F : B \underset{onto}{⟶} C \land G : A \underset{onto}{⟶} B) \to B \subseteq ran G$
8		focofo	$⊢ (F : B \underset{onto}{⟶} C \land Fun G \land B \subseteq ran G) \to (F \circ G) : G^{-1} [B] \underset{onto}{⟶} C$
9	1 3 7 8	syl3anc	$⊢ (F : B \underset{onto}{⟶} C \land G : A \underset{onto}{⟶} B) \to (F \circ G) : G^{-1} [B] \underset{onto}{⟶} C$
10		focnvimacdmdm	$⊢ G : A \underset{onto}{⟶} B \to G^{-1} [B] = A$
11	10	eqcomd	$⊢ G : A \underset{onto}{⟶} B \to A = G^{-1} [B]$
12	11	adantl	$⊢ (F : B \underset{onto}{⟶} C \land G : A \underset{onto}{⟶} B) \to A = G^{-1} [B]$
13		foeq2	$⊢ A = G^{-1} [B] \to ((F \circ G) : A \underset{onto}{⟶} C \leftrightarrow (F \circ G) : G^{-1} [B] \underset{onto}{⟶} C)$
14	12 13	syl	$⊢ (F : B \underset{onto}{⟶} C \land G : A \underset{onto}{⟶} B) \to ((F \circ G) : A \underset{onto}{⟶} C \leftrightarrow (F \circ G) : G^{-1} [B] \underset{onto}{⟶} C)$
15	9 14	mpbird	$⊢ (F : B \underset{onto}{⟶} C \land G : A \underset{onto}{⟶} B) \to (F \circ G) : A \underset{onto}{⟶} C$

Metamath Proof Explorer