focofo

Description: Composition of onto functions. Generalisation of foco . (Contributed by AV, 29-Sep-2024)

		Ref	Expression
	Assertion	focofo	$⊢ (F : A \underset{onto}{⟶} B \land Fun G \land A \subseteq ran G) \to (F \circ G) : G^{-1} [A] \underset{onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		fof	$⊢ F : A \underset{onto}{⟶} B \to F : A ⟶ B$
2		fcof	$⊢ (F : A ⟶ B \land Fun G) \to (F \circ G) : G^{-1} [A] ⟶ B$
3	1 2	sylan	$⊢ (F : A \underset{onto}{⟶} B \land Fun G) \to (F \circ G) : G^{-1} [A] ⟶ B$
4	3	3adant3	$⊢ (F : A \underset{onto}{⟶} B \land Fun G \land A \subseteq ran G) \to (F \circ G) : G^{-1} [A] ⟶ B$
5		rnco	$⊢ ran (F \circ G) = ran ({F ↾}_{ran G})$
6	1	freld	$⊢ F : A \underset{onto}{⟶} B \to Rel F$
7	6	3ad2ant1	$⊢ (F : A \underset{onto}{⟶} B \land Fun G \land A \subseteq ran G) \to Rel F$
8		fdm	$⊢ F : A ⟶ B \to dom F = A$
9	8	eqcomd	$⊢ F : A ⟶ B \to A = dom F$
10	1 9	syl	$⊢ F : A \underset{onto}{⟶} B \to A = dom F$
11	10	sseq1d	$⊢ F : A \underset{onto}{⟶} B \to (A \subseteq ran G \leftrightarrow dom F \subseteq ran G)$
12	11	biimpa	$⊢ (F : A \underset{onto}{⟶} B \land A \subseteq ran G) \to dom F \subseteq ran G$
13		relssres	$⊢ (Rel F \land dom F \subseteq ran G) \to {F ↾}_{ran G} = F$
14	13	rneqd	$⊢ (Rel F \land dom F \subseteq ran G) \to ran ({F ↾}_{ran G}) = ran F$
15	7 12 14	3imp3i2an	$⊢ (F : A \underset{onto}{⟶} B \land Fun G \land A \subseteq ran G) \to ran ({F ↾}_{ran G}) = ran F$
16		forn	$⊢ F : A \underset{onto}{⟶} B \to ran F = B$
17	16	3ad2ant1	$⊢ (F : A \underset{onto}{⟶} B \land Fun G \land A \subseteq ran G) \to ran F = B$
18	15 17	eqtrd	$⊢ (F : A \underset{onto}{⟶} B \land Fun G \land A \subseteq ran G) \to ran ({F ↾}_{ran G}) = B$
19	5 18	eqtrid	$⊢ (F : A \underset{onto}{⟶} B \land Fun G \land A \subseteq ran G) \to ran (F \circ G) = B$
20		dffo2	$⊢ (F \circ G) : G^{-1} [A] \underset{onto}{⟶} B \leftrightarrow ((F \circ G) : G^{-1} [A] ⟶ B \land ran (F \circ G) = B)$
21	4 19 20	sylanbrc	$⊢ (F : A \underset{onto}{⟶} B \land Fun G \land A \subseteq ran G) \to (F \circ G) : G^{-1} [A] \underset{onto}{⟶} B$

Metamath Proof Explorer

Theorem focofo

Proof