| Step |
Hyp |
Ref |
Expression |
| 1 |
|
prstcnid.c |
|- ( ph -> C = ( ProsetToCat ` K ) ) |
| 2 |
|
prstcnid.k |
|- ( ph -> K e. Proset ) |
| 3 |
|
eqidd |
|- ( ph -> ( Base ` C ) = ( Base ` C ) ) |
| 4 |
|
eqidd |
|- ( ph -> ( le ` C ) = ( le ` C ) ) |
| 5 |
1 2 4
|
prstchomval |
|- ( ph -> ( ( le ` C ) X. { 1o } ) = ( Hom ` C ) ) |
| 6 |
|
ovex |
|- ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) e. _V |
| 7 |
|
0ex |
|- (/) e. _V |
| 8 |
|
ccoid |
|- comp = Slot ( comp ` ndx ) |
| 9 |
8
|
setsid |
|- ( ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) e. _V /\ (/) e. _V ) -> (/) = ( comp ` ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) ) |
| 10 |
6 7 9
|
mp2an |
|- (/) = ( comp ` ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) |
| 11 |
1 2
|
prstcval |
|- ( ph -> C = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) |
| 12 |
11
|
fveq2d |
|- ( ph -> ( comp ` C ) = ( comp ` ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) ) |
| 13 |
10 12
|
eqtr4id |
|- ( ph -> (/) = ( comp ` C ) ) |
| 14 |
1 2
|
prstcprs |
|- ( ph -> C e. Proset ) |
| 15 |
3 5 13 4 14
|
prsthinc |
|- ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. ( Base ` C ) |-> (/) ) ) ) |
| 16 |
15
|
simpld |
|- ( ph -> C e. ThinCat ) |