Metamath Proof Explorer

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

Proof

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