This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem thincfth

Description: A functor from a thin category is faithful. (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Hypotheses thincfth.c ⊢ φ → C ∈ ThinCat
thincfth.f ⊢ φ → F C Func D G
Assertion thincfth ⊢ φ → F C Faith D G

Proof

Step Hyp Ref Expression
1 thincfth.c ⊢ φ → C ∈ ThinCat
2 thincfth.f ⊢ φ → F C Func D G
3 1 adantr ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C → C ∈ ThinCat
4 simprl ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C → x ∈ Base C
5 simprr ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C → y ∈ Base C
6 eqid ⊢ Base C = Base C
7 eqid ⊢ Hom ⁡ C = Hom ⁡ C
8 3 4 5 6 7 thincmo ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C → ∃* f f ∈ x Hom ⁡ C y
9 eqid ⊢ Hom ⁡ D = Hom ⁡ D
10 2 adantr ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C → F C Func D G
11 6 7 9 10 4 5 funcf2 ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C → x G y : x Hom ⁡ C y ⟶ F ⁡ x Hom ⁡ D F ⁡ y
12 f1mo ⊢ ∃* f f ∈ x Hom ⁡ C y ∧ x G y : x Hom ⁡ C y ⟶ F ⁡ x Hom ⁡ D F ⁡ y → x G y : x Hom ⁡ C y ⟶ 1-1 F ⁡ x Hom ⁡ D F ⁡ y
13 8 11 12 syl2anc ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C → x G y : x Hom ⁡ C y ⟶ 1-1 F ⁡ x Hom ⁡ D F ⁡ y
14 13 ralrimivva ⊢ φ → ∀ x ∈ Base C ∀ y ∈ Base C x G y : x Hom ⁡ C y ⟶ 1-1 F ⁡ x Hom ⁡ D F ⁡ y
15 6 7 9 isfth2 ⊢ F C Faith D G ↔ F C Func D G ∧ ∀ x ∈ Base C ∀ y ∈ Base C x G y : x Hom ⁡ C y ⟶ 1-1 F ⁡ x Hom ⁡ D F ⁡ y
16 2 14 15 sylanbrc ⊢ φ → F C Faith D G