cocan1

Description: An injection is left-cancelable. (Contributed by FL, 2-Aug-2009) (Revised by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	cocan1	$⊢ (F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \to (F \circ H = F \circ K \leftrightarrow H = K)$

Proof

Step	Hyp	Ref	Expression
1		fvco3	$⊢ (H : A ⟶ B \land x \in A) \to (F \circ H) (x) = F (H (x))$
2	1	3ad2antl2	$⊢ ((F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \land x \in A) \to (F \circ H) (x) = F (H (x))$
3		fvco3	$⊢ (K : A ⟶ B \land x \in A) \to (F \circ K) (x) = F (K (x))$
4	3	3ad2antl3	$⊢ ((F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \land x \in A) \to (F \circ K) (x) = F (K (x))$
5	2 4	eqeq12d	$⊢ ((F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \land x \in A) \to ((F \circ H) (x) = (F \circ K) (x) \leftrightarrow F (H (x)) = F (K (x)))$
6		simpl1	$⊢ ((F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \land x \in A) \to F : B \underset{1-1}{⟶} C$
7		ffvelcdm	$⊢ (H : A ⟶ B \land x \in A) \to H (x) \in B$
8	7	3ad2antl2	$⊢ ((F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \land x \in A) \to H (x) \in B$
9		ffvelcdm	$⊢ (K : A ⟶ B \land x \in A) \to K (x) \in B$
10	9	3ad2antl3	$⊢ ((F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \land x \in A) \to K (x) \in B$
11		f1fveq	$⊢ (F : B \underset{1-1}{⟶} C \land (H (x) \in B \land K (x) \in B)) \to (F (H (x)) = F (K (x)) \leftrightarrow H (x) = K (x))$
12	6 8 10 11	syl12anc	$⊢ ((F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \land x \in A) \to (F (H (x)) = F (K (x)) \leftrightarrow H (x) = K (x))$
13	5 12	bitrd	$⊢ ((F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \land x \in A) \to ((F \circ H) (x) = (F \circ K) (x) \leftrightarrow H (x) = K (x))$
14	13	ralbidva	$⊢ (F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \to (\forall x \in A (F \circ H) (x) = (F \circ K) (x) \leftrightarrow \forall x \in A H (x) = K (x))$
15		f1f	$⊢ F : B \underset{1-1}{⟶} C \to F : B ⟶ C$
16	15	3ad2ant1	$⊢ (F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \to F : B ⟶ C$
17	16	ffnd	$⊢ (F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \to F Fn B$
18		simp2	$⊢ (F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \to H : A ⟶ B$
19		fnfco	$⊢ (F Fn B \land H : A ⟶ B) \to (F \circ H) Fn A$
20	17 18 19	syl2anc	$⊢ (F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \to (F \circ H) Fn A$
21		simp3	$⊢ (F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \to K : A ⟶ B$
22		fnfco	$⊢ (F Fn B \land K : A ⟶ B) \to (F \circ K) Fn A$
23	17 21 22	syl2anc	$⊢ (F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \to (F \circ K) Fn A$
24		eqfnfv	$⊢ ((F \circ H) Fn A \land (F \circ K) Fn A) \to (F \circ H = F \circ K \leftrightarrow \forall x \in A (F \circ H) (x) = (F \circ K) (x))$
25	20 23 24	syl2anc	$⊢ (F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \to (F \circ H = F \circ K \leftrightarrow \forall x \in A (F \circ H) (x) = (F \circ K) (x))$
26	18	ffnd	$⊢ (F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \to H Fn A$
27	21	ffnd	$⊢ (F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \to K Fn A$
28		eqfnfv	$⊢ (H Fn A \land K Fn A) \to (H = K \leftrightarrow \forall x \in A H (x) = K (x))$
29	26 27 28	syl2anc	$⊢ (F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \to (H = K \leftrightarrow \forall x \in A H (x) = K (x))$
30	14 25 29	3bitr4d	$⊢ (F : B \underset{1-1}{⟶} C \land H : A ⟶ B \land K : A ⟶ B) \to (F \circ H = F \circ K \leftrightarrow H = K)$

Metamath Proof Explorer

Theorem cocan1

Proof