| 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 |
|
invfval.s |
|- S = ( Sect ` C ) |
| 7 |
1 2 3 4 5 6
|
invfval |
|- ( ph -> ( X N Y ) = ( ( X S Y ) i^i `' ( Y S X ) ) ) |
| 8 |
7
|
breqd |
|- ( ph -> ( F ( X N Y ) G <-> F ( ( X S Y ) i^i `' ( Y S X ) ) G ) ) |
| 9 |
|
brin |
|- ( F ( ( X S Y ) i^i `' ( Y S X ) ) G <-> ( F ( X S Y ) G /\ F `' ( Y S X ) G ) ) |
| 10 |
8 9
|
bitrdi |
|- ( ph -> ( F ( X N Y ) G <-> ( F ( X S Y ) G /\ F `' ( Y S X ) G ) ) ) |
| 11 |
|
eqid |
|- ( Hom ` C ) = ( Hom ` C ) |
| 12 |
|
eqid |
|- ( comp ` C ) = ( comp ` C ) |
| 13 |
|
eqid |
|- ( Id ` C ) = ( Id ` C ) |
| 14 |
1 11 12 13 6 3 5 4
|
sectss |
|- ( ph -> ( Y S X ) C_ ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) ) |
| 15 |
|
relxp |
|- Rel ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) |
| 16 |
|
relss |
|- ( ( Y S X ) C_ ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) -> ( Rel ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) -> Rel ( Y S X ) ) ) |
| 17 |
14 15 16
|
mpisyl |
|- ( ph -> Rel ( Y S X ) ) |
| 18 |
|
relbrcnvg |
|- ( Rel ( Y S X ) -> ( F `' ( Y S X ) G <-> G ( Y S X ) F ) ) |
| 19 |
17 18
|
syl |
|- ( ph -> ( F `' ( Y S X ) G <-> G ( Y S X ) F ) ) |
| 20 |
19
|
anbi2d |
|- ( ph -> ( ( F ( X S Y ) G /\ F `' ( Y S X ) G ) <-> ( F ( X S Y ) G /\ G ( Y S X ) F ) ) ) |
| 21 |
10 20
|
bitrd |
|- ( ph -> ( F ( X N Y ) G <-> ( F ( X S Y ) G /\ G ( Y S X ) F ) ) ) |