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	$$setvarc$$
2		ccat	$$class\mathrm{Cat}$$
3		cbs	$$class\mathrm{Base}$$
4	1	cv	$$setvarc$$
5	4 3	cfv	$$class{\mathrm{Base}}_c$$
6		vb	$$setvarb$$
7		chom	$$class\mathrm{Hom}$$
8	4 7	cfv	$$class\mathrm{Hom}\left(c\right)$$
9		vh	$$setvarh$$
10		vx	$$setvarx$$
11	6	cv	$$setvarb$$
12		vy	$$setvary$$
13		vf	$$setvarf$$
14	13	cv	$$setvarf$$
15	10	cv	$$setvarx$$
16	9	cv	$$setvarh$$
17	12	cv	$$setvary$$
18	15 17 16	co	$$class\left(xhy\right)$$
19	14 18	wcel	$$wfff\in \left(xhy\right)$$
20	19 13	wmo	$$wff{\exists }^{*}ff\in \left(xhy\right)$$
21	20 12 11	wral	$$wff\forall y\in b{\exists }^{*}ff\in \left(xhy\right)$$
22	21 10 11	wral	$$wff\forall x\in b\forall y\in b{\exists }^{*}ff\in \left(xhy\right)$$
23	22 9 8	wsbc	$$wff\underset{\dot{}}{[}\mathrm{Hom}\left(c\right)/h\underset{\dot{}}{]}\forall x\in b\forall y\in b{\exists }^{*}ff\in \left(xhy\right)$$
24	23 6 5	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_c/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Hom}\left(c\right)/h\underset{\dot{}}{]}\forall x\in b\forall y\in b{\exists }^{*}ff\in \left(xhy\right)$$
25	24 1 2	crab	$$class\left\{c\in \mathrm{Cat}|\underset{\dot{}}{[}{\mathrm{Base}}_c/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Hom}\left(c\right)/h\underset{\dot{}}{]}\forall x\in b\forall y\in b{\exists }^{*}ff\in \left(xhy\right)\right\}$$
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