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

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. Note that the converse also holds, so that it is a biconditional. See the proof of termc for hints. See also eufunc and euendfunc2 for some insights on why two categories are sufficient. (Contributed by Zhi Wang, 18-Oct-2025) (Proof shortened by Zhi Wang, 20-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 funcrcl 
 |-  ( f e. ( ( SetCat ` 1o ) Func C ) -> ( ( SetCat ` 1o ) e. Cat /\ C e. Cat ) )
31 30 simprd 
 |-  ( f e. ( ( SetCat ` 1o ) Func C ) -> C e. Cat )
32 31 exlimiv 
 |-  ( E. f f e. ( ( SetCat ` 1o ) Func C ) -> C e. Cat )
33 29 32 syl 
 |-  ( E! f f e. ( ( SetCat ` 1o ) Func C ) -> C e. Cat )
34 17 33 sylbi 
 |-  ( ( ( SetCat ` 1o ) Func C ) ~~ 1o -> C e. Cat )
35 prid1g 
 |-  ( C e. Cat -> C e. { C , ( SetCat ` 1o ) } )
36 34 35 syl 
 |-  ( ( ( SetCat ` 1o ) Func C ) ~~ 1o -> C e. { C , ( SetCat ` 1o ) } )
37 36 34 elind 
 |-  ( ( ( SetCat ` 1o ) Func C ) ~~ 1o -> C e. ( { C , ( SetCat ` 1o ) } i^i Cat ) )
38 24 25 28 37 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 ) ) )
39 20 a1i 
 |-  ( ( ( ( SetCat ` 1o ) Func C ) ~~ 1o /\ d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) ) -> { C , ( SetCat ` 1o ) } e. _V )
40 simpr 
 |-  ( ( ( ( SetCat ` 1o ) Func C ) ~~ 1o /\ d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) ) -> d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) )
41 37 adantr 
 |-  ( ( ( ( SetCat ` 1o ) Func C ) ~~ 1o /\ d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) ) -> C e. ( { C , ( SetCat ` 1o ) } i^i Cat ) )
42 1 24 39 25 40 41 catchom 
 |-  ( ( ( ( SetCat ` 1o ) Func C ) ~~ 1o /\ d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) ) -> ( d ( Hom ` ( CatCat ` { C , ( SetCat ` 1o ) } ) ) C ) = ( d Func C ) )
43 42 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 ) ) )
44 43 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 ) ) )
45 44 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 ) ) )
46 38 45 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 ) ) )
47 18 46 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 ) ) )
48 47 ibir 
 |-  ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> C e. ( TermO ` ( CatCat ` { C , ( SetCat ` 1o ) } ) ) )
49 1 7 48 termcterm2 
 |-  ( A. d e. ( { C , ( SetCat ` 1o ) } i^i Cat ) E! f f e. ( d Func C ) -> C e. TermCat )