Metamath Proof Explorer

Theorem isthinc2

Description: A thin category is a category in which all hom-sets have cardinality less than or equal to the cardinality of 1o . (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthinc.b ⊢ B = Base C
isthinc.h ⊢ H = Hom ⁡ C
Assertion isthinc2 ⊢ C ∈ ThinCat ↔ C ∈ Cat ∧ ∀ x ∈ B ∀ y ∈ B x H y ≼ 1 𝑜

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 modom2 ⊢ ∃* f f ∈ x H y ↔ x H y ≼ 1 𝑜
5 4 2ralbii ⊢ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y ↔ ∀ x ∈ B ∀ y ∈ B x H y ≼ 1 𝑜
6 5 anbi2i ⊢ C ∈ Cat ∧ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y ↔ C ∈ Cat ∧ ∀ x ∈ B ∀ y ∈ B x H y ≼ 1 𝑜
7 3 6 bitri ⊢ C ∈ ThinCat ↔ C ∈ Cat ∧ ∀ x ∈ B ∀ y ∈ B x H y ≼ 1 𝑜