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 ↔ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 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 ↔ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B Fun ⁡ x G y -1
5 simpll ⊢ F C Func D G ∧ x ∈ B ∧ y ∈ B → F C Func D G
6 simplr ⊢ F C Func D G ∧ x ∈ B ∧ y ∈ B → x ∈ B
7 simpr ⊢ F C Func D G ∧ x ∈ B ∧ y ∈ B → y ∈ B
8 1 2 3 5 6 7 funcf2 ⊢ F C Func D G ∧ x ∈ B ∧ y ∈ B → x G y : x H y ⟶ F ⁡ x J F ⁡ y
9 df-f1 ⊢ x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y ↔ x G y : x H y ⟶ F ⁡ x J F ⁡ y ∧ Fun ⁡ x G y -1
10 9 baib ⊢ x G y : x H y ⟶ F ⁡ x J F ⁡ y → x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y ↔ Fun ⁡ x G y -1
11 8 10 syl ⊢ F C Func D G ∧ x ∈ B ∧ y ∈ B → x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y ↔ Fun ⁡ x G y -1
12 11 ralbidva ⊢ F C Func D G ∧ x ∈ B → ∀ y ∈ B x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y ↔ ∀ y ∈ B Fun ⁡ x G y -1
13 12 ralbidva ⊢ F C Func D G → ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y ↔ ∀ x ∈ B ∀ y ∈ B Fun ⁡ x G y -1
14 13 pm5.32i ⊢ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y ↔ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B Fun ⁡ x G y -1
15 4 14 bitr4i ⊢ F C Faith D G ↔ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y