Step |
Hyp |
Ref |
Expression |
1 |
|
isohom.b |
|- B = ( Base ` C ) |
2 |
|
isohom.h |
|- H = ( Hom ` C ) |
3 |
|
isohom.i |
|- I = ( Iso ` C ) |
4 |
|
isohom.c |
|- ( ph -> C e. Cat ) |
5 |
|
isohom.x |
|- ( ph -> X e. B ) |
6 |
|
isohom.y |
|- ( ph -> Y e. B ) |
7 |
|
eqid |
|- ( Inv ` C ) = ( Inv ` C ) |
8 |
1 7 4 5 6 3
|
isoval |
|- ( ph -> ( X I Y ) = dom ( X ( Inv ` C ) Y ) ) |
9 |
1 7 4 5 6 2
|
invss |
|- ( ph -> ( X ( Inv ` C ) Y ) C_ ( ( X H Y ) X. ( Y H X ) ) ) |
10 |
|
dmss |
|- ( ( X ( Inv ` C ) Y ) C_ ( ( X H Y ) X. ( Y H X ) ) -> dom ( X ( Inv ` C ) Y ) C_ dom ( ( X H Y ) X. ( Y H X ) ) ) |
11 |
9 10
|
syl |
|- ( ph -> dom ( X ( Inv ` C ) Y ) C_ dom ( ( X H Y ) X. ( Y H X ) ) ) |
12 |
8 11
|
eqsstrd |
|- ( ph -> ( X I Y ) C_ dom ( ( X H Y ) X. ( Y H X ) ) ) |
13 |
|
dmxpss |
|- dom ( ( X H Y ) X. ( Y H X ) ) C_ ( X H Y ) |
14 |
12 13
|
sstrdi |
|- ( ph -> ( X I Y ) C_ ( X H Y ) ) |