Metamath Proof Explorer

Theorem isinito4

Description: The predicate "is an initial object" of a category, using universal property. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses isinito4.1 
|- ( ph -> .1. e. TermCat )
isinito4.x 
|- ( ph -> X e. ( Base ` .1. ) )
isinito4.f 
|- ( ph -> F e. ( C Func .1. ) )
Assertion isinito4 
|- ( ph -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) )

Proof

Step Hyp Ref Expression
1 isinito4.1 
 |-  ( ph -> .1. e. TermCat )
2 isinito4.x 
 |-  ( ph -> X e. ( Base ` .1. ) )
3 isinito4.f 
 |-  ( ph -> F e. ( C Func .1. ) )
4 eqid 
 |-  ( SetCat ` 1o ) = ( SetCat ` 1o )
5 eqid 
 |-  ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) = ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) )
6 4 5 isinito3 
 |-  ( I e. ( InitO ` C ) <-> I e. dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) ( C UP ( SetCat ` 1o ) ) (/) ) )
7 4 setc1obas 
 |-  1o = ( Base ` ( SetCat ` 1o ) )
8 eqid 
 |-  ( Base ` .1. ) = ( Base ` .1. )
9 0lt1o 
 |-  (/) e. 1o
10 9 a1i 
 |-  ( ph -> (/) e. 1o )
11 3 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( C Func .1. ) ( 2nd ` F ) )
12 11 funcrcl2 
 |-  ( ph -> C e. Cat )
13 4 5 12 funcsetc1ocl 
 |-  ( ph -> ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) e. ( C Func ( SetCat ` 1o ) ) )
14 setc1oterm 
 |-  ( SetCat ` 1o ) e. TermCat
15 14 a1i 
 |-  ( ph -> ( SetCat ` 1o ) e. TermCat )
16 7 8 10 2 13 3 15 1 uobeqterm 
 |-  ( ph -> dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) ( C UP ( SetCat ` 1o ) ) (/) ) = dom ( F ( C UP .1. ) X ) )
17 16 eleq2d 
 |-  ( ph -> ( I e. dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc C ) ) ` (/) ) ( C UP ( SetCat ` 1o ) ) (/) ) <-> I e. dom ( F ( C UP .1. ) X ) ) )
18 6 17 bitrid 
 |-  ( ph -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) )