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

Metamath Proof Explorer

Theorem indcthing

Description: An indiscrete category, i.e., a category where all hom-sets have exactly one morphism, is thin. (Contributed by Zhi Wang, 11-Nov-2025)

Ref Expression
Hypotheses indcthing.b ⊢ φ → B = Base C
indcthing.h ⊢ φ → H = Hom ⁡ C
indcthing.c ⊢ φ → C ∈ Cat
indcthing.i ⊢ φ ∧ x ∈ B ∧ y ∈ B → x H y = F
Assertion indcthing ⊢ φ → 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 indcthing.i ⊢ φ ∧ x ∈ B ∧ y ∈ B → x H y = F
5 eqid ⊢ F = F
6 mosn ⊢ F = F → ∃* f f ∈ F
7 5 6 ax-mp ⊢ ∃* f f ∈ F
8 4 eleq2d ⊢ φ ∧ x ∈ B ∧ y ∈ B → f ∈ x H y ↔ f ∈ F
9 8 mobidv ⊢ φ ∧ x ∈ B ∧ y ∈ B → ∃* f f ∈ x H y ↔ ∃* f f ∈ F
10 7 9 mpbiri ⊢ φ ∧ x ∈ B ∧ y ∈ B → ∃* f f ∈ x H y
11 1 2 10 3 isthincd ⊢ φ → C ∈ ThinCat