Metamath Proof Explorer

Theorem indthinc

Description: An indiscrete category in which all hom-sets have exactly one morphism is a thin category. Constructed here is an indiscrete category where all morphisms are (/) . This is a special case of prsthinc , where .<_ = ( B X. B ) . This theorem also implies a functor from the category of sets to the category of small categories. (Contributed by Zhi Wang, 17-Sep-2024) (Proof shortened by Zhi Wang, 19-Sep-2024)

Ref Expression
Hypotheses indthinc.b 
|- ( ph -> B = ( Base ` C ) )
indthinc.h 
|- ( ph -> ( ( B X. B ) X. { 1o } ) = ( Hom ` C ) )
indthinc.o 
|- ( ph -> (/) = ( comp ` C ) )
indthinc.c 
|- ( ph -> C e. V )
Assertion indthinc 
|- ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B |-> (/) ) ) )

Proof

Step Hyp Ref Expression
1 indthinc.b 
 |-  ( ph -> B = ( Base ` C ) )
2 indthinc.h 
 |-  ( ph -> ( ( B X. B ) X. { 1o } ) = ( Hom ` C ) )
3 indthinc.o 
 |-  ( ph -> (/) = ( comp ` C ) )
4 indthinc.c 
 |-  ( ph -> C e. V )
5 eqidd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( B X. B ) X. { 1o } ) = ( ( B X. B ) X. { 1o } ) )
6 5 f1omo 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* f f e. ( ( ( B X. B ) X. { 1o } ) ` <. x , y >. ) )
7 df-ov 
 |-  ( x ( ( B X. B ) X. { 1o } ) y ) = ( ( ( B X. B ) X. { 1o } ) ` <. x , y >. )
8 7 eleq2i 
 |-  ( f e. ( x ( ( B X. B ) X. { 1o } ) y ) <-> f e. ( ( ( B X. B ) X. { 1o } ) ` <. x , y >. ) )
9 8 mobii 
 |-  ( E* f f e. ( x ( ( B X. B ) X. { 1o } ) y ) <-> E* f f e. ( ( ( B X. B ) X. { 1o } ) ` <. x , y >. ) )
10 6 9 sylibr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* f f e. ( x ( ( B X. B ) X. { 1o } ) y ) )
11 biid 
 |-  ( ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( ( B X. B ) X. { 1o } ) y ) /\ g e. ( y ( ( B X. B ) X. { 1o } ) z ) ) ) <-> ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( ( B X. B ) X. { 1o } ) y ) /\ g e. ( y ( ( B X. B ) X. { 1o } ) z ) ) ) )
12 id 
 |-  ( y e. B -> y e. B )
13 12 ancli 
 |-  ( y e. B -> ( y e. B /\ y e. B ) )
14 1oex 
 |-  1o e. _V
15 14 ovconst2 
 |-  ( ( y e. B /\ y e. B ) -> ( y ( ( B X. B ) X. { 1o } ) y ) = 1o )
16 0lt1o 
 |-  (/) e. 1o
17 eleq2 
 |-  ( ( y ( ( B X. B ) X. { 1o } ) y ) = 1o -> ( (/) e. ( y ( ( B X. B ) X. { 1o } ) y ) <-> (/) e. 1o ) )
18 16 17 mpbiri 
 |-  ( ( y ( ( B X. B ) X. { 1o } ) y ) = 1o -> (/) e. ( y ( ( B X. B ) X. { 1o } ) y ) )
19 13 15 18 3syl 
 |-  ( y e. B -> (/) e. ( y ( ( B X. B ) X. { 1o } ) y ) )
20 19 adantl 
 |-  ( ( ph /\ y e. B ) -> (/) e. ( y ( ( B X. B ) X. { 1o } ) y ) )
21 16 a1i 
 |-  ( ( x e. B /\ y e. B /\ z e. B ) -> (/) e. 1o )
22 0ov 
 |-  ( <. x , y >. (/) z ) = (/)
23 22 oveqi 
 |-  ( g ( <. x , y >. (/) z ) f ) = ( g (/) f )
24 0ov 
 |-  ( g (/) f ) = (/)
25 23 24 eqtri 
 |-  ( g ( <. x , y >. (/) z ) f ) = (/)
26 25 a1i 
 |-  ( ( x e. B /\ y e. B /\ z e. B ) -> ( g ( <. x , y >. (/) z ) f ) = (/) )
27 14 ovconst2 
 |-  ( ( x e. B /\ z e. B ) -> ( x ( ( B X. B ) X. { 1o } ) z ) = 1o )
28 27 3adant2 
 |-  ( ( x e. B /\ y e. B /\ z e. B ) -> ( x ( ( B X. B ) X. { 1o } ) z ) = 1o )
29 21 26 28 3eltr4d 
 |-  ( ( x e. B /\ y e. B /\ z e. B ) -> ( g ( <. x , y >. (/) z ) f ) e. ( x ( ( B X. B ) X. { 1o } ) z ) )
30 29 ad2antrl 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x ( ( B X. B ) X. { 1o } ) y ) /\ g e. ( y ( ( B X. B ) X. { 1o } ) z ) ) ) ) -> ( g ( <. x , y >. (/) z ) f ) e. ( x ( ( B X. B ) X. { 1o } ) z ) )
31 1 2 10 3 4 11 20 30 isthincd2 
 |-  ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B |-> (/) ) ) )