Step |
Hyp |
Ref |
Expression |
1 |
|
invfval.b |
|- B = ( Base ` C ) |
2 |
|
invfval.n |
|- N = ( Inv ` C ) |
3 |
|
invfval.c |
|- ( ph -> C e. Cat ) |
4 |
|
invfval.x |
|- ( ph -> X e. B ) |
5 |
|
invfval.y |
|- ( ph -> Y e. B ) |
6 |
|
isoval.n |
|- I = ( Iso ` C ) |
7 |
|
inviso1.1 |
|- ( ph -> F ( X N Y ) G ) |
8 |
1 2 3 4 5
|
invfun |
|- ( ph -> Fun ( X N Y ) ) |
9 |
|
funrel |
|- ( Fun ( X N Y ) -> Rel ( X N Y ) ) |
10 |
8 9
|
syl |
|- ( ph -> Rel ( X N Y ) ) |
11 |
|
releldm |
|- ( ( Rel ( X N Y ) /\ F ( X N Y ) G ) -> F e. dom ( X N Y ) ) |
12 |
10 7 11
|
syl2anc |
|- ( ph -> F e. dom ( X N Y ) ) |
13 |
1 2 3 4 5 6
|
isoval |
|- ( ph -> ( X I Y ) = dom ( X N Y ) ) |
14 |
12 13
|
eleqtrrd |
|- ( ph -> F e. ( X I Y ) ) |