Metamath Proof Explorer

Theorem termcterm2

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

Ref Expression
Hypotheses termcterm.e 
|- E = ( CatCat ` U )
termcterm2. 
|- ( ph -> ( U i^i TermCat ) =/= (/) )
termcterm2.t 
|- ( ph -> C e. ( TermO ` E ) )
Assertion termcterm2 
|- ( ph -> C e. TermCat )

Proof

Step Hyp Ref Expression
1 termcterm.e 
 |-  E = ( CatCat ` U )
2 termcterm2. 
 |-  ( ph -> ( U i^i TermCat ) =/= (/) )
3 termcterm2.t 
 |-  ( ph -> C e. ( TermO ` E ) )
4 n0 
 |-  ( ( U i^i TermCat ) =/= (/) <-> E. d d e. ( U i^i TermCat ) )
5 2 4 sylib 
 |-  ( ph -> E. d d e. ( U i^i TermCat ) )
6 simpr 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ( U i^i TermCat ) )
7 6 elin2d 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. TermCat )
8 7 termcthind 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ThinCat )
9 eqid 
 |-  ( Base ` E ) = ( Base ` E )
10 3 adantr 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> C e. ( TermO ` E ) )
11 9 termoo2 
 |-  ( C e. ( TermO ` E ) -> C e. ( Base ` E ) )
12 10 11 syl 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> C e. ( Base ` E ) )
13 1 9 elbasfv 
 |-  ( C e. ( Base ` E ) -> U e. _V )
14 12 13 syl 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> U e. _V )
15 6 elin1d 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. U )
16 7 termccd 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. Cat )
17 15 16 elind 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ( U i^i Cat ) )
18 1 9 14 catcbas 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` E ) = ( U i^i Cat ) )
19 17 18 eleqtrrd 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ( Base ` E ) )
20 termorcl 
 |-  ( C e. ( TermO ` E ) -> E e. Cat )
21 10 20 syl 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> E e. Cat )
22 1 14 15 7 termcterm 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ( TermO ` E ) )
23 21 10 22 termoeu1w 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> C ( ~=c ` E ) d )
24 1 9 14 12 19 23 thincciso4 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( C e. ThinCat <-> d e. ThinCat ) )
25 8 24 mpbird 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> C e. ThinCat )
26 21 10 22 termoeu1 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> E! f f e. ( C ( Iso ` E ) d ) )
27 euex 
 |-  ( E! f f e. ( C ( Iso ` E ) d ) -> E. f f e. ( C ( Iso ` E ) d ) )
28 26 27 syl 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> E. f f e. ( C ( Iso ` E ) d ) )
29 eqid 
 |-  ( Base ` C ) = ( Base ` C )
30 eqid 
 |-  ( Base ` d ) = ( Base ` d )
31 eqid 
 |-  ( Iso ` E ) = ( Iso ` E )
32 1 9 29 30 14 12 19 31 catciso 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( f e. ( C ( Iso ` E ) d ) <-> ( f e. ( ( C Full d ) i^i ( C Faith d ) ) /\ ( 1st ` f ) : ( Base ` C ) -1-1-onto-> ( Base ` d ) ) ) )
33 32 simplbda 
 |-  ( ( ( ph /\ d e. ( U i^i TermCat ) ) /\ f e. ( C ( Iso ` E ) d ) ) -> ( 1st ` f ) : ( Base ` C ) -1-1-onto-> ( Base ` d ) )
34 fvex 
 |-  ( Base ` C ) e. _V
35 34 f1oen 
 |-  ( ( 1st ` f ) : ( Base ` C ) -1-1-onto-> ( Base ` d ) -> ( Base ` C ) ~~ ( Base ` d ) )
36 33 35 syl 
 |-  ( ( ( ph /\ d e. ( U i^i TermCat ) ) /\ f e. ( C ( Iso ` E ) d ) ) -> ( Base ` C ) ~~ ( Base ` d ) )
37 28 36 exlimddv 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` C ) ~~ ( Base ` d ) )
38 30 istermc3 
 |-  ( d e. TermCat <-> ( d e. ThinCat /\ ( Base ` d ) ~~ 1o ) )
39 7 38 sylib 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( d e. ThinCat /\ ( Base ` d ) ~~ 1o ) )
40 39 simprd 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` d ) ~~ 1o )
41 entr 
 |-  ( ( ( Base ` C ) ~~ ( Base ` d ) /\ ( Base ` d ) ~~ 1o ) -> ( Base ` C ) ~~ 1o )
42 37 40 41 syl2anc 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` C ) ~~ 1o )
43 29 istermc3 
 |-  ( C e. TermCat <-> ( C e. ThinCat /\ ( Base ` C ) ~~ 1o ) )
44 25 42 43 sylanbrc 
 |-  ( ( ph /\ d e. ( U i^i TermCat ) ) -> C e. TermCat )
45 5 44 exlimddv 
 |-  ( ph -> C e. TermCat )