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

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 
|- ( ph -> B = ( Base ` C ) )
indcthing.h 
|- ( ph -> H = ( Hom ` C ) )
indcthing.c 
|- ( ph -> C e. Cat )
discthing.i 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x H y ) = if ( x = y , { I } , (/) ) )
Assertion discthing 
|- ( 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 discthing.i 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x H y ) = if ( x = y , { I } , (/) ) )
5 eleq2w2 
 |-  ( { I } = if ( x = y , { I } , (/) ) -> ( i e. { I } <-> i e. if ( x = y , { I } , (/) ) ) )
6 5 mobidv 
 |-  ( { I } = if ( x = y , { I } , (/) ) -> ( E* i i e. { I } <-> E* i i e. if ( x = y , { I } , (/) ) ) )
7 eleq2w2 
 |-  ( (/) = if ( x = y , { I } , (/) ) -> ( i e. (/) <-> i e. if ( x = y , { I } , (/) ) ) )
8 7 mobidv 
 |-  ( (/) = if ( x = y , { I } , (/) ) -> ( E* i i e. (/) <-> E* i i e. if ( x = y , { I } , (/) ) ) )
9 eqid 
 |-  { I } = { I }
10 mosn 
 |-  ( { I } = { I } -> E* i i e. { I } )
11 9 10 mp1i 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ x = y ) -> E* i i e. { I } )
12 eqid 
 |-  (/) = (/)
13 mo0 
 |-  ( (/) = (/) -> E* i i e. (/) )
14 12 13 mp1i 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ -. x = y ) -> E* i i e. (/) )
15 6 8 11 14 ifbothda 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* i i e. if ( x = y , { I } , (/) ) )
16 4 eleq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( i e. ( x H y ) <-> i e. if ( x = y , { I } , (/) ) ) )
17 16 mobidv 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E* i i e. ( x H y ) <-> E* i i e. if ( x = y , { I } , (/) ) ) )
18 15 17 mpbird 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* i i e. ( x H y ) )
19 1 2 18 3 isthincd 
 |-  ( ph -> C e. ThinCat )