f1ocof1ob2

Description: If the range of F equals the domain of G , then the composition ( G o. F ) is bijective iff F and G are both bijective. Symmetric version of f1ocof1ob including the fact that F is a surjection onto its range. (Contributed by GL and AV, 20-Sep-2024) (Proof shortened by AV, 7-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		f1ocof1ob	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to ((G \circ F) : A \underset{1-1 onto}{⟶} D \leftrightarrow (F : A \underset{1-1}{⟶} C \land G : C \underset{1-1 onto}{⟶} D))$
2		f1f1orn	$⊢ F : A \underset{1-1}{⟶} C \to F : A \underset{1-1 onto}{⟶} ran F$
3		f1oeq3	$⊢ ran F = C \to (F : A \underset{1-1 onto}{⟶} ran F \leftrightarrow F : A \underset{1-1 onto}{⟶} C)$
4	2 3	imbitrid	$⊢ ran F = C \to (F : A \underset{1-1}{⟶} C \to F : A \underset{1-1 onto}{⟶} C)$
5	4	3ad2ant3	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to (F : A \underset{1-1}{⟶} C \to F : A \underset{1-1 onto}{⟶} C)$
6		f1of1	$⊢ F : A \underset{1-1 onto}{⟶} C \to F : A \underset{1-1}{⟶} C$
7	5 6	impbid1	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to (F : A \underset{1-1}{⟶} C \leftrightarrow F : A \underset{1-1 onto}{⟶} C)$
8	7	anbi1d	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to ((F : A \underset{1-1}{⟶} C \land G : C \underset{1-1 onto}{⟶} D) \leftrightarrow (F : A \underset{1-1 onto}{⟶} C \land G : C \underset{1-1 onto}{⟶} D))$
9	1 8	bitrd	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to ((G \circ F) : A \underset{1-1 onto}{⟶} D \leftrightarrow (F : A \underset{1-1 onto}{⟶} C \land G : C \underset{1-1 onto}{⟶} D))$

Metamath Proof Explorer

Theorem f1ocof1ob2

Proof