Metamath Proof Explorer

Definition df-thinc

Description: Definition of the class of thin categories, or posetal categories, whose hom-sets each contain at most one morphism. Example 3.26(2) of Adamek p. 33. "ThinCat" was taken instead of "PosCat" because the latter might mean the category of posets. (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Assertion df-thinc ⊢ ThinCat = c ∈ Cat | [˙Base c / b]˙ [˙ Hom ⁡ c / h]˙ ∀ x ∈ b ∀ y ∈ b ∃* f f ∈ x h y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cthinc class ThinCat
1 vc setvar c
2 ccat class Cat
3 cbs class Base
4 1 cv setvar c
5 4 3 cfv class Base c
6 vb setvar b
7 chom class Hom
8 4 7 cfv class Hom ⁡ c
9 vh setvar h
10 vx setvar x
11 6 cv setvar b
12 vy setvar y
13 vf setvar f
14 13 cv setvar f
15 10 cv setvar x
16 9 cv setvar h
17 12 cv setvar y
18 15 17 16 co class x h y
19 14 18 wcel wff f ∈ x h y
20 19 13 wmo wff ∃* f f ∈ x h y
21 20 12 11 wral wff ∀ y ∈ b ∃* f f ∈ x h y
22 21 10 11 wral wff ∀ x ∈ b ∀ y ∈ b ∃* f f ∈ x h y
23 22 9 8 wsbc wff [˙ Hom ⁡ c / h]˙ ∀ x ∈ b ∀ y ∈ b ∃* f f ∈ x h y
24 23 6 5 wsbc wff [˙Base c / b]˙ [˙ Hom ⁡ c / h]˙ ∀ x ∈ b ∀ y ∈ b ∃* f f ∈ x h y
25 24 1 2 crab class c ∈ Cat | [˙Base c / b]˙ [˙ Hom ⁡ c / h]˙ ∀ x ∈ b ∀ y ∈ b ∃* f f ∈ x h y
26 0 25 wceq wff ThinCat = c ∈ Cat | [˙Base c / b]˙ [˙ Hom ⁡ c / h]˙ ∀ x ∈ b ∀ y ∈ b ∃* f f ∈ x h y