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.	No typesetting found for \|- ( ph -> ( U i^i TermCat ) =/= (/) ) with typecode \|-
	termcterm2.t	$⊢ φ \to C \in TermO (E)$
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 = CatCat (U)$
2		termcterm2.	Could not format ( ph -> ( U i^i TermCat ) =/= (/) ) : No typesetting found for \|- ( ph -> ( U i^i TermCat ) =/= (/) ) with typecode \|-
3		termcterm2.t	$⊢ φ \to C \in TermO (E)$
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	$⊢ {Base}_{E} = {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 TermO (E) \to C \in {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 {Base}_{E} \to U \in 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 TermO (E) \to E \in 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! f f \in (C Iso (E) d) \to \exists f f \in (C Iso (E) d)$
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	$⊢ {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	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	$⊢ {Base}_{C} \in V$
35	34	f1oen	$⊢ 1^{st} (f) : {Base}_{C} \underset{1-1 onto}{⟶} {Base}_{d} \to {Base}_{C} \approx {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	$⊢ ({Base}_{C} \approx {Base}_{d} \land {Base}_{d} \approx 1_{𝑜}) \to {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 \|-

Metamath Proof Explorer

Theorem termcterm2

Proof