Step |
Hyp |
Ref |
Expression |
1 |
|
initoeu1.c |
|- ( ph -> C e. Cat ) |
2 |
|
initoeu1.a |
|- ( ph -> A e. ( InitO ` C ) ) |
3 |
|
initoeu1.b |
|- ( ph -> B e. ( InitO ` C ) ) |
4 |
1 2 3
|
initoeu1 |
|- ( ph -> E! f f e. ( A ( Iso ` C ) B ) ) |
5 |
|
euex |
|- ( E! f f e. ( A ( Iso ` C ) B ) -> E. f f e. ( A ( Iso ` C ) B ) ) |
6 |
4 5
|
syl |
|- ( ph -> E. f f e. ( A ( Iso ` C ) B ) ) |
7 |
|
eqid |
|- ( Iso ` C ) = ( Iso ` C ) |
8 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
9 |
|
initoo |
|- ( C e. Cat -> ( A e. ( InitO ` C ) -> A e. ( Base ` C ) ) ) |
10 |
1 2 9
|
sylc |
|- ( ph -> A e. ( Base ` C ) ) |
11 |
|
initoo |
|- ( C e. Cat -> ( B e. ( InitO ` C ) -> B e. ( Base ` C ) ) ) |
12 |
1 3 11
|
sylc |
|- ( ph -> B e. ( Base ` C ) ) |
13 |
7 8 1 10 12
|
cic |
|- ( ph -> ( A ( ~=c ` C ) B <-> E. f f e. ( A ( Iso ` C ) B ) ) ) |
14 |
6 13
|
mpbird |
|- ( ph -> A ( ~=c ` C ) B ) |