Theorem initocmd

Description: Initial objects are the object part of colimits of the empty diagram. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Assertion	initocmd	Could not format assertion : No typesetting found for |- ( InitO ` C ) = dom ( (/) ( C Colimit (/) ) (/) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		initorcl	$$⊢x\in \mathrm{InitO}\left(C\right)\to C\in \mathrm{Cat}$$
2		uobrcl	Could not format ( x e. dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) -> ( C e. Cat /\ ( (/) FuncCat C ) e. Cat ) ) : No typesetting found for |- ( x e. dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) -> ( C e. Cat /\ ( (/) FuncCat C ) e. Cat ) ) with typecode |-
3	2	simpld	Could not format ( x e. dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) -> C e. Cat ) : No typesetting found for |- ( x e. dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) -> C e. Cat ) with typecode |-
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5	4	a1i	$$⊢C\in \mathrm{Cat}\to \varnothing \in \mathrm{V}$$
6		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
7	6	a1i	$$⊢C\in \mathrm{Cat}\to \varnothing ={\mathrm{Base}}_{\varnothing }$$
8		id	$$⊢C\in \mathrm{Cat}\to C\in \mathrm{Cat}$$
9		eqid	$$⊢\varnothing \mathrm{FuncCat}C=\varnothing \mathrm{FuncCat}C$$
10	5 7 8 9	0fucterm	Could not format ( C e. Cat -> ( (/) FuncCat C ) e. TermCat ) : No typesetting found for |- ( C e. Cat -> ( (/) FuncCat C ) e. TermCat ) with typecode |-
11		opex	$$⊢⟨\varnothing ,\varnothing ⟩\in \mathrm{V}$$
12	11	snid	$$⊢⟨\varnothing ,\varnothing ⟩\in \left\{⟨\varnothing ,\varnothing ⟩\right\}$$
13	9	fucbas	$$⊢\varnothing \mathrm{Func}C={\mathrm{Base}}_{\left(\varnothing \mathrm{FuncCat}C\right)}$$
14	8	0func	$$⊢C\in \mathrm{Cat}\to \varnothing \mathrm{Func}C=\left\{⟨\varnothing ,\varnothing ⟩\right\}$$
15	13 14	eqtr3id	$$⊢C\in \mathrm{Cat}\to {\mathrm{Base}}_{\left(\varnothing \mathrm{FuncCat}C\right)}=\left\{⟨\varnothing ,\varnothing ⟩\right\}$$
16	12 15	eleqtrrid	$$⊢C\in \mathrm{Cat}\to ⟨\varnothing ,\varnothing ⟩\in {\mathrm{Base}}_{\left(\varnothing \mathrm{FuncCat}C\right)}$$
17		eqid	$$⊢C{\Delta }_{\mathrm{func}}\varnothing =C{\Delta }_{\mathrm{func}}\varnothing$$
18		0cat	$$⊢\varnothing \in \mathrm{Cat}$$
19	18	a1i	$$⊢C\in \mathrm{Cat}\to \varnothing \in \mathrm{Cat}$$
20	17 8 19 9	diagcl	$$⊢C\in \mathrm{Cat}\to C{\Delta }_{\mathrm{func}}\varnothing \in \left(C\mathrm{Func}\left(\varnothing \mathrm{FuncCat}C\right)\right)$$
21	10 16 20	isinito4	Could not format ( C e. Cat -> ( x e. ( InitO ` C ) <-> x e. dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) ) ) : No typesetting found for |- ( C e. Cat -> ( x e. ( InitO ` C ) <-> x e. dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) ) ) with typecode |-
22	1 3 21	pm5.21nii	Could not format ( x e. ( InitO ` C ) <-> x e. dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) ) : No typesetting found for |- ( x e. ( InitO ` C ) <-> x e. dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) ) with typecode |-
23	22	eqriv	Could not format ( InitO ` C ) = dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) : No typesetting found for |- ( InitO ` C ) = dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) with typecode |-
24		df-ov	Could not format ( (/) ( C Colimit (/) ) (/) ) = ( ( C Colimit (/) ) ` <. (/) , (/) >. ) : No typesetting found for |- ( (/) ( C Colimit (/) ) (/) ) = ( ( C Colimit (/) ) ` <. (/) , (/) >. ) with typecode |-
25		cmdfval2	Could not format ( ( C Colimit (/) ) ` <. (/) , (/) >. ) = ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) : No typesetting found for |- ( ( C Colimit (/) ) ` <. (/) , (/) >. ) = ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) with typecode |-
26	24 25	eqtri	Could not format ( (/) ( C Colimit (/) ) (/) ) = ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) : No typesetting found for |- ( (/) ( C Colimit (/) ) (/) ) = ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) with typecode |-
27	26	dmeqi	Could not format dom ( (/) ( C Colimit (/) ) (/) ) = dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) : No typesetting found for |- dom ( (/) ( C Colimit (/) ) (/) ) = dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) with typecode |-
28	23 27	eqtr4i	Could not format ( InitO ` C ) = dom ( (/) ( C Colimit (/) ) (/) ) : No typesetting found for |- ( InitO ` C ) = dom ( (/) ( C Colimit (/) ) (/) ) with typecode |-