Metamath Proof Explorer

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 ` C ) = dom ( (/) ( C Colimit (/) ) (/) )

Proof

Step Hyp Ref Expression
1 initorcl 
 |-  ( x e. ( InitO ` C ) -> C e. Cat )
2 uobrcl 
 |-  ( x e. dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) -> ( C e. Cat /\ ( (/) FuncCat C ) e. Cat ) )
3 2 simpld 
 |-  ( x e. dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) -> C e. Cat )
4 0ex 
 |-  (/) e. _V
5 4 a1i 
 |-  ( C e. Cat -> (/) e. _V )
6 base0 
 |-  (/) = ( Base ` (/) )
7 6 a1i 
 |-  ( C e. Cat -> (/) = ( Base ` (/) ) )
8 id 
 |-  ( C e. Cat -> C e. Cat )
9 eqid 
 |-  ( (/) FuncCat C ) = ( (/) FuncCat C )
10 5 7 8 9 0fucterm 
 |-  ( C e. Cat -> ( (/) FuncCat C ) e. TermCat )
11 opex 
 |-  <. (/) , (/) >. e. _V
12 11 snid 
 |-  <. (/) , (/) >. e. { <. (/) , (/) >. }
13 9 fucbas 
 |-  ( (/) Func C ) = ( Base ` ( (/) FuncCat C ) )
14 8 0func 
 |-  ( C e. Cat -> ( (/) Func C ) = { <. (/) , (/) >. } )
15 13 14 eqtr3id 
 |-  ( C e. Cat -> ( Base ` ( (/) FuncCat C ) ) = { <. (/) , (/) >. } )
16 12 15 eleqtrrid 
 |-  ( C e. Cat -> <. (/) , (/) >. e. ( Base ` ( (/) FuncCat C ) ) )
17 eqid 
 |-  ( C DiagFunc (/) ) = ( C DiagFunc (/) )
18 0cat 
 |-  (/) e. Cat
19 18 a1i 
 |-  ( C e. Cat -> (/) e. Cat )
20 17 8 19 9 diagcl 
 |-  ( C e. Cat -> ( C DiagFunc (/) ) e. ( C Func ( (/) FuncCat C ) ) )
21 10 16 20 isinito4 
 |-  ( C e. Cat -> ( x e. ( InitO ` C ) <-> x e. dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) ) )
22 1 3 21 pm5.21nii 
 |-  ( x e. ( InitO ` C ) <-> x e. dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. ) )
23 22 eqriv 
 |-  ( InitO ` C ) = dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. )
24 df-ov 
 |-  ( (/) ( C Colimit (/) ) (/) ) = ( ( C Colimit (/) ) ` <. (/) , (/) >. )
25 cmdfval2 
 |-  ( ( C Colimit (/) ) ` <. (/) , (/) >. ) = ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. )
26 24 25 eqtri 
 |-  ( (/) ( C Colimit (/) ) (/) ) = ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. )
27 26 dmeqi 
 |-  dom ( (/) ( C Colimit (/) ) (/) ) = dom ( ( C DiagFunc (/) ) ( C UP ( (/) FuncCat C ) ) <. (/) , (/) >. )
28 23 27 eqtr4i 
 |-  ( InitO ` C ) = dom ( (/) ( C Colimit (/) ) (/) )