| Step |
Hyp |
Ref |
Expression |
| 1 |
|
isinito2.1 |
|- .1. = ( SetCat ` 1o ) |
| 2 |
|
isinito2.f |
|- F = ( ( 1st ` ( .1. DiagFunc C ) ) ` (/) ) |
| 3 |
|
initorcl |
|- ( I e. ( InitO ` C ) -> C e. Cat ) |
| 4 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
| 5 |
4
|
initoo2 |
|- ( I e. ( InitO ` C ) -> I e. ( Base ` C ) ) |
| 6 |
1 2 3 5
|
isinito2lem |
|- ( I e. ( InitO ` C ) -> ( I e. ( InitO ` C ) <-> I ( F ( C UP .1. ) (/) ) (/) ) ) |
| 7 |
6
|
ibi |
|- ( I e. ( InitO ` C ) -> I ( F ( C UP .1. ) (/) ) (/) ) |
| 8 |
|
id |
|- ( I ( F ( C UP .1. ) (/) ) (/) -> I ( F ( C UP .1. ) (/) ) (/) ) |
| 9 |
8
|
up1st2nd |
|- ( I ( F ( C UP .1. ) (/) ) (/) -> I ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C UP .1. ) (/) ) (/) ) |
| 10 |
9
|
uprcl2 |
|- ( I ( F ( C UP .1. ) (/) ) (/) -> ( 1st ` F ) ( C Func .1. ) ( 2nd ` F ) ) |
| 11 |
10
|
funcrcl2 |
|- ( I ( F ( C UP .1. ) (/) ) (/) -> C e. Cat ) |
| 12 |
9 4
|
uprcl4 |
|- ( I ( F ( C UP .1. ) (/) ) (/) -> I e. ( Base ` C ) ) |
| 13 |
1 2 11 12
|
isinito2lem |
|- ( I ( F ( C UP .1. ) (/) ) (/) -> ( I e. ( InitO ` C ) <-> I ( F ( C UP .1. ) (/) ) (/) ) ) |
| 14 |
13
|
ibir |
|- ( I ( F ( C UP .1. ) (/) ) (/) -> I e. ( InitO ` C ) ) |
| 15 |
7 14
|
impbii |
|- ( I e. ( InitO ` C ) <-> I ( F ( C UP .1. ) (/) ) (/) ) |