fthi

Description: The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	isfth.b	$⊢ B = {Base}_{C}$
	isfth.h	$⊢ H = Hom (C)$
	isfth.j	$⊢ J = Hom (D)$
	fthf1.f	$⊢ φ \to F (C Faith D) G$
	fthf1.x	$⊢ φ \to X \in B$
	fthf1.y	$⊢ φ \to Y \in B$
	fthi.r	$⊢ φ \to R \in (X H Y)$
	fthi.s	$⊢ φ \to S \in (X H Y)$
Assertion	fthi	$⊢ φ \to ((X G Y) (R) = (X G Y) (S) \leftrightarrow R = S)$

Step	Hyp	Ref	Expression
1		isfth.b	$⊢ B = {Base}_{C}$
2		isfth.h	$⊢ H = Hom (C)$
3		isfth.j	$⊢ J = Hom (D)$
4		fthf1.f	$⊢ φ \to F (C Faith D) G$
5		fthf1.x	$⊢ φ \to X \in B$
6		fthf1.y	$⊢ φ \to Y \in B$
7		fthi.r	$⊢ φ \to R \in (X H Y)$
8		fthi.s	$⊢ φ \to S \in (X H Y)$
9	1 2 3 4 5 6	fthf1	$⊢ φ \to (X G Y) : X H Y \underset{1-1}{⟶} F (X) J F (Y)$
10		f1fveq	$⊢ ((X G Y) : X H Y \underset{1-1}{⟶} F (X) J F (Y) \land (R \in (X H Y) \land S \in (X H Y))) \to ((X G Y) (R) = (X G Y) (S) \leftrightarrow R = S)$
11	9 7 8 10	syl12anc	$⊢ φ \to ((X G Y) (R) = (X G Y) (S) \leftrightarrow R = S)$

Metamath Proof Explorer