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 Could not format assertion : No typesetting found for |- ThinCat = { c e. Cat | [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. A. x e. b A. y e. b E* f f e. ( x h y ) } with typecode |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 cthinc Could not format ThinCat : No typesetting found for class ThinCat with typecode class
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 Could not format ThinCat = { c e. Cat | [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. A. x e. b A. y e. b E* f f e. ( x h y ) } : No typesetting found for wff ThinCat = { c e. Cat | [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. A. x e. b A. y e. b E* f f e. ( x h y ) } with typecode wff