fthf1

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$
Assertion	fthf1	$⊢ φ \to (X G Y) : X H Y \underset{1-1}{⟶} F (X) J F (Y)$

Proof

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	1 2 3	isfth2	$⊢ F (C Faith D) G \leftrightarrow (F (C Func D) G \land \forall x \in B \forall y \in B (x G y) : x H y \underset{1-1}{⟶} F (x) J F (y))$
8	7	simprbi	$⊢ F (C Faith D) G \to \forall x \in B \forall y \in B (x G y) : x H y \underset{1-1}{⟶} F (x) J F (y)$
9	4 8	syl	$⊢ φ \to \forall x \in B \forall y \in B (x G y) : x H y \underset{1-1}{⟶} F (x) J F (y)$
10	6	adantr	$⊢ (φ \land x = X) \to Y \in B$
11		simplr	$⊢ ((φ \land x = X) \land y = Y) \to x = X$
12		simpr	$⊢ ((φ \land x = X) \land y = Y) \to y = Y$
13	11 12	oveq12d	$⊢ ((φ \land x = X) \land y = Y) \to x G y = X G Y$
14	11 12	oveq12d	$⊢ ((φ \land x = X) \land y = Y) \to x H y = X H Y$
15	11	fveq2d	$⊢ ((φ \land x = X) \land y = Y) \to F (x) = F (X)$
16	12	fveq2d	$⊢ ((φ \land x = X) \land y = Y) \to F (y) = F (Y)$
17	15 16	oveq12d	$⊢ ((φ \land x = X) \land y = Y) \to F (x) J F (y) = F (X) J F (Y)$
18	13 14 17	f1eq123d	$⊢ ((φ \land x = X) \land y = Y) \to ((x G y) : x H y \underset{1-1}{⟶} F (x) J F (y) \leftrightarrow (X G Y) : X H Y \underset{1-1}{⟶} F (X) J F (Y))$
19	10 18	rspcdv	$⊢ (φ \land x = X) \to (\forall y \in B (x G y) : x H y \underset{1-1}{⟶} F (x) J F (y) \to (X G Y) : X H Y \underset{1-1}{⟶} F (X) J F (Y))$
20	5 19	rspcimdv	$⊢ φ \to (\forall x \in B \forall y \in B (x G y) : x H y \underset{1-1}{⟶} F (x) J F (y) \to (X G Y) : X H Y \underset{1-1}{⟶} F (X) J F (Y))$
21	9 20	mpd	$⊢ φ \to (X G Y) : X H Y \underset{1-1}{⟶} F (X) J F (Y)$

Metamath Proof Explorer

Theorem fthf1

Proof