Metamath Proof Explorer

Theorem fnfocofob

Description: If the domain of a function G equals the range of a function F , then the composition ( G o. F ) is surjective iff G is surjective. (Contributed by GL and AV, 29-Sep-2024)

		Ref	Expression
	Assertion	fnfocofob	$⊢ (F Fn A \land G : B ⟶ C \land ran F = B) \to ((G \circ F) : A \underset{onto}{⟶} C \leftrightarrow G : B \underset{onto}{⟶} C)$

Proof

Step	Hyp	Ref	Expression
1		cnvimarndm	$⊢ F^{-1} [ran F] = dom F$
2		fndm	$⊢ F Fn A \to dom F = A$
3	2	3ad2ant1	$⊢ (F Fn A \land G : B ⟶ C \land ran F = B) \to dom F = A$
4	1 3	eqtr2id	$⊢ (F Fn A \land G : B ⟶ C \land ran F = B) \to A = F^{-1} [ran F]$
5		imaeq2	$⊢ ran F = B \to F^{-1} [ran F] = F^{-1} [B]$
6	5	3ad2ant3	$⊢ (F Fn A \land G : B ⟶ C \land ran F = B) \to F^{-1} [ran F] = F^{-1} [B]$
7	4 6	eqtrd	$⊢ (F Fn A \land G : B ⟶ C \land ran F = B) \to A = F^{-1} [B]$
8		foeq2	$⊢ A = F^{-1} [B] \to ((G \circ F) : A \underset{onto}{⟶} C \leftrightarrow (G \circ F) : F^{-1} [B] \underset{onto}{⟶} C)$
9	7 8	syl	$⊢ (F Fn A \land G : B ⟶ C \land ran F = B) \to ((G \circ F) : A \underset{onto}{⟶} C \leftrightarrow (G \circ F) : F^{-1} [B] \underset{onto}{⟶} C)$
10		fnfun	$⊢ F Fn A \to Fun F$
11		id	$⊢ G : B ⟶ C \to G : B ⟶ C$
12		eqimss2	$⊢ ran F = B \to B \subseteq ran F$
13		funfocofob	$⊢ (Fun F \land G : B ⟶ C \land B \subseteq ran F) \to ((G \circ F) : F^{-1} [B] \underset{onto}{⟶} C \leftrightarrow G : B \underset{onto}{⟶} C)$
14	10 11 12 13	syl3an	$⊢ (F Fn A \land G : B ⟶ C \land ran F = B) \to ((G \circ F) : F^{-1} [B] \underset{onto}{⟶} C \leftrightarrow G : B \underset{onto}{⟶} C)$
15	9 14	bitrd	$⊢ (F Fn A \land G : B ⟶ C \land ran F = B) \to ((G \circ F) : A \underset{onto}{⟶} C \leftrightarrow G : B \underset{onto}{⟶} C)$