Metamath Proof Explorer

Theorem f1ocof1ob

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. (Contributed by GL and AV, 7-Oct-2024)

		Ref	Expression
	Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		ffrn	$⊢ F : A ⟶ B \to F : A ⟶ ran F$
2	1	3ad2ant1	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to F : A ⟶ ran F$
3		feq3	$⊢ ran F = C \to (F : A ⟶ ran F \leftrightarrow F : A ⟶ C)$
4	3	3ad2ant3	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to (F : A ⟶ ran F \leftrightarrow F : A ⟶ C)$
5	2 4	mpbid	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to F : A ⟶ C$
6		f1cof1b	$⊢ (F : A ⟶ C \land G : C ⟶ D \land ran F = C) \to ((G \circ F) : A \underset{1-1}{⟶} D \leftrightarrow (F : A \underset{1-1}{⟶} C \land G : C \underset{1-1}{⟶} D))$
7	5 6	syld3an1	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to ((G \circ F) : A \underset{1-1}{⟶} D \leftrightarrow (F : A \underset{1-1}{⟶} C \land G : C \underset{1-1}{⟶} D))$
8		ffn	$⊢ F : A ⟶ B \to F Fn A$
9		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)$
10	8 9	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)$
11	7 10	anbi12d	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to (((G \circ F) : A \underset{1-1}{⟶} D \land (G \circ F) : A \underset{onto}{⟶} D) \leftrightarrow ((F : A \underset{1-1}{⟶} C \land G : C \underset{1-1}{⟶} D) \land G : C \underset{onto}{⟶} D))$
12		anass	$⊢ ((F : A \underset{1-1}{⟶} C \land G : C \underset{1-1}{⟶} D) \land G : C \underset{onto}{⟶} D) \leftrightarrow (F : A \underset{1-1}{⟶} C \land (G : C \underset{1-1}{⟶} D \land G : C \underset{onto}{⟶} D))$
13	11 12	bitrdi	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to (((G \circ F) : A \underset{1-1}{⟶} D \land (G \circ F) : A \underset{onto}{⟶} D) \leftrightarrow (F : A \underset{1-1}{⟶} C \land (G : C \underset{1-1}{⟶} D \land G : C \underset{onto}{⟶} D)))$
14		df-f1o	$⊢ (G \circ F) : A \underset{1-1 onto}{⟶} D \leftrightarrow ((G \circ F) : A \underset{1-1}{⟶} D \land (G \circ F) : A \underset{onto}{⟶} D)$
15		df-f1o	$⊢ G : C \underset{1-1 onto}{⟶} D \leftrightarrow (G : C \underset{1-1}{⟶} D \land G : C \underset{onto}{⟶} D)$
16	15	anbi2i	$⊢ (F : A \underset{1-1}{⟶} C \land G : C \underset{1-1 onto}{⟶} D) \leftrightarrow (F : A \underset{1-1}{⟶} C \land (G : C \underset{1-1}{⟶} D \land G : C \underset{onto}{⟶} D))$
17	13 14 16	3bitr4g	$⊢ (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))$