This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isinito4a

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. ) )
isinito4a.f 
|- F = ( ( 1st ` ( .1. DiagFunc C ) ) ` X )
Assertion isinito4a 
|- ( 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 isinito4a.f 
 |-  F = ( ( 1st ` ( .1. DiagFunc C ) ) ` X )
4 initorcl 
 |-  ( I e. ( InitO ` C ) -> C e. Cat )
5 4 anim2i 
 |-  ( ( ph /\ I e. ( InitO ` C ) ) -> ( ph /\ C e. Cat ) )
6 uobrcl 
 |-  ( I e. dom ( F ( C UP .1. ) X ) -> ( C e. Cat /\ .1. e. Cat ) )
7 6 simpld 
 |-  ( I e. dom ( F ( C UP .1. ) X ) -> C e. Cat )
8 7 anim2i 
 |-  ( ( ph /\ I e. dom ( F ( C UP .1. ) X ) ) -> ( ph /\ C e. Cat ) )
9 1 adantr 
 |-  ( ( ph /\ C e. Cat ) -> .1. e. TermCat )
10 2 adantr 
 |-  ( ( ph /\ C e. Cat ) -> X e. ( Base ` .1. ) )
11 eqid 
 |-  ( .1. DiagFunc C ) = ( .1. DiagFunc C )
12 9 termccd 
 |-  ( ( ph /\ C e. Cat ) -> .1. e. Cat )
13 simpr 
 |-  ( ( ph /\ C e. Cat ) -> C e. Cat )
14 eqid 
 |-  ( Base ` .1. ) = ( Base ` .1. )
15 11 12 13 14 10 3 diag1cl 
 |-  ( ( ph /\ C e. Cat ) -> F e. ( C Func .1. ) )
16 9 10 15 isinito4 
 |-  ( ( ph /\ C e. Cat ) -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) )
17 5 8 16 pm5.21nd 
 |-  ( ph -> ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) X ) ) )