ffthf1o

Description: The morphism map of a fully faithful functor is a bijection. (Contributed by Mario Carneiro, 29-Jan-2017)

	Ref	Expression
Hypotheses	isfth.b	$⊢ B = {Base}_{C}$
	isfth.h	$⊢ H = Hom (C)$
	isfth.j	$⊢ J = Hom (D)$
	ffthf1o.f	$⊢ φ \to F ((C Full D) \cap (C Faith D)) G$
	ffthf1o.x	$⊢ φ \to X \in B$
	ffthf1o.y	$⊢ φ \to Y \in B$
Assertion	ffthf1o	$⊢ φ \to (X G Y) : X H Y \underset{1-1 onto}{⟶} F (X) J F (Y)$

Step	Hyp	Ref	Expression
1		isfth.b	$⊢ B = {Base}_{C}$
2		isfth.h	$⊢ H = Hom (C)$
3		isfth.j	$⊢ J = Hom (D)$
4		ffthf1o.f	$⊢ φ \to F ((C Full D) \cap (C Faith D)) G$
5		ffthf1o.x	$⊢ φ \to X \in B$
6		ffthf1o.y	$⊢ φ \to Y \in B$
7		brin	$⊢ F ((C Full D) \cap (C Faith D)) G \leftrightarrow (F (C Full D) G \land F (C Faith D) G)$
8	4 7	sylib	$⊢ φ \to (F (C Full D) G \land F (C Faith D) G)$
9	8	simprd	$⊢ φ \to F (C Faith D) G$
10	1 2 3 9 5 6	fthf1	$⊢ φ \to (X G Y) : X H Y \underset{1-1}{⟶} F (X) J F (Y)$
11	8	simpld	$⊢ φ \to F (C Full D) G$
12	1 3 2 11 5 6	fullfo	$⊢ φ \to (X G Y) : X H Y \underset{onto}{⟶} F (X) J F (Y)$
13		df-f1o	$⊢ (X G Y) : X H Y \underset{1-1 onto}{⟶} F (X) J F (Y) \leftrightarrow ((X G Y) : X H Y \underset{1-1}{⟶} F (X) J F (Y) \land (X G Y) : X H Y \underset{onto}{⟶} F (X) J F (Y))$
14	10 12 13	sylanbrc	$⊢ φ \to (X G Y) : X H Y \underset{1-1 onto}{⟶} F (X) J F (Y)$

Metamath Proof Explorer