cocanfo

Description: Cancellation of a surjective function from the right side of a composition. (Contributed by Jeff Madsen, 1-Jun-2011) (Proof shortened by Mario Carneiro, 27-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ (((F : A \underset{onto}{⟶} B \land G Fn B \land H Fn B) \land G \circ F = H \circ F) \land y \in A) \to G \circ F = H \circ F$
2	1	fveq1d	$⊢ (((F : A \underset{onto}{⟶} B \land G Fn B \land H Fn B) \land G \circ F = H \circ F) \land y \in A) \to (G \circ F) (y) = (H \circ F) (y)$
3		simpl1	$⊢ ((F : A \underset{onto}{⟶} B \land G Fn B \land H Fn B) \land G \circ F = H \circ F) \to F : A \underset{onto}{⟶} B$
4		fof	$⊢ F : A \underset{onto}{⟶} B \to F : A ⟶ B$
5	3 4	syl	$⊢ ((F : A \underset{onto}{⟶} B \land G Fn B \land H Fn B) \land G \circ F = H \circ F) \to F : A ⟶ B$
6		fvco3	$⊢ (F : A ⟶ B \land y \in A) \to (G \circ F) (y) = G (F (y))$
7	5 6	sylan	$⊢ (((F : A \underset{onto}{⟶} B \land G Fn B \land H Fn B) \land G \circ F = H \circ F) \land y \in A) \to (G \circ F) (y) = G (F (y))$
8		fvco3	$⊢ (F : A ⟶ B \land y \in A) \to (H \circ F) (y) = H (F (y))$
9	5 8	sylan	$⊢ (((F : A \underset{onto}{⟶} B \land G Fn B \land H Fn B) \land G \circ F = H \circ F) \land y \in A) \to (H \circ F) (y) = H (F (y))$
10	2 7 9	3eqtr3d	$⊢ (((F : A \underset{onto}{⟶} B \land G Fn B \land H Fn B) \land G \circ F = H \circ F) \land y \in A) \to G (F (y)) = H (F (y))$
11	10	ralrimiva	$⊢ ((F : A \underset{onto}{⟶} B \land G Fn B \land H Fn B) \land G \circ F = H \circ F) \to \forall y \in A G (F (y)) = H (F (y))$
12		fveq2	$⊢ F (y) = x \to G (F (y)) = G (x)$
13		fveq2	$⊢ F (y) = x \to H (F (y)) = H (x)$
14	12 13	eqeq12d	$⊢ F (y) = x \to (G (F (y)) = H (F (y)) \leftrightarrow G (x) = H (x))$
15	14	cbvfo	$⊢ F : A \underset{onto}{⟶} B \to (\forall y \in A G (F (y)) = H (F (y)) \leftrightarrow \forall x \in B G (x) = H (x))$
16	3 15	syl	$⊢ ((F : A \underset{onto}{⟶} B \land G Fn B \land H Fn B) \land G \circ F = H \circ F) \to (\forall y \in A G (F (y)) = H (F (y)) \leftrightarrow \forall x \in B G (x) = H (x))$
17	11 16	mpbid	$⊢ ((F : A \underset{onto}{⟶} B \land G Fn B \land H Fn B) \land G \circ F = H \circ F) \to \forall x \in B G (x) = H (x)$
18		eqfnfv	$⊢ (G Fn B \land H Fn B) \to (G = H \leftrightarrow \forall x \in B G (x) = H (x))$
19	18	3adant1	$⊢ (F : A \underset{onto}{⟶} B \land G Fn B \land H Fn B) \to (G = H \leftrightarrow \forall x \in B G (x) = H (x))$
20	19	adantr	$⊢ ((F : A \underset{onto}{⟶} B \land G Fn B \land H Fn B) \land G \circ F = H \circ F) \to (G = H \leftrightarrow \forall x \in B G (x) = H (x))$
21	17 20	mpbird	$⊢ ((F : A \underset{onto}{⟶} B \land G Fn B \land H Fn B) \land G \circ F = H \circ F) \to G = H$

Metamath Proof Explorer

Theorem cocanfo

Proof