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

Metamath Proof Explorer

Theorem euendfunc

Description: If there exists a unique endofunctor (a functor from a category to itself) for a non-empty category, then the category is terminal. This partially explains why two categories are sufficient in termc2 . (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Hypotheses euendfunc.f 
|- ( ph -> E! f f e. ( C Func C ) )
euendfunc.b 
|- B = ( Base ` C )
euendfunc.0 
|- ( ph -> B =/= (/) )
Assertion euendfunc 
|- ( ph -> C e. TermCat )

Proof

Step Hyp Ref Expression
1 euendfunc.f 
 |-  ( ph -> E! f f e. ( C Func C ) )
2 euendfunc.b 
 |-  B = ( Base ` C )
3 euendfunc.0 
 |-  ( ph -> B =/= (/) )
4 n0 
 |-  ( B =/= (/) <-> E. x x e. B )
5 3 4 sylib 
 |-  ( ph -> E. x x e. B )
6 eqid 
 |-  ( idFunc ` C ) = ( idFunc ` C )
7 eqid 
 |-  ( C DiagFunc C ) = ( C DiagFunc C )
8 1 adantr 
 |-  ( ( ph /\ x e. B ) -> E! f f e. ( C Func C ) )
9 euex 
 |-  ( E! f f e. ( C Func C ) -> E. f f e. ( C Func C ) )
10 8 9 syl 
 |-  ( ( ph /\ x e. B ) -> E. f f e. ( C Func C ) )
11 funcrcl 
 |-  ( f e. ( C Func C ) -> ( C e. Cat /\ C e. Cat ) )
12 11 simpld 
 |-  ( f e. ( C Func C ) -> C e. Cat )
13 12 exlimiv 
 |-  ( E. f f e. ( C Func C ) -> C e. Cat )
14 10 13 syl 
 |-  ( ( ph /\ x e. B ) -> C e. Cat )
15 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
16 eqid 
 |-  ( ( 1st ` ( C DiagFunc C ) ) ` x ) = ( ( 1st ` ( C DiagFunc C ) ) ` x )
17 6 idfucl 
 |-  ( C e. Cat -> ( idFunc ` C ) e. ( C Func C ) )
18 14 17 syl 
 |-  ( ( ph /\ x e. B ) -> ( idFunc ` C ) e. ( C Func C ) )
19 7 14 14 2 15 16 diag1cl 
 |-  ( ( ph /\ x e. B ) -> ( ( 1st ` ( C DiagFunc C ) ) ` x ) e. ( C Func C ) )
20 eumo 
 |-  ( E! f f e. ( C Func C ) -> E* f f e. ( C Func C ) )
21 8 20 syl 
 |-  ( ( ph /\ x e. B ) -> E* f f e. ( C Func C ) )
22 eleq1w 
 |-  ( f = g -> ( f e. ( C Func C ) <-> g e. ( C Func C ) ) )
23 22 mo4 
 |-  ( E* f f e. ( C Func C ) <-> A. f A. g ( ( f e. ( C Func C ) /\ g e. ( C Func C ) ) -> f = g ) )
24 21 23 sylib 
 |-  ( ( ph /\ x e. B ) -> A. f A. g ( ( f e. ( C Func C ) /\ g e. ( C Func C ) ) -> f = g ) )
25 fvex 
 |-  ( idFunc ` C ) e. _V
26 fvex 
 |-  ( ( 1st ` ( C DiagFunc C ) ) ` x ) e. _V
27 simpl 
 |-  ( ( f = ( idFunc ` C ) /\ g = ( ( 1st ` ( C DiagFunc C ) ) ` x ) ) -> f = ( idFunc ` C ) )
28 27 eleq1d 
 |-  ( ( f = ( idFunc ` C ) /\ g = ( ( 1st ` ( C DiagFunc C ) ) ` x ) ) -> ( f e. ( C Func C ) <-> ( idFunc ` C ) e. ( C Func C ) ) )
29 simpr 
 |-  ( ( f = ( idFunc ` C ) /\ g = ( ( 1st ` ( C DiagFunc C ) ) ` x ) ) -> g = ( ( 1st ` ( C DiagFunc C ) ) ` x ) )
30 29 eleq1d 
 |-  ( ( f = ( idFunc ` C ) /\ g = ( ( 1st ` ( C DiagFunc C ) ) ` x ) ) -> ( g e. ( C Func C ) <-> ( ( 1st ` ( C DiagFunc C ) ) ` x ) e. ( C Func C ) ) )
31 28 30 anbi12d 
 |-  ( ( f = ( idFunc ` C ) /\ g = ( ( 1st ` ( C DiagFunc C ) ) ` x ) ) -> ( ( f e. ( C Func C ) /\ g e. ( C Func C ) ) <-> ( ( idFunc ` C ) e. ( C Func C ) /\ ( ( 1st ` ( C DiagFunc C ) ) ` x ) e. ( C Func C ) ) ) )
32 eqeq12 
 |-  ( ( f = ( idFunc ` C ) /\ g = ( ( 1st ` ( C DiagFunc C ) ) ` x ) ) -> ( f = g <-> ( idFunc ` C ) = ( ( 1st ` ( C DiagFunc C ) ) ` x ) ) )
33 31 32 imbi12d 
 |-  ( ( f = ( idFunc ` C ) /\ g = ( ( 1st ` ( C DiagFunc C ) ) ` x ) ) -> ( ( ( f e. ( C Func C ) /\ g e. ( C Func C ) ) -> f = g ) <-> ( ( ( idFunc ` C ) e. ( C Func C ) /\ ( ( 1st ` ( C DiagFunc C ) ) ` x ) e. ( C Func C ) ) -> ( idFunc ` C ) = ( ( 1st ` ( C DiagFunc C ) ) ` x ) ) ) )
34 33 spc2gv 
 |-  ( ( ( idFunc ` C ) e. _V /\ ( ( 1st ` ( C DiagFunc C ) ) ` x ) e. _V ) -> ( A. f A. g ( ( f e. ( C Func C ) /\ g e. ( C Func C ) ) -> f = g ) -> ( ( ( idFunc ` C ) e. ( C Func C ) /\ ( ( 1st ` ( C DiagFunc C ) ) ` x ) e. ( C Func C ) ) -> ( idFunc ` C ) = ( ( 1st ` ( C DiagFunc C ) ) ` x ) ) ) )
35 25 26 34 mp2an 
 |-  ( A. f A. g ( ( f e. ( C Func C ) /\ g e. ( C Func C ) ) -> f = g ) -> ( ( ( idFunc ` C ) e. ( C Func C ) /\ ( ( 1st ` ( C DiagFunc C ) ) ` x ) e. ( C Func C ) ) -> ( idFunc ` C ) = ( ( 1st ` ( C DiagFunc C ) ) ` x ) ) )
36 24 35 syl 
 |-  ( ( ph /\ x e. B ) -> ( ( ( idFunc ` C ) e. ( C Func C ) /\ ( ( 1st ` ( C DiagFunc C ) ) ` x ) e. ( C Func C ) ) -> ( idFunc ` C ) = ( ( 1st ` ( C DiagFunc C ) ) ` x ) ) )
37 18 19 36 mp2and 
 |-  ( ( ph /\ x e. B ) -> ( idFunc ` C ) = ( ( 1st ` ( C DiagFunc C ) ) ` x ) )
38 6 7 14 2 15 16 37 idfudiag1 
 |-  ( ( ph /\ x e. B ) -> C e. TermCat )
39 5 38 exlimddv 
 |-  ( ph -> C e. TermCat )