Metamath Proof Explorer

Theorem isthinc3

Description: A thin category is a category in which, given a pair of objects x and y and any two morphisms f , g from x to y , the morphisms are equal. (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthinc.b ⊢ B = Base C
isthinc.h ⊢ H = Hom ⁡ C
Assertion isthinc3 ⊢ C ∈ ThinCat ↔ C ∈ Cat ∧ ∀ x ∈ B ∀ y ∈ B ∀ f ∈ x H y ∀ g ∈ x H y f = g

Proof

Step Hyp Ref Expression
1 isthinc.b ⊢ B = Base C
2 isthinc.h ⊢ H = Hom ⁡ C
3 1 2 isthinc ⊢ C ∈ ThinCat ↔ C ∈ Cat ∧ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y
4 moel ⊢ ∃* f f ∈ x H y ↔ ∀ f ∈ x H y ∀ g ∈ x H y f = g
5 4 2ralbii ⊢ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y ↔ ∀ x ∈ B ∀ y ∈ B ∀ f ∈ x H y ∀ g ∈ x H y f = g
6 5 anbi2i ⊢ C ∈ Cat ∧ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y ↔ C ∈ Cat ∧ ∀ x ∈ B ∀ y ∈ B ∀ f ∈ x H y ∀ g ∈ x H y f = g
7 3 6 bitri ⊢ C ∈ ThinCat ↔ C ∈ Cat ∧ ∀ x ∈ B ∀ y ∈ B ∀ f ∈ x H y ∀ g ∈ x H y f = g