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=\mathrm{CatCat}\left(U\right)$$
	termcterm2.	No typesetting found for |- ( ph -> ( U i^i TermCat ) =/= (/) ) with typecode |-
	termcterm2.t	$$⊢\phi \to C\in \mathrm{TermO}\left(E\right)$$
Assertion	termcterm2	Could not format assertion : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		termcterm.e	$$⊢E=\mathrm{CatCat}\left(U\right)$$
2		termcterm2.	Could not format ( ph -> ( U i^i TermCat ) =/= (/) ) : No typesetting found for |- ( ph -> ( U i^i TermCat ) =/= (/) ) with typecode |-
3		termcterm2.t	$$⊢\phi \to C\in \mathrm{TermO}\left(E\right)$$
4		n0	Could not format ( ( U i^i TermCat ) =/= (/) <-> E. d d e. ( U i^i TermCat ) ) : No typesetting found for |- ( ( U i^i TermCat ) =/= (/) <-> E. d d e. ( U i^i TermCat ) ) with typecode |-
5	2 4	sylib	Could not format ( ph -> E. d d e. ( U i^i TermCat ) ) : No typesetting found for |- ( ph -> E. d d e. ( U i^i TermCat ) ) with typecode |-
6		simpr	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ( U i^i TermCat ) ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ( U i^i TermCat ) ) with typecode |-
7	6	elin2d	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. TermCat ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. TermCat ) with typecode |-
8	7	termcthind	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ThinCat ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ThinCat ) with typecode |-
9		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
10	3	adantr	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> C e. ( TermO ` E ) ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> C e. ( TermO ` E ) ) with typecode |-
11		eqid	$$⊢\mathrm{Hom}\left(E\right)=\mathrm{Hom}\left(E\right)$$
12		termorcl	$$⊢C\in \mathrm{TermO}\left(E\right)\to E\in \mathrm{Cat}$$
13	10 12	syl	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> E e. Cat ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> E e. Cat ) with typecode |-
14	9 11 13	istermoi	Could not format ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) with typecode |-
15	10 14	mpdan	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( C e. ( Base ` E ) /\ A. d e. ( Base ` E ) E! f f e. ( d ( Hom ` E ) C ) ) ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( C e. ( Base ` E ) /\ A. d e. ( Base ` E ) E! f f e. ( d ( Hom ` E ) C ) ) ) with typecode |-
16	15	simpld	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> C e. ( Base ` E ) ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> C e. ( Base ` E ) ) with typecode |-
17	1 9	elbasfv	$$⊢C\in {\mathrm{Base}}_E\to U\in \mathrm{V}$$
18	16 17	syl	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> U e. _V ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> U e. _V ) with typecode |-
19	6	elin1d	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. U ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. U ) with typecode |-
20	7	termccd	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. Cat ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. Cat ) with typecode |-
21	19 20	elind	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ( U i^i Cat ) ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ( U i^i Cat ) ) with typecode |-
22	1 9 18	catcbas	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` E ) = ( U i^i Cat ) ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` E ) = ( U i^i Cat ) ) with typecode |-
23	21 22	eleqtrrd	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ( Base ` E ) ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ( Base ` E ) ) with typecode |-
24	1 18 19 7	termcterm	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ( TermO ` E ) ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> d e. ( TermO ` E ) ) with typecode |-
25	13 10 24	termoeu1w	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> C ( ~=c ` E ) d ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> C ( ~=c ` E ) d ) with typecode |-
26	1 9 18 16 23 25	thincciso4	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( C e. ThinCat <-> d e. ThinCat ) ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( C e. ThinCat <-> d e. ThinCat ) ) with typecode |-
27	8 26	mpbird	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> C e. ThinCat ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> C e. ThinCat ) with typecode |-
28	13 10 24	termoeu1	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> E! f f e. ( C ( Iso ` E ) d ) ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> E! f f e. ( C ( Iso ` E ) d ) ) with typecode |-
29		euex	$$⊢\exists !ff\in \left(C\mathrm{Iso}\left(E\right)d\right)\to \exists ff\in \left(C\mathrm{Iso}\left(E\right)d\right)$$
30	28 29	syl	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> E. f f e. ( C ( Iso ` E ) d ) ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> E. f f e. ( C ( Iso ` E ) d ) ) with typecode |-
31		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
32		eqid	$$⊢{\mathrm{Base}}_d={\mathrm{Base}}_d$$
33		eqid	$$⊢\mathrm{Iso}\left(E\right)=\mathrm{Iso}\left(E\right)$$
34	1 9 31 32 18 16 23 33	catciso	Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
35	34	simplbda	Could not format ( ( ( ph /\ d e. ( U i^i TermCat ) ) /\ f e. ( C ( Iso ` E ) d ) ) -> ( 1st ` f ) : ( Base ` C ) -1-1-onto-> ( Base ` d ) ) : No typesetting found for |- ( ( ( ph /\ d e. ( U i^i TermCat ) ) /\ f e. ( C ( Iso ` E ) d ) ) -> ( 1st ` f ) : ( Base ` C ) -1-1-onto-> ( Base ` d ) ) with typecode |-
36		fvex	$$⊢{\mathrm{Base}}_C\in \mathrm{V}$$
37	36	f1oen	$$⊢1^{st}\left(f\right):{\mathrm{Base}}_C\underset{1-1\; onto}{⟶}{\mathrm{Base}}_d\to {\mathrm{Base}}_C\approx {\mathrm{Base}}_d$$
38	35 37	syl	Could not format ( ( ( ph /\ d e. ( U i^i TermCat ) ) /\ f e. ( C ( Iso ` E ) d ) ) -> ( Base ` C ) ~~ ( Base ` d ) ) : No typesetting found for |- ( ( ( ph /\ d e. ( U i^i TermCat ) ) /\ f e. ( C ( Iso ` E ) d ) ) -> ( Base ` C ) ~~ ( Base ` d ) ) with typecode |-
39	30 38	exlimddv	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` C ) ~~ ( Base ` d ) ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` C ) ~~ ( Base ` d ) ) with typecode |-
40	32	istermc3	Could not format ( d e. TermCat <-> ( d e. ThinCat /\ ( Base ` d ) ~~ 1o ) ) : No typesetting found for |- ( d e. TermCat <-> ( d e. ThinCat /\ ( Base ` d ) ~~ 1o ) ) with typecode |-
41	7 40	sylib	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( d e. ThinCat /\ ( Base ` d ) ~~ 1o ) ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( d e. ThinCat /\ ( Base ` d ) ~~ 1o ) ) with typecode |-
42	41	simprd	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` d ) ~~ 1o ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` d ) ~~ 1o ) with typecode |-
43		entr	$$⊢\left({\mathrm{Base}}_C\approx {\mathrm{Base}}_d\wedge {\mathrm{Base}}_d\approx 1_{𝑜}\right)\to {\mathrm{Base}}_C\approx 1_{𝑜}$$
44	39 42 43	syl2anc	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` C ) ~~ 1o ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> ( Base ` C ) ~~ 1o ) with typecode |-
45	31	istermc3	Could not format ( C e. TermCat <-> ( C e. ThinCat /\ ( Base ` C ) ~~ 1o ) ) : No typesetting found for |- ( C e. TermCat <-> ( C e. ThinCat /\ ( Base ` C ) ~~ 1o ) ) with typecode |-
46	27 44 45	sylanbrc	Could not format ( ( ph /\ d e. ( U i^i TermCat ) ) -> C e. TermCat ) : No typesetting found for |- ( ( ph /\ d e. ( U i^i TermCat ) ) -> C e. TermCat ) with typecode |-
47	5 46	exlimddv	Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-