Metamath Proof Explorer

Theorem dftermo4

Description: An alternate definition of df-termo using universal property. See also the "Equivalent formulations" section of https://en.wikipedia.org/wiki/Initial_and_terminal_objects . (Contributed by Zhi Wang, 23-Oct-2025)

Ref Expression
Assertion dftermo4 
|- TermO = ( c e. Cat |-> [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) )

Proof

Step Hyp Ref Expression
1 dftermo2 
 |-  TermO = ( c e. Cat |-> ( InitO ` ( oppCat ` c ) ) )
2 eqid 
 |-  ( oppCat ` c ) = ( oppCat ` c )
3 2 oppccat 
 |-  ( c e. Cat -> ( oppCat ` c ) e. Cat )
4 ovex 
 |-  ( f ( o UP d ) (/) ) e. _V
5 4 dmex 
 |-  dom ( f ( o UP d ) (/) ) e. _V
6 5 csbex 
 |-  [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V
7 6 csbex 
 |-  [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V
8 7 csbex 
 |-  [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V
9 dfinito4 
 |-  InitO = ( o e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) )
10 9 fvmpts 
 |-  ( ( ( oppCat ` c ) e. Cat /\ [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V ) -> ( InitO ` ( oppCat ` c ) ) = [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) )
11 3 8 10 sylancl 
 |-  ( c e. Cat -> ( InitO ` ( oppCat ` c ) ) = [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) )
12 11 mpteq2ia 
 |-  ( c e. Cat |-> ( InitO ` ( oppCat ` c ) ) ) = ( c e. Cat |-> [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) )
13 1 12 eqtri 
 |-  TermO = ( c e. Cat |-> [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) )