Theorem termolmd

Description: Terminal objects are the object part of limits of the empty diagram. (Contributed by Zhi Wang, 20-Nov-2025)

	Ref	Expression
Assertion	termolmd	Could not format assertion : No typesetting found for |- ( TermO ` C ) = dom ( (/) ( C Limit (/) ) (/) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		termorcl	$$⊢x\in \mathrm{TermO}\left(C\right)\to C\in \mathrm{Cat}$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	eldm	Could not format ( x e. dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) <-> E. y x ( ( C Limit (/) ) ` <. (/) , (/) >. ) y ) : No typesetting found for |- ( x e. dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) <-> E. y x ( ( C Limit (/) ) ` <. (/) , (/) >. ) y ) with typecode |-
4		df-br	Could not format ( x ( ( C Limit (/) ) ` <. (/) , (/) >. ) y <-> <. x , y >. e. ( ( C Limit (/) ) ` <. (/) , (/) >. ) ) : No typesetting found for |- ( x ( ( C Limit (/) ) ` <. (/) , (/) >. ) y <-> <. x , y >. e. ( ( C Limit (/) ) ` <. (/) , (/) >. ) ) with typecode |-
5		lmdrcl	Could not format ( <. x , y >. e. ( ( C Limit (/) ) ` <. (/) , (/) >. ) -> <. (/) , (/) >. e. ( (/) Func C ) ) : No typesetting found for |- ( <. x , y >. e. ( ( C Limit (/) ) ` <. (/) , (/) >. ) -> <. (/) , (/) >. e. ( (/) Func C ) ) with typecode |-
6	4 5	sylbi	Could not format ( x ( ( C Limit (/) ) ` <. (/) , (/) >. ) y -> <. (/) , (/) >. e. ( (/) Func C ) ) : No typesetting found for |- ( x ( ( C Limit (/) ) ` <. (/) , (/) >. ) y -> <. (/) , (/) >. e. ( (/) Func C ) ) with typecode |-
7	6	func1st2nd	Could not format ( x ( ( C Limit (/) ) ` <. (/) , (/) >. ) y -> ( 1st ` <. (/) , (/) >. ) ( (/) Func C ) ( 2nd ` <. (/) , (/) >. ) ) : No typesetting found for |- ( x ( ( C Limit (/) ) ` <. (/) , (/) >. ) y -> ( 1st ` <. (/) , (/) >. ) ( (/) Func C ) ( 2nd ` <. (/) , (/) >. ) ) with typecode |-
8	7	funcrcl3	Could not format ( x ( ( C Limit (/) ) ` <. (/) , (/) >. ) y -> C e. Cat ) : No typesetting found for |- ( x ( ( C Limit (/) ) ` <. (/) , (/) >. ) y -> C e. Cat ) with typecode |-
9	8	exlimiv	Could not format ( E. y x ( ( C Limit (/) ) ` <. (/) , (/) >. ) y -> C e. Cat ) : No typesetting found for |- ( E. y x ( ( C Limit (/) ) ` <. (/) , (/) >. ) y -> C e. Cat ) with typecode |-
10	3 9	sylbi	Could not format ( x e. dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) -> C e. Cat ) : No typesetting found for |- ( x e. dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) -> C e. Cat ) with typecode |-
11		initocmd	Could not format ( InitO ` ( oppCat ` C ) ) = dom ( (/) ( ( oppCat ` C ) Colimit (/) ) (/) ) : No typesetting found for |- ( InitO ` ( oppCat ` C ) ) = dom ( (/) ( ( oppCat ` C ) Colimit (/) ) (/) ) with typecode |-
12		oppctermo	$$⊢x\in \mathrm{TermO}\left(C\right)\leftrightarrow x\in \mathrm{InitO}\left(\mathrm{oppCat}\left(C\right)\right)$$
13	12	eqriv	$$⊢\mathrm{TermO}\left(C\right)=\mathrm{InitO}\left(\mathrm{oppCat}\left(C\right)\right)$$
14	13	a1i	$$⊢C\in \mathrm{Cat}\to \mathrm{TermO}\left(C\right)=\mathrm{InitO}\left(\mathrm{oppCat}\left(C\right)\right)$$
15		eqid	$$⊢\mathrm{oppCat}\left(C\right)=\mathrm{oppCat}\left(C\right)$$
16	15	2oppchomf	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(\mathrm{oppCat}\left(C\right)\right)\right)$$
17	16	a1i	$$⊢C\in \mathrm{Cat}\to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(\mathrm{oppCat}\left(C\right)\right)\right)$$
18	15	2oppccomf	$$⊢{\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(\mathrm{oppCat}\left(C\right)\right)\right)$$
19	18	a1i	$$⊢C\in \mathrm{Cat}\to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(\mathrm{oppCat}\left(C\right)\right)\right)$$
20		ral0	$$⊢\forall x\in \varnothing \forall y\in \varnothing x\mathrm{Hom}\left(\varnothing \right)y=x\mathrm{Hom}\left(\mathrm{oppCat}\left(\varnothing \right)\right)y$$
21		eqid	$$⊢\mathrm{Hom}\left(\varnothing \right)=\mathrm{Hom}\left(\varnothing \right)$$
22		eqid	$$⊢\mathrm{Hom}\left(\mathrm{oppCat}\left(\varnothing \right)\right)=\mathrm{Hom}\left(\mathrm{oppCat}\left(\varnothing \right)\right)$$
23		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
24	23	a1i	$$⊢C\in \mathrm{Cat}\to \varnothing ={\mathrm{Base}}_{\varnothing }$$
25		eqid	$$⊢\mathrm{oppCat}\left(\varnothing \right)=\mathrm{oppCat}\left(\varnothing \right)$$
26	25 23	oppcbas	$$⊢\varnothing ={\mathrm{Base}}_{\mathrm{oppCat}\left(\varnothing \right)}$$
27	26	a1i	$$⊢C\in \mathrm{Cat}\to \varnothing ={\mathrm{Base}}_{\mathrm{oppCat}\left(\varnothing \right)}$$
28	21 22 24 27	homfeq	$$⊢C\in \mathrm{Cat}\to \left({\mathrm{Hom}}_{𝑓}\left(\varnothing \right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(\varnothing \right)\right)\leftrightarrow \forall x\in \varnothing \forall y\in \varnothing x\mathrm{Hom}\left(\varnothing \right)y=x\mathrm{Hom}\left(\mathrm{oppCat}\left(\varnothing \right)\right)y\right)$$
29	20 28	mpbiri	$$⊢C\in \mathrm{Cat}\to {\mathrm{Hom}}_{𝑓}\left(\varnothing \right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(\varnothing \right)\right)$$
30		ral0	$$⊢\forall x\in \varnothing \forall y\in \varnothing \forall z\in \varnothing \forall f\in \left(x\mathrm{Hom}\left(\varnothing \right)y\right)\forall g\in \left(y\mathrm{Hom}\left(\varnothing \right)z\right)g\left(⟨x,y⟩\mathrm{comp}\left(\varnothing \right)z\right)f=g\left(⟨x,y⟩\mathrm{comp}\left(\mathrm{oppCat}\left(\varnothing \right)\right)z\right)f$$
31		eqid	$$⊢\mathrm{comp}\left(\varnothing \right)=\mathrm{comp}\left(\varnothing \right)$$
32		eqid	$$⊢\mathrm{comp}\left(\mathrm{oppCat}\left(\varnothing \right)\right)=\mathrm{comp}\left(\mathrm{oppCat}\left(\varnothing \right)\right)$$
33	31 32 21 24 27 29	comfeq	$$⊢C\in \mathrm{Cat}\to \left({\mathrm{comp}}_{𝑓}\left(\varnothing \right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(\varnothing \right)\right)\leftrightarrow \forall x\in \varnothing \forall y\in \varnothing \forall z\in \varnothing \forall f\in \left(x\mathrm{Hom}\left(\varnothing \right)y\right)\forall g\in \left(y\mathrm{Hom}\left(\varnothing \right)z\right)g\left(⟨x,y⟩\mathrm{comp}\left(\varnothing \right)z\right)f=g\left(⟨x,y⟩\mathrm{comp}\left(\mathrm{oppCat}\left(\varnothing \right)\right)z\right)f\right)$$
34	30 33	mpbiri	$$⊢C\in \mathrm{Cat}\to {\mathrm{comp}}_{𝑓}\left(\varnothing \right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(\varnothing \right)\right)$$
35		elex	$$⊢C\in \mathrm{Cat}\to C\in \mathrm{V}$$
36		fvexd	$$⊢C\in \mathrm{Cat}\to \mathrm{oppCat}\left(\mathrm{oppCat}\left(C\right)\right)\in \mathrm{V}$$
37		0ex	$$⊢\varnothing \in \mathrm{V}$$
38	37	a1i	$$⊢C\in \mathrm{Cat}\to \varnothing \in \mathrm{V}$$
39		fvexd	$$⊢C\in \mathrm{Cat}\to \mathrm{oppCat}\left(\varnothing \right)\in \mathrm{V}$$
40	17 19 29 34 35 36 38 39	lmdpropd	Could not format ( C e. Cat -> ( C Limit (/) ) = ( ( oppCat ` ( oppCat ` C ) ) Limit ( oppCat ` (/) ) ) ) : No typesetting found for |- ( C e. Cat -> ( C Limit (/) ) = ( ( oppCat ` ( oppCat ` C ) ) Limit ( oppCat ` (/) ) ) ) with typecode |-
41		eqidd	$$⊢C\in \mathrm{Cat}\to \varnothing =\varnothing$$
42		0cat	$$⊢\varnothing \in \mathrm{Cat}$$
43	42	a1i	$$⊢C\in \mathrm{Cat}\to \varnothing \in \mathrm{Cat}$$
44	43 24 43	0funcg2	$$⊢C\in \mathrm{Cat}\to \left(\varnothing \left(\varnothing \mathrm{Func}\varnothing \right)\varnothing \leftrightarrow \left(\varnothing =\varnothing \wedge \varnothing =\varnothing \right)\right)$$
45	41 41 44	mpbir2and	$$⊢C\in \mathrm{Cat}\to \varnothing \left(\varnothing \mathrm{Func}\varnothing \right)\varnothing$$
46		oppfval	Could not format ( (/) ( (/) Func (/) ) (/) -> ( (/) oppFunc (/) ) = <. (/) , tpos (/) >. ) : No typesetting found for |- ( (/) ( (/) Func (/) ) (/) -> ( (/) oppFunc (/) ) = <. (/) , tpos (/) >. ) with typecode |-
47	45 46	syl	Could not format ( C e. Cat -> ( (/) oppFunc (/) ) = <. (/) , tpos (/) >. ) : No typesetting found for |- ( C e. Cat -> ( (/) oppFunc (/) ) = <. (/) , tpos (/) >. ) with typecode |-
48		tpos0	$$⊢tpos\varnothing =\varnothing$$
49	48	opeq2i	$$⊢⟨\varnothing ,tpos\varnothing ⟩=⟨\varnothing ,\varnothing ⟩$$
50	47 49	eqtr2di	Could not format ( C e. Cat -> <. (/) , (/) >. = ( (/) oppFunc (/) ) ) : No typesetting found for |- ( C e. Cat -> <. (/) , (/) >. = ( (/) oppFunc (/) ) ) with typecode |-
51	40 50	fveq12d	Could not format ( C e. Cat -> ( ( C Limit (/) ) ` <. (/) , (/) >. ) = ( ( ( oppCat ` ( oppCat ` C ) ) Limit ( oppCat ` (/) ) ) ` ( (/) oppFunc (/) ) ) ) : No typesetting found for |- ( C e. Cat -> ( ( C Limit (/) ) ` <. (/) , (/) >. ) = ( ( ( oppCat ` ( oppCat ` C ) ) Limit ( oppCat ` (/) ) ) ` ( (/) oppFunc (/) ) ) ) with typecode |-
52		df-ov	Could not format ( (/) ( ( oppCat ` C ) Colimit (/) ) (/) ) = ( ( ( oppCat ` C ) Colimit (/) ) ` <. (/) , (/) >. ) : No typesetting found for |- ( (/) ( ( oppCat ` C ) Colimit (/) ) (/) ) = ( ( ( oppCat ` C ) Colimit (/) ) ` <. (/) , (/) >. ) with typecode |-
53		eqid	$$⊢\mathrm{oppCat}\left(\mathrm{oppCat}\left(C\right)\right)=\mathrm{oppCat}\left(\mathrm{oppCat}\left(C\right)\right)$$
54		df-ov	Could not format ( (/) oppFunc (/) ) = ( oppFunc ` <. (/) , (/) >. ) : No typesetting found for |- ( (/) oppFunc (/) ) = ( oppFunc ` <. (/) , (/) >. ) with typecode |-
55		fvexd	$$⊢C\in \mathrm{Cat}\to \mathrm{oppCat}\left(C\right)\in \mathrm{V}$$
56	53 25 54 55 38	cmddu	Could not format ( C e. Cat -> ( ( ( oppCat ` C ) Colimit (/) ) ` <. (/) , (/) >. ) = ( ( ( oppCat ` ( oppCat ` C ) ) Limit ( oppCat ` (/) ) ) ` ( (/) oppFunc (/) ) ) ) : No typesetting found for |- ( C e. Cat -> ( ( ( oppCat ` C ) Colimit (/) ) ` <. (/) , (/) >. ) = ( ( ( oppCat ` ( oppCat ` C ) ) Limit ( oppCat ` (/) ) ) ` ( (/) oppFunc (/) ) ) ) with typecode |-
57	52 56	eqtrid	Could not format ( C e. Cat -> ( (/) ( ( oppCat ` C ) Colimit (/) ) (/) ) = ( ( ( oppCat ` ( oppCat ` C ) ) Limit ( oppCat ` (/) ) ) ` ( (/) oppFunc (/) ) ) ) : No typesetting found for |- ( C e. Cat -> ( (/) ( ( oppCat ` C ) Colimit (/) ) (/) ) = ( ( ( oppCat ` ( oppCat ` C ) ) Limit ( oppCat ` (/) ) ) ` ( (/) oppFunc (/) ) ) ) with typecode |-
58	51 57	eqtr4d	Could not format ( C e. Cat -> ( ( C Limit (/) ) ` <. (/) , (/) >. ) = ( (/) ( ( oppCat ` C ) Colimit (/) ) (/) ) ) : No typesetting found for |- ( C e. Cat -> ( ( C Limit (/) ) ` <. (/) , (/) >. ) = ( (/) ( ( oppCat ` C ) Colimit (/) ) (/) ) ) with typecode |-
59	58	dmeqd	Could not format ( C e. Cat -> dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) = dom ( (/) ( ( oppCat ` C ) Colimit (/) ) (/) ) ) : No typesetting found for |- ( C e. Cat -> dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) = dom ( (/) ( ( oppCat ` C ) Colimit (/) ) (/) ) ) with typecode |-
60	11 14 59	3eqtr4a	Could not format ( C e. Cat -> ( TermO ` C ) = dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) ) : No typesetting found for |- ( C e. Cat -> ( TermO ` C ) = dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) ) with typecode |-
61	60	eleq2d	Could not format ( C e. Cat -> ( x e. ( TermO ` C ) <-> x e. dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) ) ) : No typesetting found for |- ( C e. Cat -> ( x e. ( TermO ` C ) <-> x e. dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) ) ) with typecode |-
62	1 10 61	pm5.21nii	Could not format ( x e. ( TermO ` C ) <-> x e. dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) ) : No typesetting found for |- ( x e. ( TermO ` C ) <-> x e. dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) ) with typecode |-
63	62	eqriv	Could not format ( TermO ` C ) = dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) : No typesetting found for |- ( TermO ` C ) = dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) with typecode |-
64		df-ov	Could not format ( (/) ( C Limit (/) ) (/) ) = ( ( C Limit (/) ) ` <. (/) , (/) >. ) : No typesetting found for |- ( (/) ( C Limit (/) ) (/) ) = ( ( C Limit (/) ) ` <. (/) , (/) >. ) with typecode |-
65	64	dmeqi	Could not format dom ( (/) ( C Limit (/) ) (/) ) = dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) : No typesetting found for |- dom ( (/) ( C Limit (/) ) (/) ) = dom ( ( C Limit (/) ) ` <. (/) , (/) >. ) with typecode |-
66	63 65	eqtr4i	Could not format ( TermO ` C ) = dom ( (/) ( C Limit (/) ) (/) ) : No typesetting found for |- ( TermO ` C ) = dom ( (/) ( C Limit (/) ) (/) ) with typecode |-