Metamath Proof Explorer

Theorem arweutermc

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

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

Proof

Step Hyp Ref Expression
1 arweuthinc 
 |-  ( E! a a e. ( Arrow ` C ) -> C e. ThinCat )
2 euex 
 |-  ( E! a a e. ( Arrow ` C ) -> E. a a e. ( Arrow ` C ) )
3 eqid 
 |-  ( Arrow ` C ) = ( Arrow ` C )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 3 4 arwdm 
 |-  ( a e. ( Arrow ` C ) -> ( domA ` a ) e. ( Base ` C ) )
6 eleq1 
 |-  ( x = ( domA ` a ) -> ( x e. ( Base ` C ) <-> ( domA ` a ) e. ( Base ` C ) ) )
7 5 5 6 spcedv 
 |-  ( a e. ( Arrow ` C ) -> E. x x e. ( Base ` C ) )
8 7 exlimiv 
 |-  ( E. a a e. ( Arrow ` C ) -> E. x x e. ( Base ` C ) )
9 2 8 syl 
 |-  ( E! a a e. ( Arrow ` C ) -> E. x x e. ( Base ` C ) )
10 eqeq1 
 |-  ( a = <. x , x , ( ( Id ` C ) ` x ) >. -> ( a = b <-> <. x , x , ( ( Id ` C ) ` x ) >. = b ) )
11 eqeq2 
 |-  ( b = <. y , y , ( ( Id ` C ) ` y ) >. -> ( <. x , x , ( ( Id ` C ) ` x ) >. = b <-> <. x , x , ( ( Id ` C ) ` x ) >. = <. y , y , ( ( Id ` C ) ` y ) >. ) )
12 eumo 
 |-  ( E! a a e. ( Arrow ` C ) -> E* a a e. ( Arrow ` C ) )
13 12 adantr 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> E* a a e. ( Arrow ` C ) )
14 moel 
 |-  ( E* a a e. ( Arrow ` C ) <-> A. a e. ( Arrow ` C ) A. b e. ( Arrow ` C ) a = b )
15 13 14 sylib 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> A. a e. ( Arrow ` C ) A. b e. ( Arrow ` C ) a = b )
16 eqid 
 |-  ( HomA ` C ) = ( HomA ` C )
17 3 16 homarw 
 |-  ( x ( HomA ` C ) x ) C_ ( Arrow ` C )
18 1 adantr 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> C e. ThinCat )
19 18 thinccd 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> C e. Cat )
20 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
21 simprl 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
22 eqid 
 |-  ( Id ` C ) = ( Id ` C )
23 4 20 22 19 21 catidcl 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) )
24 16 4 19 20 21 21 23 elhomai2 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> <. x , x , ( ( Id ` C ) ` x ) >. e. ( x ( HomA ` C ) x ) )
25 17 24 sselid 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> <. x , x , ( ( Id ` C ) ` x ) >. e. ( Arrow ` C ) )
26 3 16 homarw 
 |-  ( y ( HomA ` C ) y ) C_ ( Arrow ` C )
27 simprr 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
28 4 20 22 19 27 catidcl 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( Id ` C ) ` y ) e. ( y ( Hom ` C ) y ) )
29 16 4 19 20 27 27 28 elhomai2 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> <. y , y , ( ( Id ` C ) ` y ) >. e. ( y ( HomA ` C ) y ) )
30 26 29 sselid 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> <. y , y , ( ( Id ` C ) ` y ) >. e. ( Arrow ` C ) )
31 10 11 15 25 30 rspc2dv 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> <. x , x , ( ( Id ` C ) ` x ) >. = <. y , y , ( ( Id ` C ) ` y ) >. )
32 vex 
 |-  x e. _V
33 fvex 
 |-  ( ( Id ` C ) ` x ) e. _V
34 32 32 33 otth 
 |-  ( <. x , x , ( ( Id ` C ) ` x ) >. = <. y , y , ( ( Id ` C ) ` y ) >. <-> ( x = y /\ x = y /\ ( ( Id ` C ) ` x ) = ( ( Id ` C ) ` y ) ) )
35 34 simp1bi 
 |-  ( <. x , x , ( ( Id ` C ) ` x ) >. = <. y , y , ( ( Id ` C ) ` y ) >. -> x = y )
36 31 35 syl 
 |-  ( ( E! a a e. ( Arrow ` C ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x = y )
37 36 ralrimivva 
 |-  ( E! a a e. ( Arrow ` C ) -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) x = y )
38 moel 
 |-  ( E* x x e. ( Base ` C ) <-> A. x e. ( Base ` C ) A. y e. ( Base ` C ) x = y )
39 37 38 sylibr 
 |-  ( E! a a e. ( Arrow ` C ) -> E* x x e. ( Base ` C ) )
40 df-eu 
 |-  ( E! x x e. ( Base ` C ) <-> ( E. x x e. ( Base ` C ) /\ E* x x e. ( Base ` C ) ) )
41 9 39 40 sylanbrc 
 |-  ( E! a a e. ( Arrow ` C ) -> E! x x e. ( Base ` C ) )
42 4 istermc2 
 |-  ( C e. TermCat <-> ( C e. ThinCat /\ E! x x e. ( Base ` C ) ) )
43 1 41 42 sylanbrc 
 |-  ( E! a a e. ( Arrow ` C ) -> C e. TermCat )