| Step |
Hyp |
Ref |
Expression |
| 1 |
|
funcsetc1o.1 |
|- .1. = ( SetCat ` 1o ) |
| 2 |
|
df-ot |
|- <. (/) , (/) , 1o >. = <. <. (/) , (/) >. , 1o >. |
| 3 |
2
|
sneqi |
|- { <. (/) , (/) , 1o >. } = { <. <. (/) , (/) >. , 1o >. } |
| 4 |
|
0ex |
|- (/) e. _V |
| 5 |
|
1oex |
|- 1o e. _V |
| 6 |
|
df1o2 |
|- 1o = { (/) } |
| 7 |
6
|
fveq2i |
|- ( SetCat ` 1o ) = ( SetCat ` { (/) } ) |
| 8 |
1 7
|
eqtri |
|- .1. = ( SetCat ` { (/) } ) |
| 9 |
|
p0ex |
|- { (/) } e. _V |
| 10 |
9
|
a1i |
|- ( T. -> { (/) } e. _V ) |
| 11 |
|
eqid |
|- ( Hom ` .1. ) = ( Hom ` .1. ) |
| 12 |
8 10 11
|
setchomfval |
|- ( T. -> ( Hom ` .1. ) = ( x e. { (/) } , y e. { (/) } |-> ( y ^m x ) ) ) |
| 13 |
12
|
mptru |
|- ( Hom ` .1. ) = ( x e. { (/) } , y e. { (/) } |-> ( y ^m x ) ) |
| 14 |
|
oveq2 |
|- ( x = (/) -> ( y ^m x ) = ( y ^m (/) ) ) |
| 15 |
|
oveq1 |
|- ( y = (/) -> ( y ^m (/) ) = ( (/) ^m (/) ) ) |
| 16 |
|
0map0sn0 |
|- ( (/) ^m (/) ) = { (/) } |
| 17 |
16 6
|
eqtr4i |
|- ( (/) ^m (/) ) = 1o |
| 18 |
15 17
|
eqtrdi |
|- ( y = (/) -> ( y ^m (/) ) = 1o ) |
| 19 |
13 14 18
|
mposn |
|- ( ( (/) e. _V /\ (/) e. _V /\ 1o e. _V ) -> ( Hom ` .1. ) = { <. <. (/) , (/) >. , 1o >. } ) |
| 20 |
4 4 5 19
|
mp3an |
|- ( Hom ` .1. ) = { <. <. (/) , (/) >. , 1o >. } |
| 21 |
3 20
|
eqtr4i |
|- { <. (/) , (/) , 1o >. } = ( Hom ` .1. ) |