Metamath Proof Explorer

Theorem arweuthinc

Description: If a structure has a unique disjointified arrow, then the structure is a thin category. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Assertion arweuthinc 
|- ( E! a a e. ( Arrow ` C ) -> C e. ThinCat )

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( E! a a e. ( Arrow ` C ) -> ( Base ` C ) = ( Base ` C ) )
2 eqidd 
 |-  ( E! a a e. ( Arrow ` C ) -> ( Hom ` C ) = ( Hom ` C ) )
3 eqeq1 
 |-  ( a = <. x , y , f >. -> ( a = b <-> <. x , y , f >. = b ) )
4 eqeq2 
 |-  ( b = <. x , y , g >. -> ( <. x , y , f >. = b <-> <. x , y , f >. = <. x , y , g >. ) )
5 eumo 
 |-  ( E! a a e. ( Arrow ` C ) -> E* a a e. ( Arrow ` C ) )
6 5 ad2antrr 
 |-  ( ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( x ( Hom ` C ) y ) ) ) -> E* a a e. ( Arrow ` C ) )
7 moel 
 |-  ( E* a a e. ( Arrow ` C ) <-> A. a e. ( Arrow ` C ) A. b e. ( Arrow ` C ) a = b )
8 6 7 sylib 
 |-  ( ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( x ( Hom ` C ) y ) ) ) -> A. a e. ( Arrow ` C ) A. b e. ( Arrow ` C ) a = b )
9 eqid 
 |-  ( Arrow ` C ) = ( Arrow ` C )
10 eqid 
 |-  ( HomA ` C ) = ( HomA ` C )
11 9 10 homarw 
 |-  ( x ( HomA ` C ) y ) C_ ( Arrow ` C )
12 eqid 
 |-  ( Base ` C ) = ( Base ` C )
13 euex 
 |-  ( E! a a e. ( Arrow ` C ) -> E. a a e. ( Arrow ` C ) )
14 9 arwrcl 
 |-  ( a e. ( Arrow ` C ) -> C e. Cat )
15 14 exlimiv 
 |-  ( E. a a e. ( Arrow ` C ) -> C e. Cat )
16 13 15 syl 
 |-  ( E! a a e. ( Arrow ` C ) -> C e. Cat )
17 16 ad2antrr 
 |-  ( ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( x ( Hom ` C ) y ) ) ) -> C e. Cat )
18 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
19 simplrl 
 |-  ( ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( x ( Hom ` C ) y ) ) ) -> x e. ( Base ` C ) )
20 simplrr 
 |-  ( ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( x ( Hom ` C ) y ) ) ) -> y e. ( Base ` C ) )
21 simprl 
 |-  ( ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( x ( Hom ` C ) y ) ) ) -> f e. ( x ( Hom ` C ) y ) )
22 10 12 17 18 19 20 21 elhomai2 
 |-  ( ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( x ( Hom ` C ) y ) ) ) -> <. x , y , f >. e. ( x ( HomA ` C ) y ) )
23 11 22 sselid 
 |-  ( ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( x ( Hom ` C ) y ) ) ) -> <. x , y , f >. e. ( Arrow ` C ) )
24 simprr 
 |-  ( ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( x ( Hom ` C ) y ) ) ) -> g e. ( x ( Hom ` C ) y ) )
25 10 12 17 18 19 20 24 elhomai2 
 |-  ( ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( x ( Hom ` C ) y ) ) ) -> <. x , y , g >. e. ( x ( HomA ` C ) y ) )
26 11 25 sselid 
 |-  ( ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( x ( Hom ` C ) y ) ) ) -> <. x , y , g >. e. ( Arrow ` C ) )
27 3 4 8 23 26 rspc2dv 
 |-  ( ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( x ( Hom ` C ) y ) ) ) -> <. x , y , f >. = <. x , y , g >. )
28 vex 
 |-  x e. _V
29 vex 
 |-  y e. _V
30 vex 
 |-  f e. _V
31 28 29 30 otth 
 |-  ( <. x , y , f >. = <. x , y , g >. <-> ( x = x /\ y = y /\ f = g ) )
32 31 simp3bi 
 |-  ( <. x , y , f >. = <. x , y , g >. -> f = g )
33 27 32 syl 
 |-  ( ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( x ( Hom ` C ) y ) ) ) -> f = g )
34 33 ralrimivva 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> A. f e. ( x ( Hom ` C ) y ) A. g e. ( x ( Hom ` C ) y ) f = g )
35 moel 
 |-  ( E* f f e. ( x ( Hom ` C ) y ) <-> A. f e. ( x ( Hom ` C ) y ) A. g e. ( x ( Hom ` C ) y ) f = g )
36 34 35 sylibr 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> E* f f e. ( x ( Hom ` C ) y ) )
37 1 2 36 16 isthincd 
 |-  ( E! a a e. ( Arrow ` C ) -> C e. ThinCat )