Metamath Proof Explorer

Theorem initoeu2

Description: Initial objects are essentially unique, if A is an initial object, then so is every object that is isomorphic to A. Proposition 7.3 (2) in Adamek p. 102. (Contributed by AV, 10-Apr-2020)

Ref Expression
Hypotheses initoeu1.c 
|- ( ph -> C e. Cat )
initoeu1.a 
|- ( ph -> A e. ( InitO ` C ) )
initoeu2.i 
|- ( ph -> A ( ~=c ` C ) B )
Assertion initoeu2 
|- ( ph -> B e. ( InitO ` C ) )

Proof

Step Hyp Ref Expression
1 initoeu1.c 
 |-  ( ph -> C e. Cat )
2 initoeu1.a 
 |-  ( ph -> A e. ( InitO ` C ) )
3 initoeu2.i 
 |-  ( ph -> A ( ~=c ` C ) B )
4 ciclcl 
 |-  ( ( C e. Cat /\ A ( ~=c ` C ) B ) -> A e. ( Base ` C ) )
5 1 4 sylan 
 |-  ( ( ph /\ A ( ~=c ` C ) B ) -> A e. ( Base ` C ) )
6 cicrcl 
 |-  ( ( C e. Cat /\ A ( ~=c ` C ) B ) -> B e. ( Base ` C ) )
7 1 6 sylan 
 |-  ( ( ph /\ A ( ~=c ` C ) B ) -> B e. ( Base ` C ) )
8 1 adantr 
 |-  ( ( ph /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) -> C e. Cat )
9 cicsym 
 |-  ( ( C e. Cat /\ A ( ~=c ` C ) B ) -> B ( ~=c ` C ) A )
10 8 9 sylan 
 |-  ( ( ( ph /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) /\ A ( ~=c ` C ) B ) -> B ( ~=c ` C ) A )
11 eqid 
 |-  ( Iso ` C ) = ( Iso ` C )
12 eqid 
 |-  ( Base ` C ) = ( Base ` C )
13 simprr 
 |-  ( ( ph /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) -> B e. ( Base ` C ) )
14 simprl 
 |-  ( ( ph /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) -> A e. ( Base ` C ) )
15 11 12 8 13 14 cic 
 |-  ( ( ph /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) -> ( B ( ~=c ` C ) A <-> E. k k e. ( B ( Iso ` C ) A ) ) )
16 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
17 12 16 1 isinitoi 
 |-  ( ( ph /\ A e. ( InitO ` C ) ) -> ( A e. ( Base ` C ) /\ A. a e. ( Base ` C ) E! f f e. ( A ( Hom ` C ) a ) ) )
18 2 17 mpdan 
 |-  ( ph -> ( A e. ( Base ` C ) /\ A. a e. ( Base ` C ) E! f f e. ( A ( Hom ` C ) a ) ) )
19 oveq2 
 |-  ( a = b -> ( A ( Hom ` C ) a ) = ( A ( Hom ` C ) b ) )
20 19 eleq2d 
 |-  ( a = b -> ( f e. ( A ( Hom ` C ) a ) <-> f e. ( A ( Hom ` C ) b ) ) )
21 20 eubidv 
 |-  ( a = b -> ( E! f f e. ( A ( Hom ` C ) a ) <-> E! f f e. ( A ( Hom ` C ) b ) ) )
22 21 rspcva 
 |-  ( ( b e. ( Base ` C ) /\ A. a e. ( Base ` C ) E! f f e. ( A ( Hom ` C ) a ) ) -> E! f f e. ( A ( Hom ` C ) b ) )
23 nfv 
 |-  F/ h f e. ( A ( Hom ` C ) b )
24 nfv 
 |-  F/ f h e. ( A ( Hom ` C ) b )
25 eleq1w 
 |-  ( f = h -> ( f e. ( A ( Hom ` C ) b ) <-> h e. ( A ( Hom ` C ) b ) ) )
26 23 24 25 cbveuw 
 |-  ( E! f f e. ( A ( Hom ` C ) b ) <-> E! h h e. ( A ( Hom ` C ) b ) )
27 euex 
 |-  ( E! h h e. ( A ( Hom ` C ) b ) -> E. h h e. ( A ( Hom ` C ) b ) )
28 1 adantr 
 |-  ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) -> C e. Cat )
29 simpr 
 |-  ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> B e. ( Base ` C ) )
30 29 ad2antrl 
 |-  ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) -> B e. ( Base ` C ) )
31 simprll 
 |-  ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) -> A e. ( Base ` C ) )
32 12 16 11 28 30 31 isohom 
 |-  ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) -> ( B ( Iso ` C ) A ) C_ ( B ( Hom ` C ) A ) )
33 32 sselda 
 |-  ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) -> k e. ( B ( Hom ` C ) A ) )
34 eqid 
 |-  ( comp ` C ) = ( comp ` C )
35 28 ad2antrr 
 |-  ( ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) /\ ( k e. ( B ( Hom ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) ) ) -> C e. Cat )
36 30 ad2antrr 
 |-  ( ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) /\ ( k e. ( B ( Hom ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) ) ) -> B e. ( Base ` C ) )
37 31 ad2antrr 
 |-  ( ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) /\ ( k e. ( B ( Hom ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) ) ) -> A e. ( Base ` C ) )
38 simprr 
 |-  ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) -> b e. ( Base ` C ) )
39 38 ad2antrr 
 |-  ( ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) /\ ( k e. ( B ( Hom ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) ) ) -> b e. ( Base ` C ) )
40 simprl 
 |-  ( ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) /\ ( k e. ( B ( Hom ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) ) ) -> k e. ( B ( Hom ` C ) A ) )
41 simprr 
 |-  ( ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) /\ ( k e. ( B ( Hom ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) ) ) -> h e. ( A ( Hom ` C ) b ) )
42 12 16 34 35 36 37 39 40 41 catcocl 
 |-  ( ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) /\ ( k e. ( B ( Hom ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) ) ) -> ( h ( <. B , A >. ( comp ` C ) b ) k ) e. ( B ( Hom ` C ) b ) )
43 simp-4l 
 |-  ( ( ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) /\ ( k e. ( B ( Hom ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) ) ) /\ ( h ( <. B , A >. ( comp ` C ) b ) k ) e. ( B ( Hom ` C ) b ) ) -> ph )
44 df-3an 
 |-  ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) /\ b e. ( Base ` C ) ) <-> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) )
45 44 biimpri 
 |-  ( ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> ( A e. ( Base ` C ) /\ B e. ( Base ` C ) /\ b e. ( Base ` C ) ) )
46 45 ad4antlr 
 |-  ( ( ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) /\ ( k e. ( B ( Hom ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) ) ) /\ ( h ( <. B , A >. ( comp ` C ) b ) k ) e. ( B ( Hom ` C ) b ) ) -> ( A e. ( Base ` C ) /\ B e. ( Base ` C ) /\ b e. ( Base ` C ) ) )
47 simpr 
 |-  ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) -> k e. ( B ( Iso ` C ) A ) )
48 47 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) /\ ( k e. ( B ( Hom ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) ) ) /\ ( h ( <. B , A >. ( comp ` C ) b ) k ) e. ( B ( Hom ` C ) b ) ) -> k e. ( B ( Iso ` C ) A ) )
49 41 adantr 
 |-  ( ( ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) /\ ( k e. ( B ( Hom ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) ) ) /\ ( h ( <. B , A >. ( comp ` C ) b ) k ) e. ( B ( Hom ` C ) b ) ) -> h e. ( A ( Hom ` C ) b ) )
50 simpr 
 |-  ( ( ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) /\ ( k e. ( B ( Hom ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) ) ) /\ ( h ( <. B , A >. ( comp ` C ) b ) k ) e. ( B ( Hom ` C ) b ) ) -> ( h ( <. B , A >. ( comp ` C ) b ) k ) e. ( B ( Hom ` C ) b ) )
51 1 2 12 16 11 34 initoeu2lem2 
 |-  ( ( ph /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) /\ b e. ( Base ` C ) ) /\ ( k e. ( B ( Iso ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) /\ ( h ( <. B , A >. ( comp ` C ) b ) k ) e. ( B ( Hom ` C ) b ) ) ) -> ( E! f f e. ( A ( Hom ` C ) b ) -> E! g g e. ( B ( Hom ` C ) b ) ) )
52 43 46 48 49 50 51 syl113anc 
 |-  ( ( ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) /\ ( k e. ( B ( Hom ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) ) ) /\ ( h ( <. B , A >. ( comp ` C ) b ) k ) e. ( B ( Hom ` C ) b ) ) -> ( E! f f e. ( A ( Hom ` C ) b ) -> E! g g e. ( B ( Hom ` C ) b ) ) )
53 42 52 mpdan 
 |-  ( ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) /\ ( k e. ( B ( Hom ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) ) ) -> ( E! f f e. ( A ( Hom ` C ) b ) -> E! g g e. ( B ( Hom ` C ) b ) ) )
54 53 ex 
 |-  ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) -> ( ( k e. ( B ( Hom ` C ) A ) /\ h e. ( A ( Hom ` C ) b ) ) -> ( E! f f e. ( A ( Hom ` C ) b ) -> E! g g e. ( B ( Hom ` C ) b ) ) ) )
55 33 54 mpand 
 |-  ( ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) /\ k e. ( B ( Iso ` C ) A ) ) -> ( h e. ( A ( Hom ` C ) b ) -> ( E! f f e. ( A ( Hom ` C ) b ) -> E! g g e. ( B ( Hom ` C ) b ) ) ) )
56 55 ex 
 |-  ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) -> ( k e. ( B ( Iso ` C ) A ) -> ( h e. ( A ( Hom ` C ) b ) -> ( E! f f e. ( A ( Hom ` C ) b ) -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) )
57 56 com23 
 |-  ( ( ph /\ ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) ) -> ( h e. ( A ( Hom ` C ) b ) -> ( k e. ( B ( Iso ` C ) A ) -> ( E! f f e. ( A ( Hom ` C ) b ) -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) )
58 57 ex 
 |-  ( ph -> ( ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> ( h e. ( A ( Hom ` C ) b ) -> ( k e. ( B ( Iso ` C ) A ) -> ( E! f f e. ( A ( Hom ` C ) b ) -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) ) )
59 58 com15 
 |-  ( E! f f e. ( A ( Hom ` C ) b ) -> ( ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) /\ b e. ( Base ` C ) ) -> ( h e. ( A ( Hom ` C ) b ) -> ( k e. ( B ( Iso ` C ) A ) -> ( ph -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) ) )
60 59 expd 
 |-  ( E! f f e. ( A ( Hom ` C ) b ) -> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> ( b e. ( Base ` C ) -> ( h e. ( A ( Hom ` C ) b ) -> ( k e. ( B ( Iso ` C ) A ) -> ( ph -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) ) ) )
61 60 com24 
 |-  ( E! f f e. ( A ( Hom ` C ) b ) -> ( h e. ( A ( Hom ` C ) b ) -> ( b e. ( Base ` C ) -> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> ( k e. ( B ( Iso ` C ) A ) -> ( ph -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) ) ) )
62 61 com12 
 |-  ( h e. ( A ( Hom ` C ) b ) -> ( E! f f e. ( A ( Hom ` C ) b ) -> ( b e. ( Base ` C ) -> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> ( k e. ( B ( Iso ` C ) A ) -> ( ph -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) ) ) )
63 62 exlimiv 
 |-  ( E. h h e. ( A ( Hom ` C ) b ) -> ( E! f f e. ( A ( Hom ` C ) b ) -> ( b e. ( Base ` C ) -> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> ( k e. ( B ( Iso ` C ) A ) -> ( ph -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) ) ) )
64 27 63 syl 
 |-  ( E! h h e. ( A ( Hom ` C ) b ) -> ( E! f f e. ( A ( Hom ` C ) b ) -> ( b e. ( Base ` C ) -> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> ( k e. ( B ( Iso ` C ) A ) -> ( ph -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) ) ) )
65 26 64 sylbi 
 |-  ( E! f f e. ( A ( Hom ` C ) b ) -> ( E! f f e. ( A ( Hom ` C ) b ) -> ( b e. ( Base ` C ) -> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> ( k e. ( B ( Iso ` C ) A ) -> ( ph -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) ) ) )
66 65 pm2.43i 
 |-  ( E! f f e. ( A ( Hom ` C ) b ) -> ( b e. ( Base ` C ) -> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> ( k e. ( B ( Iso ` C ) A ) -> ( ph -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) ) )
67 66 com12 
 |-  ( b e. ( Base ` C ) -> ( E! f f e. ( A ( Hom ` C ) b ) -> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> ( k e. ( B ( Iso ` C ) A ) -> ( ph -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) ) )
68 67 adantr 
 |-  ( ( b e. ( Base ` C ) /\ A. a e. ( Base ` C ) E! f f e. ( A ( Hom ` C ) a ) ) -> ( E! f f e. ( A ( Hom ` C ) b ) -> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> ( k e. ( B ( Iso ` C ) A ) -> ( ph -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) ) )
69 22 68 mpd 
 |-  ( ( b e. ( Base ` C ) /\ A. a e. ( Base ` C ) E! f f e. ( A ( Hom ` C ) a ) ) -> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> ( k e. ( B ( Iso ` C ) A ) -> ( ph -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) )
70 69 ex 
 |-  ( b e. ( Base ` C ) -> ( A. a e. ( Base ` C ) E! f f e. ( A ( Hom ` C ) a ) -> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> ( k e. ( B ( Iso ` C ) A ) -> ( ph -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) ) )
71 70 com15 
 |-  ( ph -> ( A. a e. ( Base ` C ) E! f f e. ( A ( Hom ` C ) a ) -> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> ( k e. ( B ( Iso ` C ) A ) -> ( b e. ( Base ` C ) -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) ) )
72 71 adantld 
 |-  ( ph -> ( ( A e. ( Base ` C ) /\ A. a e. ( Base ` C ) E! f f e. ( A ( Hom ` C ) a ) ) -> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> ( k e. ( B ( Iso ` C ) A ) -> ( b e. ( Base ` C ) -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) ) )
73 18 72 mpd 
 |-  ( ph -> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> ( k e. ( B ( Iso ` C ) A ) -> ( b e. ( Base ` C ) -> E! g g e. ( B ( Hom ` C ) b ) ) ) ) )
74 73 imp 
 |-  ( ( ph /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) -> ( k e. ( B ( Iso ` C ) A ) -> ( b e. ( Base ` C ) -> E! g g e. ( B ( Hom ` C ) b ) ) ) )
75 74 exlimdv 
 |-  ( ( ph /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) -> ( E. k k e. ( B ( Iso ` C ) A ) -> ( b e. ( Base ` C ) -> E! g g e. ( B ( Hom ` C ) b ) ) ) )
76 15 75 sylbid 
 |-  ( ( ph /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) -> ( B ( ~=c ` C ) A -> ( b e. ( Base ` C ) -> E! g g e. ( B ( Hom ` C ) b ) ) ) )
77 76 adantr 
 |-  ( ( ( ph /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) /\ A ( ~=c ` C ) B ) -> ( B ( ~=c ` C ) A -> ( b e. ( Base ` C ) -> E! g g e. ( B ( Hom ` C ) b ) ) ) )
78 10 77 mpd 
 |-  ( ( ( ph /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) /\ A ( ~=c ` C ) B ) -> ( b e. ( Base ` C ) -> E! g g e. ( B ( Hom ` C ) b ) ) )
79 78 an32s 
 |-  ( ( ( ph /\ A ( ~=c ` C ) B ) /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) -> ( b e. ( Base ` C ) -> E! g g e. ( B ( Hom ` C ) b ) ) )
80 79 ralrimiv 
 |-  ( ( ( ph /\ A ( ~=c ` C ) B ) /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) -> A. b e. ( Base ` C ) E! g g e. ( B ( Hom ` C ) b ) )
81 1 ad2antrr 
 |-  ( ( ( ph /\ A ( ~=c ` C ) B ) /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) -> C e. Cat )
82 simprr 
 |-  ( ( ( ph /\ A ( ~=c ` C ) B ) /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) -> B e. ( Base ` C ) )
83 12 16 81 82 isinito 
 |-  ( ( ( ph /\ A ( ~=c ` C ) B ) /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) -> ( B e. ( InitO ` C ) <-> A. b e. ( Base ` C ) E! g g e. ( B ( Hom ` C ) b ) ) )
84 80 83 mpbird 
 |-  ( ( ( ph /\ A ( ~=c ` C ) B ) /\ ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) ) -> B e. ( InitO ` C ) )
85 84 ex 
 |-  ( ( ph /\ A ( ~=c ` C ) B ) -> ( ( A e. ( Base ` C ) /\ B e. ( Base ` C ) ) -> B e. ( InitO ` C ) ) )
86 5 7 85 mp2and 
 |-  ( ( ph /\ A ( ~=c ` C ) B ) -> B e. ( InitO ` C ) )
87 3 86 mpdan 
 |-  ( ph -> B e. ( InitO ` C ) )