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 = { 𝑐 ∈ Cat ∣ [ ( Base ‘ 𝑐 ) / 𝑏 ] [ ( Hom ‘ 𝑐 ) / ℎ ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cthinc	⊢ ThinCat
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3		cbs	⊢ Base
4	1	cv	⊢ 𝑐
5	4 3	cfv	⊢ ( Base ‘ 𝑐 )
6		vb	⊢ 𝑏
7		chom	⊢ Hom
8	4 7	cfv	⊢ ( Hom ‘ 𝑐 )
9		vh	⊢ ℎ
10		vx	⊢ 𝑥
11	6	cv	⊢ 𝑏
12		vy	⊢ 𝑦
13		vf	⊢ 𝑓
14	13	cv	⊢ 𝑓
15	10	cv	⊢ 𝑥
16	9	cv	⊢ ℎ
17	12	cv	⊢ 𝑦
18	15 17 16	co	⊢ ( 𝑥 ℎ 𝑦 )
19	14 18	wcel	⊢ 𝑓 ∈ ( 𝑥 ℎ 𝑦 )
20	19 13	wmo	⊢ ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 )
21	20 12 11	wral	⊢ ∀ 𝑦 ∈ 𝑏 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 )
22	21 10 11	wral	⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 )
23	22 9 8	wsbc	⊢ [ ( Hom ‘ 𝑐 ) / ℎ ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 )
24	23 6 5	wsbc	⊢ [ ( Base ‘ 𝑐 ) / 𝑏 ] [ ( Hom ‘ 𝑐 ) / ℎ ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 )
25	24 1 2	crab	⊢ { 𝑐 ∈ Cat ∣ [ ( Base ‘ 𝑐 ) / 𝑏 ] [ ( Hom ‘ 𝑐 ) / ℎ ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) }
26	0 25	wceq	⊢ ThinCat = { 𝑐 ∈ Cat ∣ [ ( Base ‘ 𝑐 ) / 𝑏 ] [ ( Hom ‘ 𝑐 ) / ℎ ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃* 𝑓 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) }