f1cof1b

Description: If the range of F equals the domain of G , then the composition ( G o. F ) is injective iff F and G are both injective. (Contributed by GL and AV, 19-Sep-2024)

		Ref	Expression
	Assertion	f1cof1b	$⊢ (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}{⟶} B \land G : C \underset{1-1}{⟶} D))$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to F : A ⟶ B$
2		eqid	$⊢ ran F \cap C = ran F \cap C$
3		eqid	$⊢ F^{-1} [C] = F^{-1} [C]$
4		eqid	$⊢ {F ↾}_{F^{-1} [C]} = {F ↾}_{F^{-1} [C]}$
5		simp2	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to G : C ⟶ D$
6		eqid	$⊢ {G ↾}_{(ran F \cap C)} = {G ↾}_{(ran F \cap C)}$
7		simp3	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to ran F = C$
8	1 2 3 4 5 6 7	f1cof1blem	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to ((F^{-1} [C] = A \land ran F \cap C = C) \land ({F ↾}_{F^{-1} [C]} = F \land {G ↾}_{(ran F \cap C)} = G))$
9		simpll	$⊢ ((F^{-1} [C] = A \land ran F \cap C = C) \land ({F ↾}_{F^{-1} [C]} = F \land {G ↾}_{(ran F \cap C)} = G)) \to F^{-1} [C] = A$
10		f1eq2	$⊢ F^{-1} [C] = A \to ((G \circ F) : F^{-1} [C] \underset{1-1}{⟶} D \leftrightarrow (G \circ F) : A \underset{1-1}{⟶} D)$
11	8 9 10	3syl	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to ((G \circ F) : F^{-1} [C] \underset{1-1}{⟶} D \leftrightarrow (G \circ F) : A \underset{1-1}{⟶} D)$
12	11	bicomd	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to ((G \circ F) : A \underset{1-1}{⟶} D \leftrightarrow (G \circ F) : F^{-1} [C] \underset{1-1}{⟶} D)$
13		ancom	$⊢ ({G ↾}_{(ran F \cap C)} = G \land {F ↾}_{F^{-1} [C]} = F) \leftrightarrow ({F ↾}_{F^{-1} [C]} = F \land {G ↾}_{(ran F \cap C)} = G)$
14	13	anbi2i	$⊢ ((F^{-1} [C] = A \land ran F \cap C = C) \land ({G ↾}_{(ran F \cap C)} = G \land {F ↾}_{F^{-1} [C]} = F)) \leftrightarrow ((F^{-1} [C] = A \land ran F \cap C = C) \land ({F ↾}_{F^{-1} [C]} = F \land {G ↾}_{(ran F \cap C)} = G))$
15	8 14	sylibr	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to ((F^{-1} [C] = A \land ran F \cap C = C) \land ({G ↾}_{(ran F \cap C)} = G \land {F ↾}_{F^{-1} [C]} = F))$
16	15	adantr	$⊢ ((F : A ⟶ B \land G : C ⟶ D \land ran F = C) \land (G \circ F) : F^{-1} [C] \underset{1-1}{⟶} D) \to ((F^{-1} [C] = A \land ran F \cap C = C) \land ({G ↾}_{(ran F \cap C)} = G \land {F ↾}_{F^{-1} [C]} = F))$
17	1	adantr	$⊢ ((F : A ⟶ B \land G : C ⟶ D \land ran F = C) \land (G \circ F) : F^{-1} [C] \underset{1-1}{⟶} D) \to F : A ⟶ B$
18	5	adantr	$⊢ ((F : A ⟶ B \land G : C ⟶ D \land ran F = C) \land (G \circ F) : F^{-1} [C] \underset{1-1}{⟶} D) \to G : C ⟶ D$
19		simpr	$⊢ ((F : A ⟶ B \land G : C ⟶ D \land ran F = C) \land (G \circ F) : F^{-1} [C] \underset{1-1}{⟶} D) \to (G \circ F) : F^{-1} [C] \underset{1-1}{⟶} D$
20	17 2 3 4 18 6 19	fcoresf1	$⊢ ((F : A ⟶ B \land G : C ⟶ D \land ran F = C) \land (G \circ F) : F^{-1} [C] \underset{1-1}{⟶} D) \to (({F ↾}_{F^{-1} [C]}) : F^{-1} [C] \underset{1-1}{⟶} ran F \cap C \land ({G ↾}_{(ran F \cap C)}) : ran F \cap C \underset{1-1}{⟶} D)$
21	20	ancomd	$⊢ ((F : A ⟶ B \land G : C ⟶ D \land ran F = C) \land (G \circ F) : F^{-1} [C] \underset{1-1}{⟶} D) \to (({G ↾}_{(ran F \cap C)}) : ran F \cap C \underset{1-1}{⟶} D \land ({F ↾}_{F^{-1} [C]}) : F^{-1} [C] \underset{1-1}{⟶} ran F \cap C)$
22		simprl	$⊢ ((F^{-1} [C] = A \land ran F \cap C = C) \land ({G ↾}_{(ran F \cap C)} = G \land {F ↾}_{F^{-1} [C]} = F)) \to {G ↾}_{(ran F \cap C)} = G$
23		simpr	$⊢ (F^{-1} [C] = A \land ran F \cap C = C) \to ran F \cap C = C$
24	23	adantr	$⊢ ((F^{-1} [C] = A \land ran F \cap C = C) \land ({G ↾}_{(ran F \cap C)} = G \land {F ↾}_{F^{-1} [C]} = F)) \to ran F \cap C = C$
25		eqidd	$⊢ ((F^{-1} [C] = A \land ran F \cap C = C) \land ({G ↾}_{(ran F \cap C)} = G \land {F ↾}_{F^{-1} [C]} = F)) \to D = D$
26	22 24 25	f1eq123d	$⊢ ((F^{-1} [C] = A \land ran F \cap C = C) \land ({G ↾}_{(ran F \cap C)} = G \land {F ↾}_{F^{-1} [C]} = F)) \to (({G ↾}_{(ran F \cap C)}) : ran F \cap C \underset{1-1}{⟶} D \leftrightarrow G : C \underset{1-1}{⟶} D)$
27	26	biimpd	$⊢ ((F^{-1} [C] = A \land ran F \cap C = C) \land ({G ↾}_{(ran F \cap C)} = G \land {F ↾}_{F^{-1} [C]} = F)) \to (({G ↾}_{(ran F \cap C)}) : ran F \cap C \underset{1-1}{⟶} D \to G : C \underset{1-1}{⟶} D)$
28		simprr	$⊢ ((F^{-1} [C] = A \land ran F \cap C = C) \land ({G ↾}_{(ran F \cap C)} = G \land {F ↾}_{F^{-1} [C]} = F)) \to {F ↾}_{F^{-1} [C]} = F$
29		simpll	$⊢ ((F^{-1} [C] = A \land ran F \cap C = C) \land ({G ↾}_{(ran F \cap C)} = G \land {F ↾}_{F^{-1} [C]} = F)) \to F^{-1} [C] = A$
30	28 29 24	f1eq123d	$⊢ ((F^{-1} [C] = A \land ran F \cap C = C) \land ({G ↾}_{(ran F \cap C)} = G \land {F ↾}_{F^{-1} [C]} = F)) \to (({F ↾}_{F^{-1} [C]}) : F^{-1} [C] \underset{1-1}{⟶} ran F \cap C \leftrightarrow F : A \underset{1-1}{⟶} C)$
31	30	biimpd	$⊢ ((F^{-1} [C] = A \land ran F \cap C = C) \land ({G ↾}_{(ran F \cap C)} = G \land {F ↾}_{F^{-1} [C]} = F)) \to (({F ↾}_{F^{-1} [C]}) : F^{-1} [C] \underset{1-1}{⟶} ran F \cap C \to F : A \underset{1-1}{⟶} C)$
32	27 31	anim12d	$⊢ ((F^{-1} [C] = A \land ran F \cap C = C) \land ({G ↾}_{(ran F \cap C)} = G \land {F ↾}_{F^{-1} [C]} = F)) \to ((({G ↾}_{(ran F \cap C)}) : ran F \cap C \underset{1-1}{⟶} D \land ({F ↾}_{F^{-1} [C]}) : F^{-1} [C] \underset{1-1}{⟶} ran F \cap C) \to (G : C \underset{1-1}{⟶} D \land F : A \underset{1-1}{⟶} C))$
33	16 21 32	sylc	$⊢ ((F : A ⟶ B \land G : C ⟶ D \land ran F = C) \land (G \circ F) : F^{-1} [C] \underset{1-1}{⟶} D) \to (G : C \underset{1-1}{⟶} D \land F : A \underset{1-1}{⟶} C)$
34	12 33	sylbida	$⊢ ((F : A ⟶ B \land G : C ⟶ D \land ran F = C) \land (G \circ F) : A \underset{1-1}{⟶} D) \to (G : C \underset{1-1}{⟶} D \land F : A \underset{1-1}{⟶} C)$
35		ffrn	$⊢ F : A ⟶ B \to F : A ⟶ ran F$
36		ax-1	$⊢ F : A ⟶ B \to (F : A ⟶ ran F \to F : A ⟶ B)$
37	35 36	impbid2	$⊢ F : A ⟶ B \to (F : A ⟶ B \leftrightarrow F : A ⟶ ran F)$
38	37	anbi1d	$⊢ F : A ⟶ B \to ((F : A ⟶ B \land Fun F^{-1}) \leftrightarrow (F : A ⟶ ran F \land Fun F^{-1}))$
39		df-f1	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land Fun F^{-1})$
40		df-f1	$⊢ F : A \underset{1-1}{⟶} ran F \leftrightarrow (F : A ⟶ ran F \land Fun F^{-1})$
41	38 39 40	3bitr4g	$⊢ F : A ⟶ B \to (F : A \underset{1-1}{⟶} B \leftrightarrow F : A \underset{1-1}{⟶} ran F)$
42	41	3ad2ant1	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to (F : A \underset{1-1}{⟶} B \leftrightarrow F : A \underset{1-1}{⟶} ran F)$
43		f1eq3	$⊢ ran F = C \to (F : A \underset{1-1}{⟶} ran F \leftrightarrow F : A \underset{1-1}{⟶} C)$
44	43	3ad2ant3	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to (F : A \underset{1-1}{⟶} ran F \leftrightarrow F : A \underset{1-1}{⟶} C)$
45	42 44	bitrd	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to (F : A \underset{1-1}{⟶} B \leftrightarrow F : A \underset{1-1}{⟶} C)$
46	45	anbi2d	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to ((G : C \underset{1-1}{⟶} D \land F : A \underset{1-1}{⟶} B) \leftrightarrow (G : C \underset{1-1}{⟶} D \land F : A \underset{1-1}{⟶} C))$
47	46	adantr	$⊢ ((F : A ⟶ B \land G : C ⟶ D \land ran F = C) \land (G \circ F) : A \underset{1-1}{⟶} D) \to ((G : C \underset{1-1}{⟶} D \land F : A \underset{1-1}{⟶} B) \leftrightarrow (G : C \underset{1-1}{⟶} D \land F : A \underset{1-1}{⟶} C))$
48	34 47	mpbird	$⊢ ((F : A ⟶ B \land G : C ⟶ D \land ran F = C) \land (G \circ F) : A \underset{1-1}{⟶} D) \to (G : C \underset{1-1}{⟶} D \land F : A \underset{1-1}{⟶} B)$
49	48	ancomd	$⊢ ((F : A ⟶ B \land G : C ⟶ D \land ran F = C) \land (G \circ F) : A \underset{1-1}{⟶} D) \to (F : A \underset{1-1}{⟶} B \land G : C \underset{1-1}{⟶} D)$
50	49	ex	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to ((G \circ F) : A \underset{1-1}{⟶} D \to (F : A \underset{1-1}{⟶} B \land G : C \underset{1-1}{⟶} D))$
51		f1cof1	$⊢ (G : C \underset{1-1}{⟶} D \land F : A \underset{1-1}{⟶} B) \to (G \circ F) : F^{-1} [C] \underset{1-1}{⟶} D$
52	51	ancoms	$⊢ (F : A \underset{1-1}{⟶} B \land G : C \underset{1-1}{⟶} D) \to (G \circ F) : F^{-1} [C] \underset{1-1}{⟶} D$
53		imaeq2	$⊢ C = ran F \to F^{-1} [C] = F^{-1} [ran F]$
54		cnvimarndm	$⊢ F^{-1} [ran F] = dom F$
55	53 54	eqtrdi	$⊢ C = ran F \to F^{-1} [C] = dom F$
56	55	eqcoms	$⊢ ran F = C \to F^{-1} [C] = dom F$
57	56	3ad2ant3	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to F^{-1} [C] = dom F$
58	1	fdmd	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to dom F = A$
59	57 58	eqtrd	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to F^{-1} [C] = A$
60	59 10	syl	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to ((G \circ F) : F^{-1} [C] \underset{1-1}{⟶} D \leftrightarrow (G \circ F) : A \underset{1-1}{⟶} D)$
61	52 60	syl5ib	$⊢ (F : A ⟶ B \land G : C ⟶ D \land ran F = C) \to ((F : A \underset{1-1}{⟶} B \land G : C \underset{1-1}{⟶} D) \to (G \circ F) : A \underset{1-1}{⟶} D)$
62	50 61	impbid	$⊢ (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}{⟶} B \land G : C \underset{1-1}{⟶} D))$

Metamath Proof Explorer

Theorem f1cof1b

Proof