focofob

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 and F as function to the domain of G are both surjective. Symmetric version of fnfocofob including the fact that F is a surjection onto its range. (Contributed by GL and AV, 20-Sep-2024) (Proof shortened by AV, 29-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		ffn	$⊢ F : A ⟶ B \to F Fn A$
2		fnfocofob	$⊢ (F Fn A \land G : C ⟶ D \land ran F = C) \to ((G \circ F) : A \underset{onto}{⟶} D \leftrightarrow G : C \underset{onto}{⟶} D)$
3	1 2	syl3an1	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to ((G \circ F) : A \underset{onto}{⟶} D \leftrightarrow G : C \underset{onto}{⟶} D)$
4		dffn4	$⊢ F Fn A \leftrightarrow F : A \underset{onto}{⟶} ran F$
5	1 4	sylib	$⊢ F : A ⟶ B \to F : A \underset{onto}{⟶} ran F$
6	5	3ad2ant1	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to F : A \underset{onto}{⟶} ran F$
7		foeq3	$⊢ ran F = C \to (F : A \underset{onto}{⟶} ran F \leftrightarrow F : A \underset{onto}{⟶} C)$
8	7	3ad2ant3	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to (F : A \underset{onto}{⟶} ran F \leftrightarrow F : A \underset{onto}{⟶} C)$
9	6 8	mpbid	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to F : A \underset{onto}{⟶} C$
10	9	biantrurd	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to (G : C \underset{onto}{⟶} D \leftrightarrow (F : A \underset{onto}{⟶} C \land G : C \underset{onto}{⟶} D))$
11	3 10	bitrd	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to ((G \circ F) : A \underset{onto}{⟶} D \leftrightarrow (F : A \underset{onto}{⟶} C \land G : C \underset{onto}{⟶} D))$

Metamath Proof Explorer

Theorem focofob

Proof