Step |
Hyp |
Ref |
Expression |
1 |
|
invisoinv.b |
|- B = ( Base ` C ) |
2 |
|
invisoinv.i |
|- I = ( Iso ` C ) |
3 |
|
invisoinv.n |
|- N = ( Inv ` C ) |
4 |
|
invisoinv.c |
|- ( ph -> C e. Cat ) |
5 |
|
invisoinv.x |
|- ( ph -> X e. B ) |
6 |
|
invisoinv.y |
|- ( ph -> Y e. B ) |
7 |
|
invisoinv.f |
|- ( ph -> F e. ( X I Y ) ) |
8 |
|
eqid |
|- ( comp ` C ) = ( comp ` C ) |
9 |
|
eqid |
|- ( Id ` C ) = ( Id ` C ) |
10 |
1 9 4 6
|
idiso |
|- ( ph -> ( ( Id ` C ) ` Y ) e. ( Y ( Iso ` C ) Y ) ) |
11 |
2
|
a1i |
|- ( ph -> I = ( Iso ` C ) ) |
12 |
11
|
oveqd |
|- ( ph -> ( Y I Y ) = ( Y ( Iso ` C ) Y ) ) |
13 |
10 12
|
eleqtrrd |
|- ( ph -> ( ( Id ` C ) ` Y ) e. ( Y I Y ) ) |
14 |
1 3 4 5 6 2 7 8 6 13
|
invco |
|- ( ph -> ( ( ( Id ` C ) ` Y ) ( <. X , Y >. ( comp ` C ) Y ) F ) ( X N Y ) ( ( ( X N Y ) ` F ) ( <. Y , Y >. ( comp ` C ) X ) ( ( Y N Y ) ` ( ( Id ` C ) ` Y ) ) ) ) |
15 |
|
eqid |
|- ( Hom ` C ) = ( Hom ` C ) |
16 |
1 15 2 4 5 6
|
isohom |
|- ( ph -> ( X I Y ) C_ ( X ( Hom ` C ) Y ) ) |
17 |
16 7
|
sseldd |
|- ( ph -> F e. ( X ( Hom ` C ) Y ) ) |
18 |
1 15 9 4 5 8 6 17
|
catlid |
|- ( ph -> ( ( ( Id ` C ) ` Y ) ( <. X , Y >. ( comp ` C ) Y ) F ) = F ) |
19 |
3
|
a1i |
|- ( ph -> N = ( Inv ` C ) ) |
20 |
19
|
oveqd |
|- ( ph -> ( Y N Y ) = ( Y ( Inv ` C ) Y ) ) |
21 |
20
|
fveq1d |
|- ( ph -> ( ( Y N Y ) ` ( ( Id ` C ) ` Y ) ) = ( ( Y ( Inv ` C ) Y ) ` ( ( Id ` C ) ` Y ) ) ) |
22 |
1 9 4 6
|
idinv |
|- ( ph -> ( ( Y ( Inv ` C ) Y ) ` ( ( Id ` C ) ` Y ) ) = ( ( Id ` C ) ` Y ) ) |
23 |
21 22
|
eqtrd |
|- ( ph -> ( ( Y N Y ) ` ( ( Id ` C ) ` Y ) ) = ( ( Id ` C ) ` Y ) ) |
24 |
23
|
oveq2d |
|- ( ph -> ( ( ( X N Y ) ` F ) ( <. Y , Y >. ( comp ` C ) X ) ( ( Y N Y ) ` ( ( Id ` C ) ` Y ) ) ) = ( ( ( X N Y ) ` F ) ( <. Y , Y >. ( comp ` C ) X ) ( ( Id ` C ) ` Y ) ) ) |
25 |
1 15 2 4 6 5
|
isohom |
|- ( ph -> ( Y I X ) C_ ( Y ( Hom ` C ) X ) ) |
26 |
1 3 4 5 6 2
|
invf |
|- ( ph -> ( X N Y ) : ( X I Y ) --> ( Y I X ) ) |
27 |
26 7
|
ffvelrnd |
|- ( ph -> ( ( X N Y ) ` F ) e. ( Y I X ) ) |
28 |
25 27
|
sseldd |
|- ( ph -> ( ( X N Y ) ` F ) e. ( Y ( Hom ` C ) X ) ) |
29 |
1 15 9 4 6 8 5 28
|
catrid |
|- ( ph -> ( ( ( X N Y ) ` F ) ( <. Y , Y >. ( comp ` C ) X ) ( ( Id ` C ) ` Y ) ) = ( ( X N Y ) ` F ) ) |
30 |
24 29
|
eqtrd |
|- ( ph -> ( ( ( X N Y ) ` F ) ( <. Y , Y >. ( comp ` C ) X ) ( ( Y N Y ) ` ( ( Id ` C ) ` Y ) ) ) = ( ( X N Y ) ` F ) ) |
31 |
14 18 30
|
3brtr3d |
|- ( ph -> F ( X N Y ) ( ( X N Y ) ` F ) ) |
32 |
1 3 4 6 5
|
invsym |
|- ( ph -> ( ( ( X N Y ) ` F ) ( Y N X ) F <-> F ( X N Y ) ( ( X N Y ) ` F ) ) ) |
33 |
31 32
|
mpbird |
|- ( ph -> ( ( X N Y ) ` F ) ( Y N X ) F ) |