Definition df-thinc 50661

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.)

Assertion

Ref	Expression
df-thinc	⊢ ThinCat = {𝑐 ∈ Cat ∣ [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃*𝑓 𝑓 ∈ (𝑥ℎ𝑦)}

Distinct variable group:   𝑏,𝑐,𝑓,ℎ,𝑥,𝑦

Detailed syntax breakdown of Definition df-thinc

Step	Hyp	Ref	Expression
1		cthinc 50660	. 2 class ThinCat
2		vf	. . . . . . . . . 10 setvar 𝑓
3	2	cv 1568	. . . . . . . . 9 class 𝑓
4		vx	. . . . . . . . . . 11 setvar 𝑥
5	4	cv 1568	. . . . . . . . . 10 class 𝑥
6		vy	. . . . . . . . . . 11 setvar 𝑦
7	6	cv 1568	. . . . . . . . . 10 class 𝑦
8		vh	. . . . . . . . . . 11 setvar ℎ
9	8	cv 1568	. . . . . . . . . 10 class ℎ
10	5, 7, 9	co 7424	. . . . . . . . 9 class (𝑥ℎ𝑦)
11	3, 10	wcel 2144	. . . . . . . 8 wff 𝑓 ∈ (𝑥ℎ𝑦)
12	11, 2	wmo 2562	. . . . . . 7 wff ∃*𝑓 𝑓 ∈ (𝑥ℎ𝑦)
13		vb	. . . . . . . 8 setvar 𝑏
14	13	cv 1568	. . . . . . 7 class 𝑏
15	12, 6, 14	wral 3076	. . . . . 6 wff ∀𝑦 ∈ 𝑏 ∃*𝑓 𝑓 ∈ (𝑥ℎ𝑦)
16	15, 4, 14	wral 3076	. . . . 5 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃*𝑓 𝑓 ∈ (𝑥ℎ𝑦)
17		vc	. . . . . . 7 setvar 𝑐
18	17	cv 1568	. . . . . 6 class 𝑐
19		chom 17448	. . . . . 6 class Hom
20	18, 19	cfv 6543	. . . . 5 class (Hom ‘𝑐)
21	16, 8, 20	wsbc 3738	. . . 4 wff [(Hom ‘𝑐) / ℎ]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃*𝑓 𝑓 ∈ (𝑥ℎ𝑦)
22		cbs 17396	. . . . 5 class Base
23	18, 22	cfv 6543	. . . 4 class (Base‘𝑐)
24	21, 13, 23	wsbc 3738	. . 3 wff [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃*𝑓 𝑓 ∈ (𝑥ℎ𝑦)
25		ccat 17847	. . 3 class Cat
26	24, 17, 25	crab 3412	. 2 class {𝑐 ∈ Cat ∣ [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃*𝑓 𝑓 ∈ (𝑥ℎ𝑦)}
27	1, 26	wceq 1569	1 wff ThinCat = {𝑐 ∈ Cat ∣ [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃*𝑓 𝑓 ∈ (𝑥ℎ𝑦)}

This definition is used by:  isthinc  50662