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 |
|
eqid |
|- ( Sect ` C ) = ( Sect ` C ) |
7 |
1 2 3 4 5 6
|
isinv |
|- ( ph -> ( F ( X N Y ) G <-> ( F ( X ( Sect ` C ) Y ) G /\ G ( Y ( Sect ` C ) X ) F ) ) ) |
8 |
7
|
biancomd |
|- ( ph -> ( F ( X N Y ) G <-> ( G ( Y ( Sect ` C ) X ) F /\ F ( X ( Sect ` C ) Y ) G ) ) ) |
9 |
1 2 3 5 4 6
|
isinv |
|- ( ph -> ( G ( Y N X ) F <-> ( G ( Y ( Sect ` C ) X ) F /\ F ( X ( Sect ` C ) Y ) G ) ) ) |
10 |
8 9
|
bitr4d |
|- ( ph -> ( F ( X N Y ) G <-> G ( Y N X ) F ) ) |