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 ∩ C Faith D G ↔ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 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 ↔ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y
5 1 2 3 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
6 4 5 anbi12i ⊢ F C Full D G ∧ F C Faith D G ↔ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ∧ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y
7 brin ⊢ F C Full D ∩ C Faith D G ↔ F C Full D G ∧ F C Faith D G
8 df-f1o ⊢ x G y : x H y ⟶ 1-1 onto F ⁡ x J F ⁡ y ↔ x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y ∧ x G y : x H y ⟶ onto F ⁡ x J F ⁡ y
9 8 biancomi ⊢ x G y : x H y ⟶ 1-1 onto F ⁡ x J F ⁡ y ↔ x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ∧ x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y
10 9 2ralbii ⊢ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 1-1 onto F ⁡ x J F ⁡ y ↔ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ∧ x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y
11 r19.26-2 ⊢ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ∧ x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y ↔ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y
12 10 11 bitri ⊢ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 1-1 onto F ⁡ x J F ⁡ y ↔ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y
13 12 anbi2i ⊢ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 1-1 onto F ⁡ x J F ⁡ y ↔ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y
14 anandi ⊢ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ∧ ∀ 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 x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ∧ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y
15 13 14 bitri ⊢ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 1-1 onto F ⁡ x J F ⁡ y ↔ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ onto F ⁡ x J F ⁡ y ∧ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 1-1 F ⁡ x J F ⁡ y
16 6 7 15 3bitr4i ⊢ F C Full D ∩ C Faith D G ↔ F C Func D G ∧ ∀ x ∈ B ∀ y ∈ B x G y : x H y ⟶ 1-1 onto F ⁡ x J F ⁡ y