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=\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	9	termoo2	$$⊢C\in \mathrm{TermO}\left(E\right)\to C\in {\mathrm{Base}}_E$$
12	10 11	syl	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 |-
13	1 9	elbasfv	$$⊢C\in {\mathrm{Base}}_E\to U\in \mathrm{V}$$
14	12 13	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 |-
15	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 |-
16	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 |-
17	15 16	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 |-
18	1 9 14	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 |-
19	17 18	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 |-
20		termorcl	$$⊢C\in \mathrm{TermO}\left(E\right)\to E\in \mathrm{Cat}$$
21	10 20	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 |-
22	1 14 15 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 |-
23	21 10 22	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 |-
24	1 9 14 12 19 23	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 |-
25	8 24	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 |-
26	21 10 22	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 |-
27		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)$$
28	26 27	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 |-
29		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
30		eqid	$$⊢{\mathrm{Base}}_d={\mathrm{Base}}_d$$
31		eqid	$$⊢\mathrm{Iso}\left(E\right)=\mathrm{Iso}\left(E\right)$$
32	1 9 29 30 14 12 19 31	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 |-
33	32	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 |-
34		fvex	$$⊢{\mathrm{Base}}_C\in \mathrm{V}$$
35	34	f1oen	$$⊢1^{st}\left(f\right):{\mathrm{Base}}_C\underset{1-1\; onto}{⟶}{\mathrm{Base}}_d\to {\mathrm{Base}}_C\approx {\mathrm{Base}}_d$$
36	33 35	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 |-
37	28 36	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 |-
38	30	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 |-
39	7 38	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 |-
40	39	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 |-
41		entr	$$⊢\left({\mathrm{Base}}_C\approx {\mathrm{Base}}_d\wedge {\mathrm{Base}}_d\approx 1_{𝑜}\right)\to {\mathrm{Base}}_C\approx 1_{𝑜}$$
42	37 40 41	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 |-
43	29	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 |-
44	25 42 43	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 |-
45	5 44	exlimddv	Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-