Metamath Proof Explorer

Theorem termc2

Description: If there exists a unique functor from both the category itself and the trivial category, then the category is terminal. (Contributed by Zhi Wang, 18-Oct-2025)

Ref Expression
Assertion termc2 
|- ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> C e. TermCat )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( CatCat ` { C , ( SetCat ` 1o ) } ) = ( CatCat ` { C , ( SetCat ` 1o ) } )
2 fvex 
 |-  ( SetCat ` 1o ) e. _V
3 2 prid2 
 |-  ( SetCat ` 1o ) e. { C , ( SetCat ` 1o ) }
4 setc1oterm 
 |-  ( SetCat ` 1o ) e. TermCat
5 3 4 elini 
 |-  ( SetCat ` 1o ) e. ( { C , ( SetCat ` 1o ) } i^i TermCat )
6 5 ne0ii 
 |-  ( { C , ( SetCat ` 1o ) } i^i TermCat ) =/= (/)
7 6 a1i 
 |-  ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> ( { C , ( SetCat ` 1o ) } i^i TermCat ) =/= (/) )
8 4 a1i 
 |-  ( T. -> ( SetCat ` 1o ) e. TermCat )
9 8 termccd 
 |-  ( T. -> ( SetCat ` 1o ) e. Cat )
10 9 mptru 
 |-  ( SetCat ` 1o ) e. Cat
11 3 10 elini 
 |-  ( SetCat ` 1o ) e. ( { C , ( SetCat ` 1o ) } i^i Cat )
12 oveq1 
 |-  ( d = ( SetCat ` 1o ) -> ( d Func C ) = ( ( SetCat ` 1o ) Func C ) )
13 12 eleq2d 
 |-  ( d = ( SetCat ` 1o ) -> ( f e. ( d Func C ) <-> f e. ( ( SetCat ` 1o ) Func C ) ) )
14 13 eubidv 
 |-  ( d = ( SetCat ` 1o ) -> ( E! f f e. ( d Func C ) <-> E! f f e. ( ( SetCat ` 1o ) Func C ) ) )
15 14 rspcv 
 |-  ( ( SetCat ` 1o ) e. ( { C , ( SetCat ` 1o ) } i^i Cat ) -> ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> E! f f e. ( ( SetCat ` 1o ) Func C ) ) )
16 11 15 ax-mp 
 |-  ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> E! f f e. ( ( SetCat ` 1o ) Func C ) )
17 euen1b 
 |-  ( ( ( SetCat ` 1o ) Func C ) ~~ 1o <-> E! f f e. ( ( SetCat ` 1o ) Func C ) )
18 16 17 sylibr 
 |-  ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> ( ( SetCat ` 1o ) Func C ) ~~ 1o )
19 eqid 
 |-  ( Base ` ( CatCat ` { C , ( SetCat ` 1o ) } ) ) = ( Base ` ( CatCat ` { C , ( SetCat ` 1o ) } ) )
20 prex 
 |-  { C , ( SetCat ` 1o ) } e. _V
21 20 a1i 
 |-  ( T. -> { C , ( SetCat ` 1o ) } e. _V )
22 1 19 21 catcbas 
 |-  ( T. -> ( Base ` ( CatCat ` { C , ( SetCat ` 1o ) } ) ) = ( { C , ( SetCat ` 1o ) } i^i Cat ) )
23 22 mptru 
 |-  ( Base ` ( CatCat ` { C , ( SetCat ` 1o ) } ) ) = ( { C , ( SetCat ` 1o ) } i^i Cat )
24 23 eqcomi 
 |-  ( { C , ( SetCat ` 1o ) } i^i Cat ) = ( Base ` ( CatCat ` { C , ( SetCat ` 1o ) } ) )
25 eqid 
 |-  ( Hom ` ( CatCat ` { C , ( SetCat ` 1o ) } ) ) = ( Hom ` ( CatCat ` { C , ( SetCat ` 1o ) } ) )
26 1 catccat 
 |-  ( { C , ( SetCat ` 1o ) } e. _V -> ( CatCat ` { C , ( SetCat ` 1o ) } ) e. Cat )
27 20 26 ax-mp 
 |-  ( CatCat ` { C , ( SetCat ` 1o ) } ) e. Cat
28 27 a1i 
 |-  ( ( ( SetCat ` 1o ) Func C ) ~~ 1o -> ( CatCat ` { C , ( SetCat ` 1o ) } ) e. Cat )
29 euex 
 |-  ( E! f f e. ( ( SetCat ` 1o ) Func C ) -> E. f f e. ( ( SetCat ` 1o ) Func C ) )
30 relfunc 
 |-  Rel ( ( SetCat ` 1o ) Func C )
31 1st2ndbr 
 |-  ( ( Rel ( ( SetCat ` 1o ) Func C ) /\ f e. ( ( SetCat ` 1o ) Func C ) ) -> ( 1st ` f ) ( ( SetCat ` 1o ) Func C ) ( 2nd ` f ) )
32 30 31 mpan 
 |-  ( f e. ( ( SetCat ` 1o ) Func C ) -> ( 1st ` f ) ( ( SetCat ` 1o ) Func C ) ( 2nd ` f ) )
33 32 funcrcl3 
 |-  ( f e. ( ( SetCat ` 1o ) Func C ) -> C e. Cat )
34 33 exlimiv 
 |-  ( E. f f e. ( ( SetCat ` 1o ) Func C ) -> C e. Cat )
35 29 34 syl 
 |-  ( E! f f e. ( ( SetCat ` 1o ) Func C ) -> C e. Cat )
36 17 35 sylbi 
 |-  ( ( ( SetCat ` 1o ) Func C ) ~~ 1o -> C e. Cat )
37 prid1g 
 |-  ( C e. Cat -> C e. { C , ( SetCat ` 1o ) } )
38 36 37 syl 
 |-  ( ( ( SetCat ` 1o ) Func C ) ~~ 1o -> C e. { C , ( SetCat ` 1o ) } )
39 38 36 elind 
 |-  ( ( ( SetCat ` 1o ) Func C ) ~~ 1o -> C e. ( { C , ( SetCat ` 1o ) } i^i Cat ) )
40 24 25 28 39 istermo 
 |-  ( ( ( SetCat ` 1o ) Func C ) ~~ 1o -> ( C e. ( TermO ` ( CatCat ` { C , ( SetCat ` 1o ) } ) ) <-> A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d ( Hom ` ( CatCat ` { C , ( SetCat ` 1o ) } ) ) C ) ) )
41 20 a1i 
 |-  ( ( ( ( SetCat ` 1o ) Func C ) ~~ 1o /\ d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) ) -> { C , ( SetCat ` 1o ) } e. _V )
42 simpr 
 |-  ( ( ( ( SetCat ` 1o ) Func C ) ~~ 1o /\ d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) ) -> d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) )
43 39 adantr 
 |-  ( ( ( ( SetCat ` 1o ) Func C ) ~~ 1o /\ d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) ) -> C e. ( { C , ( SetCat ` 1o ) } i^i Cat ) )
44 1 24 41 25 42 43 catchom 
 |-  ( ( ( ( SetCat ` 1o ) Func C ) ~~ 1o /\ d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) ) -> ( d ( Hom ` ( CatCat ` { C , ( SetCat ` 1o ) } ) ) C ) = ( d Func C ) )
45 44 eleq2d 
 |-  ( ( ( ( SetCat ` 1o ) Func C ) ~~ 1o /\ d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) ) -> ( f e. ( d ( Hom ` ( CatCat ` { C , ( SetCat ` 1o ) } ) ) C ) <-> f e. ( d Func C ) ) )
46 45 eubidv 
 |-  ( ( ( ( SetCat ` 1o ) Func C ) ~~ 1o /\ d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) ) -> ( E! f f e. ( d ( Hom ` ( CatCat ` { C , ( SetCat ` 1o ) } ) ) C ) <-> E! f f e. ( d Func C ) ) )
47 46 ralbidva 
 |-  ( ( ( SetCat ` 1o ) Func C ) ~~ 1o -> ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d ( Hom ` ( CatCat ` { C , ( SetCat ` 1o ) } ) ) C ) <-> A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) ) )
48 40 47 bitrd 
 |-  ( ( ( SetCat ` 1o ) Func C ) ~~ 1o -> ( C e. ( TermO ` ( CatCat ` { C , ( SetCat ` 1o ) } ) ) <-> A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) ) )
49 18 48 syl 
 |-  ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> ( C e. ( TermO ` ( CatCat ` { C , ( SetCat ` 1o ) } ) ) <-> A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) ) )
50 49 ibir 
 |-  ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> C e. ( TermO ` ( CatCat ` { C , ( SetCat ` 1o ) } ) ) )
51 1 7 50 termcterm2 
 |-  ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> C e. TermCat )