Metamath Proof Explorer

Theorem isfth2

Description: Equivalent condition for a faithful functor. (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	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))$

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	isfth	$⊢ F (C Faith D) G \leftrightarrow (F (C Func D) G \land \forall x \in B \forall y \in B Fun {(x G y)}^{-1})$
5		simpll	$⊢ ((F (C Func D) G \land x \in B) \land y \in B) \to F (C Func D) G$
6		simplr	$⊢ ((F (C Func D) G \land x \in B) \land y \in B) \to x \in B$
7		simpr	$⊢ ((F (C Func D) G \land x \in B) \land y \in B) \to y \in B$
8	1 2 3 5 6 7	funcf2	$⊢ ((F (C Func D) G \land x \in B) \land y \in B) \to (x G y) : x H y ⟶ F (x) J F (y)$
9		df-f1	$⊢ (x G y) : x H y \underset{1-1}{⟶} F (x) J F (y) \leftrightarrow ((x G y) : x H y ⟶ F (x) J F (y) \land Fun {(x G y)}^{-1})$
10	9	baib	$⊢ (x G y) : x H y ⟶ F (x) J F (y) \to ((x G y) : x H y \underset{1-1}{⟶} F (x) J F (y) \leftrightarrow Fun {(x G y)}^{-1})$
11	8 10	syl	$⊢ ((F (C Func D) G \land x \in B) \land y \in B) \to ((x G y) : x H y \underset{1-1}{⟶} F (x) J F (y) \leftrightarrow Fun {(x G y)}^{-1})$
12	11	ralbidva	$⊢ (F (C Func D) G \land x \in B) \to (\forall y \in B (x G y) : x H y \underset{1-1}{⟶} F (x) J F (y) \leftrightarrow \forall y \in B Fun {(x G y)}^{-1})$
13	12	ralbidva	$⊢ F (C Func 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) \leftrightarrow \forall x \in B \forall y \in B Fun {(x G y)}^{-1})$
14	13	pm5.32i	$⊢ (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)) \leftrightarrow (F (C Func D) G \land \forall x \in B \forall y \in B Fun {(x G y)}^{-1})$
15	4 14	bitr4i	$⊢ 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))$