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 
|- ( ph -> B = ( Base ` C ) )
indcthing.h 
|- ( ph -> H = ( Hom ` C ) )
indcthing.c 
|- ( ph -> C e. Cat )
indcthing.i 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x H y ) = { F } )
Assertion indcthing 
|- ( ph -> C e. ThinCat )

Proof

Step Hyp Ref Expression
1 indcthing.b 
 |-  ( ph -> B = ( Base ` C ) )
2 indcthing.h 
 |-  ( ph -> H = ( Hom ` C ) )
3 indcthing.c 
 |-  ( ph -> C e. Cat )
4 indcthing.i 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x H y ) = { F } )
5 eqid 
 |-  { F } = { F }
6 mosn 
 |-  ( { F } = { F } -> E* f f e. { F } )
7 5 6 ax-mp 
 |-  E* f f e. { F }
8 4 eleq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( f e. ( x H y ) <-> f e. { F } ) )
9 8 mobidv 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E* f f e. ( x H y ) <-> E* f f e. { F } ) )
10 7 9 mpbiri 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* f f e. ( x H y ) )
11 1 2 10 3 isthincd 
 |-  ( ph -> C e. ThinCat )