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	⊢ ( InitO ‘ 𝐶 ) = dom ( ∅ ( 𝐶 Colimit ∅ ) ∅ )

Proof

Step	Hyp	Ref	Expression
1		initorcl	⊢ ( 𝑥 ∈ ( InitO ‘ 𝐶 ) → 𝐶 ∈ Cat )
2		uobrcl	⊢ ( 𝑥 ∈ dom ( ( 𝐶 Δfunc ∅ ) ( 𝐶 UP ( ∅ FuncCat 𝐶 ) ) ⟨ ∅ , ∅ ⟩ ) → ( 𝐶 ∈ Cat ∧ ( ∅ FuncCat 𝐶 ) ∈ Cat ) )
3	2	simpld	⊢ ( 𝑥 ∈ dom ( ( 𝐶 Δfunc ∅ ) ( 𝐶 UP ( ∅ FuncCat 𝐶 ) ) ⟨ ∅ , ∅ ⟩ ) → 𝐶 ∈ Cat )
4		0ex	⊢ ∅ ∈ V
5	4	a1i	⊢ ( 𝐶 ∈ Cat → ∅ ∈ V )
6		base0	⊢ ∅ = ( Base ‘ ∅ )
7	6	a1i	⊢ ( 𝐶 ∈ Cat → ∅ = ( Base ‘ ∅ ) )
8		id	⊢ ( 𝐶 ∈ Cat → 𝐶 ∈ Cat )
9		eqid	⊢ ( ∅ FuncCat 𝐶 ) = ( ∅ FuncCat 𝐶 )
10	5 7 8 9	0fucterm	⊢ ( 𝐶 ∈ Cat → ( ∅ FuncCat 𝐶 ) ∈ TermCat )
11		opex	⊢ ⟨ ∅ , ∅ ⟩ ∈ V
12	11	snid	⊢ ⟨ ∅ , ∅ ⟩ ∈ { ⟨ ∅ , ∅ ⟩ }
13	9	fucbas	⊢ ( ∅ Func 𝐶 ) = ( Base ‘ ( ∅ FuncCat 𝐶 ) )
14	8	0func	⊢ ( 𝐶 ∈ Cat → ( ∅ Func 𝐶 ) = { ⟨ ∅ , ∅ ⟩ } )
15	13 14	eqtr3id	⊢ ( 𝐶 ∈ Cat → ( Base ‘ ( ∅ FuncCat 𝐶 ) ) = { ⟨ ∅ , ∅ ⟩ } )
16	12 15	eleqtrrid	⊢ ( 𝐶 ∈ Cat → ⟨ ∅ , ∅ ⟩ ∈ ( Base ‘ ( ∅ FuncCat 𝐶 ) ) )
17		eqid	⊢ ( 𝐶 Δfunc ∅ ) = ( 𝐶 Δfunc ∅ )
18		0cat	⊢ ∅ ∈ Cat
19	18	a1i	⊢ ( 𝐶 ∈ Cat → ∅ ∈ Cat )
20	17 8 19 9	diagcl	⊢ ( 𝐶 ∈ Cat → ( 𝐶 Δfunc ∅ ) ∈ ( 𝐶 Func ( ∅ FuncCat 𝐶 ) ) )
21	10 16 20	isinito4	⊢ ( 𝐶 ∈ Cat → ( 𝑥 ∈ ( InitO ‘ 𝐶 ) ↔ 𝑥 ∈ dom ( ( 𝐶 Δfunc ∅ ) ( 𝐶 UP ( ∅ FuncCat 𝐶 ) ) ⟨ ∅ , ∅ ⟩ ) ) )
22	1 3 21	pm5.21nii	⊢ ( 𝑥 ∈ ( InitO ‘ 𝐶 ) ↔ 𝑥 ∈ dom ( ( 𝐶 Δfunc ∅ ) ( 𝐶 UP ( ∅ FuncCat 𝐶 ) ) ⟨ ∅ , ∅ ⟩ ) )
23	22	eqriv	⊢ ( InitO ‘ 𝐶 ) = dom ( ( 𝐶 Δfunc ∅ ) ( 𝐶 UP ( ∅ FuncCat 𝐶 ) ) ⟨ ∅ , ∅ ⟩ )
24		df-ov	⊢ ( ∅ ( 𝐶 Colimit ∅ ) ∅ ) = ( ( 𝐶 Colimit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ )
25		cmdfval2	⊢ ( ( 𝐶 Colimit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) = ( ( 𝐶 Δfunc ∅ ) ( 𝐶 UP ( ∅ FuncCat 𝐶 ) ) ⟨ ∅ , ∅ ⟩ )
26	24 25	eqtri	⊢ ( ∅ ( 𝐶 Colimit ∅ ) ∅ ) = ( ( 𝐶 Δfunc ∅ ) ( 𝐶 UP ( ∅ FuncCat 𝐶 ) ) ⟨ ∅ , ∅ ⟩ )
27	26	dmeqi	⊢ dom ( ∅ ( 𝐶 Colimit ∅ ) ∅ ) = dom ( ( 𝐶 Δfunc ∅ ) ( 𝐶 UP ( ∅ FuncCat 𝐶 ) ) ⟨ ∅ , ∅ ⟩ )
28	23 27	eqtr4i	⊢ ( InitO ‘ 𝐶 ) = dom ( ∅ ( 𝐶 Colimit ∅ ) ∅ )