This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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