Metamath Proof Explorer

Theorem discthing

Description: A discrete category, i.e., a category where all morphisms are identity morphisms, is thin. Example 3.26(1) of Adamek p. 33. (Contributed by Zhi Wang, 11-Nov-2025)

Ref Expression
Hypotheses indcthing.b ⊢ φ → B = Base C
indcthing.h ⊢ φ → H = Hom ⁡ C
indcthing.c ⊢ φ → C ∈ Cat
discthing.i ⊢ φ ∧ x ∈ B ∧ y ∈ B → x H y = if x = y I ∅
Assertion discthing ⊢ φ → C ∈ ThinCat

Proof

Step Hyp Ref Expression
1 indcthing.b ⊢ φ → B = Base C
2 indcthing.h ⊢ φ → H = Hom ⁡ C
3 indcthing.c ⊢ φ → C ∈ Cat
4 discthing.i ⊢ φ ∧ x ∈ B ∧ y ∈ B → x H y = if x = y I ∅
5 eleq2w2 ⊢ I = if x = y I ∅ → i ∈ I ↔ i ∈ if x = y I ∅
6 5 mobidv ⊢ I = if x = y I ∅ → ∃* i i ∈ I ↔ ∃* i i ∈ if x = y I ∅
7 eleq2w2 ⊢ ∅ = if x = y I ∅ → i ∈ ∅ ↔ i ∈ if x = y I ∅
8 7 mobidv ⊢ ∅ = if x = y I ∅ → ∃* i i ∈ ∅ ↔ ∃* i i ∈ if x = y I ∅
9 eqid ⊢ I = I
10 mosn ⊢ I = I → ∃* i i ∈ I
11 9 10 mp1i ⊢ φ ∧ x ∈ B ∧ y ∈ B ∧ x = y → ∃* i i ∈ I
12 eqid ⊢ ∅ = ∅
13 mo0 ⊢ ∅ = ∅ → ∃* i i ∈ ∅
14 12 13 mp1i ⊢ φ ∧ x ∈ B ∧ y ∈ B ∧ ¬ x = y → ∃* i i ∈ ∅
15 6 8 11 14 ifbothda ⊢ φ ∧ x ∈ B ∧ y ∈ B → ∃* i i ∈ if x = y I ∅
16 4 eleq2d ⊢ φ ∧ x ∈ B ∧ y ∈ B → i ∈ x H y ↔ i ∈ if x = y I ∅
17 16 mobidv ⊢ φ ∧ x ∈ B ∧ y ∈ B → ∃* i i ∈ x H y ↔ ∃* i i ∈ if x = y I ∅
18 15 17 mpbird ⊢ φ ∧ x ∈ B ∧ y ∈ B → ∃* i i ∈ x H y
19 1 2 18 3 isthincd ⊢ φ → C ∈ ThinCat