Metamath Proof Explorer

Theorem dfinito4

Description: An alternate definition of df-inito 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 dfinito4 
|- InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) )

Proof

Step Hyp Ref Expression
1 initofn 
 |-  InitO Fn Cat
2 ovex 
 |-  ( f ( c UP d ) (/) ) e. _V
3 2 dmex 
 |-  dom ( f ( c UP d ) (/) ) e. _V
4 3 csbex 
 |-  [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) e. _V
5 4 csbex 
 |-  [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) e. _V
6 eqid 
 |-  ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) )
7 5 6 fnmpti 
 |-  ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) Fn Cat
8 eqfnfv 
 |-  ( ( InitO Fn Cat /\ ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) Fn Cat ) -> ( InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) <-> A. e e. Cat ( InitO ` e ) = ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) ) )
9 1 7 8 mp2an 
 |-  ( InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) <-> A. e e. Cat ( InitO ` e ) = ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) )
10 eqid 
 |-  ( SetCat ` 1o ) = ( SetCat ` 1o )
11 eqid 
 |-  ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) = ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) )
12 10 11 isinito3 
 |-  ( x e. ( InitO ` e ) <-> x e. dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) )
13 12 eqriv 
 |-  ( InitO ` e ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) )
14 fvex 
 |-  ( SetCat ` 1o ) e. _V
15 fvexd 
 |-  ( d = ( SetCat ` 1o ) -> ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) e. _V )
16 simpl 
 |-  ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> d = ( SetCat ` 1o ) )
17 16 oveq2d 
 |-  ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> ( e UP d ) = ( e UP ( SetCat ` 1o ) ) )
18 simpr 
 |-  ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) )
19 16 fvoveq1d 
 |-  ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> ( 1st ` ( d DiagFunc e ) ) = ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) )
20 19 fveq1d 
 |-  ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) = ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) )
21 18 20 eqtrd 
 |-  ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> f = ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) )
22 eqidd 
 |-  ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> (/) = (/) )
23 17 21 22 oveq123d 
 |-  ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> ( f ( e UP d ) (/) ) = ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) )
24 23 dmeqd 
 |-  ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> dom ( f ( e UP d ) (/) ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) )
25 15 24 csbied 
 |-  ( d = ( SetCat ` 1o ) -> [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) )
26 14 25 csbie 
 |-  [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) )
27 13 26 eqtr4i 
 |-  ( InitO ` e ) = [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) )
28 oveq2 
 |-  ( c = e -> ( d DiagFunc c ) = ( d DiagFunc e ) )
29 28 fveq2d 
 |-  ( c = e -> ( 1st ` ( d DiagFunc c ) ) = ( 1st ` ( d DiagFunc e ) ) )
30 29 fveq1d 
 |-  ( c = e -> ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) )
31 oveq1 
 |-  ( c = e -> ( c UP d ) = ( e UP d ) )
32 31 oveqd 
 |-  ( c = e -> ( f ( c UP d ) (/) ) = ( f ( e UP d ) (/) ) )
33 32 dmeqd 
 |-  ( c = e -> dom ( f ( c UP d ) (/) ) = dom ( f ( e UP d ) (/) ) )
34 30 33 csbeq12dv 
 |-  ( c = e -> [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) = [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) )
35 34 csbeq2dv 
 |-  ( c = e -> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) = [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) )
36 ovex 
 |-  ( f ( e UP d ) (/) ) e. _V
37 36 dmex 
 |-  dom ( f ( e UP d ) (/) ) e. _V
38 37 csbex 
 |-  [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) e. _V
39 38 csbex 
 |-  [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) e. _V
40 35 6 39 fvmpt 
 |-  ( e e. Cat -> ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) = [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) )
41 27 40 eqtr4id 
 |-  ( e e. Cat -> ( InitO ` e ) = ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) )
42 9 41 mprgbir 
 |-  InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) )