Metamath Proof Explorer

Theorem termcterm

Description: A terminal category is a terminal object of the category of small categories. (Contributed by Zhi Wang, 17-Oct-2025)

Ref Expression
Hypotheses termcterm.e 
|- E = ( CatCat ` U )
termcterm.u 
|- ( ph -> U e. V )
termcterm.c 
|- ( ph -> C e. U )
termcterm.t 
|- ( ph -> C e. TermCat )
Assertion termcterm 
|- ( ph -> C e. ( TermO ` E ) )

Proof

Step Hyp Ref Expression
1 termcterm.e 
 |-  E = ( CatCat ` U )
2 termcterm.u 
 |-  ( ph -> U e. V )
3 termcterm.c 
 |-  ( ph -> C e. U )
4 termcterm.t 
 |-  ( ph -> C e. TermCat )
5 simpr 
 |-  ( ( ph /\ d e. ( Base ` E ) ) -> d e. ( Base ` E ) )
6 eqid 
 |-  ( Base ` E ) = ( Base ` E )
7 1 6 2 catcbas 
 |-  ( ph -> ( Base ` E ) = ( U i^i Cat ) )
8 7 adantr 
 |-  ( ( ph /\ d e. ( Base ` E ) ) -> ( Base ` E ) = ( U i^i Cat ) )
9 5 8 eleqtrd 
 |-  ( ( ph /\ d e. ( Base ` E ) ) -> d e. ( U i^i Cat ) )
10 9 elin2d 
 |-  ( ( ph /\ d e. ( Base ` E ) ) -> d e. Cat )
11 4 adantr 
 |-  ( ( ph /\ d e. ( Base ` E ) ) -> C e. TermCat )
12 10 11 functermceu 
 |-  ( ( ph /\ d e. ( Base ` E ) ) -> E! f f e. ( d Func C ) )
13 2 adantr 
 |-  ( ( ph /\ d e. ( Base ` E ) ) -> U e. V )
14 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
15 4 termccd 
 |-  ( ph -> C e. Cat )
16 3 15 elind 
 |-  ( ph -> C e. ( U i^i Cat ) )
17 16 7 eleqtrrd 
 |-  ( ph -> C e. ( Base ` E ) )
18 17 adantr 
 |-  ( ( ph /\ d e. ( Base ` E ) ) -> C e. ( Base ` E ) )
19 1 6 13 14 5 18 catchom 
 |-  ( ( ph /\ d e. ( Base ` E ) ) -> ( d ( Hom ` E ) C ) = ( d Func C ) )
20 19 eleq2d 
 |-  ( ( ph /\ d e. ( Base ` E ) ) -> ( f e. ( d ( Hom ` E ) C ) <-> f e. ( d Func C ) ) )
21 20 eubidv 
 |-  ( ( ph /\ d e. ( Base ` E ) ) -> ( E! f f e. ( d ( Hom ` E ) C ) <-> E! f f e. ( d Func C ) ) )
22 12 21 mpbird 
 |-  ( ( ph /\ d e. ( Base ` E ) ) -> E! f f e. ( d ( Hom ` E ) C ) )
23 22 ralrimiva 
 |-  ( ph -> A. d e. ( Base ` E ) E! f f e. ( d ( Hom ` E ) C ) )
24 1 catccat 
 |-  ( U e. V -> E e. Cat )
25 2 24 syl 
 |-  ( ph -> E e. Cat )
26 6 14 25 17 istermo 
 |-  ( ph -> ( C e. ( TermO ` E ) <-> A. d e. ( Base ` E ) E! f f e. ( d ( Hom ` E ) C ) ) )
27 23 26 mpbird 
 |-  ( ph -> C e. ( TermO ` E ) )