Metamath Proof Explorer

Theorem isinito3

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

Ref Expression
Hypotheses isinito2.1 
|- .1. = ( SetCat ` 1o )
isinito2.f 
|- F = ( ( 1st ` ( .1. DiagFunc C ) ) ` (/) )
Assertion isinito3 
|- ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) (/) ) )

Proof

Step Hyp Ref Expression
1 isinito2.1 
 |-  .1. = ( SetCat ` 1o )
2 isinito2.f 
 |-  F = ( ( 1st ` ( .1. DiagFunc C ) ) ` (/) )
3 relup 
 |-  Rel ( F ( C UP .1. ) (/) )
4 1 2 isinito2 
 |-  ( I e. ( InitO ` C ) <-> I ( F ( C UP .1. ) (/) ) (/) )
5 4 biimpi 
 |-  ( I e. ( InitO ` C ) -> I ( F ( C UP .1. ) (/) ) (/) )
6 releldm 
 |-  ( ( Rel ( F ( C UP .1. ) (/) ) /\ I ( F ( C UP .1. ) (/) ) (/) ) -> I e. dom ( F ( C UP .1. ) (/) ) )
7 3 5 6 sylancr 
 |-  ( I e. ( InitO ` C ) -> I e. dom ( F ( C UP .1. ) (/) ) )
8 releldmb 
 |-  ( Rel ( F ( C UP .1. ) (/) ) -> ( I e. dom ( F ( C UP .1. ) (/) ) <-> E. y I ( F ( C UP .1. ) (/) ) y ) )
9 3 8 ax-mp 
 |-  ( I e. dom ( F ( C UP .1. ) (/) ) <-> E. y I ( F ( C UP .1. ) (/) ) y )
10 id 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> I ( F ( C UP .1. ) (/) ) y )
11 10 up1st2nd 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> I ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP .1. ) (/) ) y )
12 1 setc1ohomfval 
 |-  { <. (/) , (/) , 1o >. } = ( Hom ` .1. )
13 11 12 uprcl5 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> y e. ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` I ) ) )
14 eqid 
 |-  ( .1. DiagFunc C ) = ( .1. DiagFunc C )
15 setc1oterm 
 |-  ( SetCat ` 1o ) e. TermCat
16 1 15 eqeltri 
 |-  .1. e. TermCat
17 16 a1i 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> .1. e. TermCat )
18 17 termccd 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> .1. e. Cat )
19 11 uprcl2 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> ( 1st ` F ) ( C Func .1. ) ( 2nd ` F ) )
20 19 funcrcl2 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> C e. Cat )
21 1 setc1obas 
 |-  1o = ( Base ` .1. )
22 11 21 uprcl3 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> (/) e. 1o )
23 eqid 
 |-  ( Base ` C ) = ( Base ` C )
24 11 23 uprcl4 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> I e. ( Base ` C ) )
25 14 18 20 21 22 2 23 24 diag11 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> ( ( 1st ` F ) ` I ) = (/) )
26 25 oveq2d 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` I ) ) = ( (/) { <. (/) , (/) , 1o >. } (/) ) )
27 1oex 
 |-  1o e. _V
28 27 ovsn2 
 |-  ( (/) { <. (/) , (/) , 1o >. } (/) ) = 1o
29 26 28 eqtrdi 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` I ) ) = 1o )
30 13 29 eleqtrd 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> y e. 1o )
31 el1o 
 |-  ( y e. 1o <-> y = (/) )
32 30 31 sylib 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> y = (/) )
33 10 32 breqtrd 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> I ( F ( C UP .1. ) (/) ) (/) )
34 33 4 sylibr 
 |-  ( I ( F ( C UP .1. ) (/) ) y -> I e. ( InitO ` C ) )
35 34 exlimiv 
 |-  ( E. y I ( F ( C UP .1. ) (/) ) y -> I e. ( InitO ` C ) )
36 9 35 sylbi 
 |-  ( I e. dom ( F ( C UP .1. ) (/) ) -> I e. ( InitO ` C ) )
37 7 36 impbii 
 |-  ( I e. ( InitO ` C ) <-> I e. dom ( F ( C UP .1. ) (/) ) )