cocan2

Description: A surjection is right-cancelable. (Contributed by FL, 21-Nov-2011) (Proof shortened by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	cocan2	$⊢ (F : A \underset{onto}{⟶} B \land H Fn B \land K Fn B) \to (H \circ F = K \circ F \leftrightarrow H = K)$

Proof

Step	Hyp	Ref	Expression
1		fof	$⊢ F : A \underset{onto}{⟶} B \to F : A ⟶ B$
2	1	3ad2ant1	$⊢ (F : A \underset{onto}{⟶} B \land H Fn B \land K Fn B) \to F : A ⟶ B$
3		fvco3	$⊢ (F : A ⟶ B \land y \in A) \to (H \circ F) (y) = H (F (y))$
4	2 3	sylan	$⊢ ((F : A \underset{onto}{⟶} B \land H Fn B \land K Fn B) \land y \in A) \to (H \circ F) (y) = H (F (y))$
5		fvco3	$⊢ (F : A ⟶ B \land y \in A) \to (K \circ F) (y) = K (F (y))$
6	2 5	sylan	$⊢ ((F : A \underset{onto}{⟶} B \land H Fn B \land K Fn B) \land y \in A) \to (K \circ F) (y) = K (F (y))$
7	4 6	eqeq12d	$⊢ ((F : A \underset{onto}{⟶} B \land H Fn B \land K Fn B) \land y \in A) \to ((H \circ F) (y) = (K \circ F) (y) \leftrightarrow H (F (y)) = K (F (y)))$
8	7	ralbidva	$⊢ (F : A \underset{onto}{⟶} B \land H Fn B \land K Fn B) \to (\forall y \in A (H \circ F) (y) = (K \circ F) (y) \leftrightarrow \forall y \in A H (F (y)) = K (F (y)))$
9		fveq2	$⊢ F (y) = x \to H (F (y)) = H (x)$
10		fveq2	$⊢ F (y) = x \to K (F (y)) = K (x)$
11	9 10	eqeq12d	$⊢ F (y) = x \to (H (F (y)) = K (F (y)) \leftrightarrow H (x) = K (x))$
12	11	cbvfo	$⊢ F : A \underset{onto}{⟶} B \to (\forall y \in A H (F (y)) = K (F (y)) \leftrightarrow \forall x \in B H (x) = K (x))$
13	12	3ad2ant1	$⊢ (F : A \underset{onto}{⟶} B \land H Fn B \land K Fn B) \to (\forall y \in A H (F (y)) = K (F (y)) \leftrightarrow \forall x \in B H (x) = K (x))$
14	8 13	bitrd	$⊢ (F : A \underset{onto}{⟶} B \land H Fn B \land K Fn B) \to (\forall y \in A (H \circ F) (y) = (K \circ F) (y) \leftrightarrow \forall x \in B H (x) = K (x))$
15		simp2	$⊢ (F : A \underset{onto}{⟶} B \land H Fn B \land K Fn B) \to H Fn B$
16		fnfco	$⊢ (H Fn B \land F : A ⟶ B) \to (H \circ F) Fn A$
17	15 2 16	syl2anc	$⊢ (F : A \underset{onto}{⟶} B \land H Fn B \land K Fn B) \to (H \circ F) Fn A$
18		simp3	$⊢ (F : A \underset{onto}{⟶} B \land H Fn B \land K Fn B) \to K Fn B$
19		fnfco	$⊢ (K Fn B \land F : A ⟶ B) \to (K \circ F) Fn A$
20	18 2 19	syl2anc	$⊢ (F : A \underset{onto}{⟶} B \land H Fn B \land K Fn B) \to (K \circ F) Fn A$
21		eqfnfv	$⊢ ((H \circ F) Fn A \land (K \circ F) Fn A) \to (H \circ F = K \circ F \leftrightarrow \forall y \in A (H \circ F) (y) = (K \circ F) (y))$
22	17 20 21	syl2anc	$⊢ (F : A \underset{onto}{⟶} B \land H Fn B \land K Fn B) \to (H \circ F = K \circ F \leftrightarrow \forall y \in A (H \circ F) (y) = (K \circ F) (y))$
23		eqfnfv	$⊢ (H Fn B \land K Fn B) \to (H = K \leftrightarrow \forall x \in B H (x) = K (x))$
24	15 18 23	syl2anc	$⊢ (F : A \underset{onto}{⟶} B \land H Fn B \land K Fn B) \to (H = K \leftrightarrow \forall x \in B H (x) = K (x))$
25	14 22 24	3bitr4d	$⊢ (F : A \underset{onto}{⟶} B \land H Fn B \land K Fn B) \to (H \circ F = K \circ F \leftrightarrow H = K)$

Metamath Proof Explorer

Theorem cocan2

Proof