Metamath Proof Explorer

Theorem isinito2lem

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 ) ) ` (/) )
isinito2lem.c 
|- ( ph -> C e. Cat )
isinito2lem.i 
|- ( ph -> I e. ( Base ` C ) )
Assertion isinito2lem 
|- ( ph -> ( I e. ( InitO ` C ) <-> I ( F ( C UP .1. ) (/) ) (/) ) )

Proof

Step Hyp Ref Expression
1 isinito2.1 
 |-  .1. = ( SetCat ` 1o )
2 isinito2.f 
 |-  F = ( ( 1st ` ( .1. DiagFunc C ) ) ` (/) )
3 isinito2lem.c 
 |-  ( ph -> C e. Cat )
4 isinito2lem.i 
 |-  ( ph -> I e. ( Base ` C ) )
5 reutru 
 |-  ( E! f f e. ( I ( Hom ` C ) x ) <-> E! f e. ( I ( Hom ` C ) x ) T. )
6 0ex 
 |-  (/) e. _V
7 eqeq1 
 |-  ( y = (/) -> ( y = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) <-> (/) = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) ) )
8 7 reubidv 
 |-  ( y = (/) -> ( E! f e. ( I ( Hom ` C ) x ) y = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) <-> E! f e. ( I ( Hom ` C ) x ) (/) = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) ) )
9 6 8 ralsn 
 |-  ( A. y e. { (/) } E! f e. ( I ( Hom ` C ) x ) y = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) <-> E! f e. ( I ( Hom ` C ) x ) (/) = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) )
10 eqid 
 |-  ( .1. DiagFunc C ) = ( .1. DiagFunc C )
11 setc1oterm 
 |-  ( SetCat ` 1o ) e. TermCat
12 1 11 eqeltri 
 |-  .1. e. TermCat
13 12 a1i 
 |-  ( ph -> .1. e. TermCat )
14 13 termccd 
 |-  ( ph -> .1. e. Cat )
15 1 setc1obas 
 |-  1o = ( Base ` .1. )
16 0lt1o 
 |-  (/) e. 1o
17 16 a1i 
 |-  ( ph -> (/) e. 1o )
18 eqid 
 |-  ( Base ` C ) = ( Base ` C )
19 10 14 3 15 17 2 18 4 diag11 
 |-  ( ph -> ( ( 1st ` F ) ` I ) = (/) )
20 19 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` I ) = (/) )
21 20 opeq2d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> <. (/) , ( ( 1st ` F ) ` I ) >. = <. (/) , (/) >. )
22 14 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> .1. e. Cat )
23 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> C e. Cat )
24 16 a1i 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> (/) e. 1o )
25 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
26 10 22 23 15 24 2 18 25 diag11 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` F ) ` x ) = (/) )
27 21 26 oveq12d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) = ( <. (/) , (/) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } (/) ) )
28 snex 
 |-  { <. (/) , (/) , (/) >. } e. _V
29 28 ovsn2 
 |-  ( <. (/) , (/) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } (/) ) = { <. (/) , (/) , (/) >. }
30 27 29 eqtrdi 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) = { <. (/) , (/) , (/) >. } )
31 30 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) = { <. (/) , (/) , (/) >. } )
32 12 a1i 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> .1. e. TermCat )
33 32 termccd 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> .1. e. Cat )
34 3 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> C e. Cat )
35 16 a1i 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> (/) e. 1o )
36 4 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> I e. ( Base ` C ) )
37 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
38 eqid 
 |-  ( Id ` .1. ) = ( Id ` .1. )
39 simplr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> x e. ( Base ` C ) )
40 simpr 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> f e. ( I ( Hom ` C ) x ) )
41 10 33 34 15 35 2 18 36 37 38 39 40 diag12 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> ( ( I ( 2nd ` F ) x ) ` f ) = ( ( Id ` .1. ) ` (/) ) )
42 1 38 setc1oid 
 |-  ( ( Id ` .1. ) ` (/) ) = (/)
43 41 42 eqtrdi 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> ( ( I ( 2nd ` F ) x ) ` f ) = (/) )
44 eqidd 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> (/) = (/) )
45 31 43 44 oveq123d 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) = ( (/) { <. (/) , (/) , (/) >. } (/) ) )
46 6 ovsn2 
 |-  ( (/) { <. (/) , (/) , (/) >. } (/) ) = (/)
47 45 46 eqtr2di 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> (/) = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) )
48 tbtru 
 |-  ( (/) = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) <-> ( (/) = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) <-> T. ) )
49 47 48 sylib 
 |-  ( ( ( ph /\ x e. ( Base ` C ) ) /\ f e. ( I ( Hom ` C ) x ) ) -> ( (/) = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) <-> T. ) )
50 49 reubidva 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( E! f e. ( I ( Hom ` C ) x ) (/) = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) <-> E! f e. ( I ( Hom ` C ) x ) T. ) )
51 9 50 bitr2id 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( E! f e. ( I ( Hom ` C ) x ) T. <-> A. y e. { (/) } E! f e. ( I ( Hom ` C ) x ) y = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) ) )
52 26 oveq2d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` x ) ) = ( (/) { <. (/) , (/) , 1o >. } (/) ) )
53 1oex 
 |-  1o e. _V
54 53 ovsn2 
 |-  ( (/) { <. (/) , (/) , 1o >. } (/) ) = 1o
55 df1o2 
 |-  1o = { (/) }
56 54 55 eqtri 
 |-  ( (/) { <. (/) , (/) , 1o >. } (/) ) = { (/) }
57 52 56 eqtrdi 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` x ) ) = { (/) } )
58 57 raleqdv 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( A. y e. ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` x ) ) E! f e. ( I ( Hom ` C ) x ) y = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) <-> A. y e. { (/) } E! f e. ( I ( Hom ` C ) x ) y = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) ) )
59 51 58 bitr4d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( E! f e. ( I ( Hom ` C ) x ) T. <-> A. y e. ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` x ) ) E! f e. ( I ( Hom ` C ) x ) y = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) ) )
60 5 59 bitrid 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( E! f f e. ( I ( Hom ` C ) x ) <-> A. y e. ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` x ) ) E! f e. ( I ( Hom ` C ) x ) y = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) ) )
61 60 ralbidva 
 |-  ( ph -> ( A. x e. ( Base ` C ) E! f f e. ( I ( Hom ` C ) x ) <-> A. x e. ( Base ` C ) A. y e. ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` x ) ) E! f e. ( I ( Hom ` C ) x ) y = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) ) )
62 18 37 3 4 isinito 
 |-  ( ph -> ( I e. ( InitO ` C ) <-> A. x e. ( Base ` C ) E! f f e. ( I ( Hom ` C ) x ) ) )
63 1 setc1ohomfval 
 |-  { <. (/) , (/) , 1o >. } = ( Hom ` .1. )
64 1 setc1ocofval 
 |-  { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } = ( comp ` .1. )
65 1 2 3 funcsetc1ocl 
 |-  ( ph -> F e. ( C Func .1. ) )
66 65 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( C Func .1. ) ( 2nd ` F ) )
67 19 oveq2d 
 |-  ( ph -> ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` I ) ) = ( (/) { <. (/) , (/) , 1o >. } (/) ) )
68 67 54 eqtrdi 
 |-  ( ph -> ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` I ) ) = 1o )
69 16 68 eleqtrrid 
 |-  ( ph -> (/) e. ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` I ) ) )
70 18 15 37 63 64 17 66 4 69 isup 
 |-  ( ph -> ( I ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP .1. ) (/) ) (/) <-> A. x e. ( Base ` C ) A. y e. ( (/) { <. (/) , (/) , 1o >. } ( ( 1st ` F ) ` x ) ) E! f e. ( I ( Hom ` C ) x ) y = ( ( ( I ( 2nd ` F ) x ) ` f ) ( <. (/) , ( ( 1st ` F ) ` I ) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } ( ( 1st ` F ) ` x ) ) (/) ) ) )
71 61 62 70 3bitr4d 
 |-  ( ph -> ( I e. ( InitO ` C ) <-> I ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP .1. ) (/) ) (/) ) )
72 65 up1st2ndb 
 |-  ( ph -> ( I ( F ( C UP .1. ) (/) ) (/) <-> I ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP .1. ) (/) ) (/) ) )
73 71 72 bitr4d 
 |-  ( ph -> ( I e. ( InitO ` C ) <-> I ( F ( C UP .1. ) (/) ) (/) ) )