Theorem termcterm2

Description: A terminal object of the category of small categories is a terminal category. (Contributed by Zhi Wang, 18-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		eqid	|- ( Hom ` E ) = ( Hom ` E )
12		termorcl	|- ( C e. ( TermO ` E ) -> E e. Cat )
13	10 12	syl	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> E e. Cat )
14	9 11 13	istermoi	|- ( ( ( ph /\ d e. ( U i^i TermCat ) ) /\ C e. ( TermO ` E ) ) -> ( C e. ( Base ` E ) /\ A. d e. ( Base ` E ) E! f f e. ( d ( Hom ` E ) C ) ) )
15	10 14	mpdan	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( C e. ( Base ` E ) /\ A. d e. ( Base ` E ) E! f f e. ( d ( Hom ` E ) C ) ) )
16	15	simpld	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> C e. ( Base ` E ) )
17	1 9	elbasfv	|- ( C e. ( Base ` E ) -> U e. _V )
18	16 17	syl	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> U e. _V )
19	6	elin1d	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. U )
20	7	termccd	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. Cat )
21	19 20	elind	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ( U i^i Cat ) )
22	1 9 18	catcbas	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` E ) = ( U i^i Cat ) )
23	21 22	eleqtrrd	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ( Base ` E ) )
24	1 18 19 7	termcterm	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ( TermO ` E ) )
25	13 10 24	termoeu1w	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> C ( ~=c ` E ) d )
26	1 9 18 16 23 25	thincciso4	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( C e. ThinCat <-> d e. ThinCat ) )
27	8 26	mpbird	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> C e. ThinCat )
28	13 10 24	termoeu1	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> E! f f e. ( C ( Iso ` E ) d ) )
29		euex	|- ( E! f f e. ( C ( Iso ` E ) d ) -> E. f f e. ( C ( Iso ` E ) d ) )
30	28 29	syl	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> E. f f e. ( C ( Iso ` E ) d ) )
31		eqid	|- ( Base ` C ) = ( Base ` C )
32		eqid	|- ( Base ` d ) = ( Base ` d )
33		eqid	|- ( Iso ` E ) = ( Iso ` E )
34	1 9 31 32 18 16 23 33	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 ) ) ) )
35	34	simplbda	|- ( ( ( ph /\ d e. ( U i^i TermCat ) ) /\ f e. ( C ( Iso ` E ) d ) ) -> ( 1st ` f ) : ( Base ` C ) -1-1-onto-> ( Base ` d ) )
36		fvex	|- ( Base ` C ) e. _V
37	36	f1oen	|- ( ( 1st ` f ) : ( Base ` C ) -1-1-onto-> ( Base ` d ) -> ( Base ` C ) ~~ ( Base ` d ) )
38	35 37	syl	|- ( ( ( ph /\ d e. ( U i^i TermCat ) ) /\ f e. ( C ( Iso ` E ) d ) ) -> ( Base ` C ) ~~ ( Base ` d ) )
39	30 38	exlimddv	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` C ) ~~ ( Base ` d ) )
40	32	istermc3	|- ( d e. TermCat <-> ( d e. ThinCat /\ ( Base ` d ) ~~ 1o ) )
41	7 40	sylib	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( d e. ThinCat /\ ( Base ` d ) ~~ 1o ) )
42	41	simprd	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` d ) ~~ 1o )
43		entr	|- ( ( ( Base ` C ) ~~ ( Base ` d ) /\ ( Base ` d ) ~~ 1o ) -> ( Base ` C ) ~~ 1o )
44	39 42 43	syl2anc	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` C ) ~~ 1o )
45	31	istermc3	|- ( C e. TermCat <-> ( C e. ThinCat /\ ( Base ` C ) ~~ 1o ) )
46	27 44 45	sylanbrc	|- ( ( ph /\ d e. ( U i^i TermCat ) ) -> C e. TermCat )
47	5 46	exlimddv	|- ( ph -> C e. TermCat )