Metamath Proof Explorer

Theorem isffth2

Description: A fully faithful functor is a functor which is bijective on hom-sets. (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)$
	Assertion	isffth2	$⊢ F ((C Full D) \cap (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 onto}{⟶} 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	1 3 2	isfull2	$⊢ F (C Full D) G \leftrightarrow (F (C Func D) G \land \forall x \in B \forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y))$
5	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))$
6	4 5	anbi12i	$⊢ (F (C Full D) G \land 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{onto}{⟶} F (x) J F (y)) \land (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)))$
7		brin	$⊢ F ((C Full D) \cap (C Faith D)) G \leftrightarrow (F (C Full D) G \land F (C Faith D) G)$
8		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))$
9	8	biancomi	$⊢ (x G y) : x H y \underset{1-1 onto}{⟶} F (x) J F (y) \leftrightarrow ((x G y) : x H y \underset{onto}{⟶} F (x) J F (y) \land (x G y) : x H y \underset{1-1}{⟶} F (x) J F (y))$
10	9	2ralbii	$⊢ \forall x \in B \forall y \in B (x G y) : x H y \underset{1-1 onto}{⟶} F (x) J F (y) \leftrightarrow \forall x \in B \forall y \in B ((x G y) : x H y \underset{onto}{⟶} F (x) J F (y) \land (x G y) : x H y \underset{1-1}{⟶} F (x) J F (y))$
11		r19.26-2	$⊢ \forall x \in B \forall y \in B ((x G y) : x H y \underset{onto}{⟶} F (x) J F (y) \land (x G y) : x H y \underset{1-1}{⟶} F (x) J F (y)) \leftrightarrow (\forall x \in B \forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y) \land \forall x \in B \forall y \in B (x G y) : x H y \underset{1-1}{⟶} F (x) J F (y))$
12	10 11	bitri	$⊢ \forall x \in B \forall y \in B (x G y) : x H y \underset{1-1 onto}{⟶} F (x) J F (y) \leftrightarrow (\forall x \in B \forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y) \land \forall x \in B \forall y \in B (x G y) : x H y \underset{1-1}{⟶} F (x) J F (y))$
13	12	anbi2i	$⊢ (F (C Func D) G \land \forall x \in B \forall y \in B (x G y) : x H y \underset{1-1 onto}{⟶} F (x) J F (y)) \leftrightarrow (F (C Func D) G \land (\forall x \in B \forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y) \land \forall x \in B \forall y \in B (x G y) : x H y \underset{1-1}{⟶} F (x) J F (y)))$
14		anandi	$⊢ (F (C Func D) G \land (\forall x \in B \forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y) \land \forall x \in B \forall y \in B (x G y) : x H y \underset{1-1}{⟶} F (x) J F (y))) \leftrightarrow ((F (C Func D) G \land \forall x \in B \forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y)) \land (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)))$
15	13 14	bitri	$⊢ (F (C Func D) G \land \forall x \in B \forall y \in B (x G y) : x H y \underset{1-1 onto}{⟶} F (x) J F (y)) \leftrightarrow ((F (C Func D) G \land \forall x \in B \forall y \in B (x G y) : x H y \underset{onto}{⟶} F (x) J F (y)) \land (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)))$
16	6 7 15	3bitr4i	$⊢ F ((C Full D) \cap (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 onto}{⟶} F (x) J F (y))$