Step |
Hyp |
Ref |
Expression |
1 |
|
dfiso3.b |
|- B = ( Base ` C ) |
2 |
|
dfiso3.h |
|- H = ( Hom ` C ) |
3 |
|
dfiso3.i |
|- I = ( Iso ` C ) |
4 |
|
dfiso3.s |
|- S = ( Sect ` C ) |
5 |
|
dfiso3.c |
|- ( ph -> C e. Cat ) |
6 |
|
dfiso3.x |
|- ( ph -> X e. B ) |
7 |
|
dfiso3.y |
|- ( ph -> Y e. B ) |
8 |
|
dfiso3.f |
|- ( ph -> F e. ( X H Y ) ) |
9 |
|
eqid |
|- ( Id ` C ) = ( Id ` C ) |
10 |
|
eqid |
|- ( <. X , Y >. ( comp ` C ) X ) = ( <. X , Y >. ( comp ` C ) X ) |
11 |
|
eqid |
|- ( <. Y , X >. ( comp ` C ) Y ) = ( <. Y , X >. ( comp ` C ) Y ) |
12 |
1 2 5 3 6 7 8 9 10 11
|
dfiso2 |
|- ( ph -> ( F e. ( X I Y ) <-> E. g e. ( Y H X ) ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( ( Id ` C ) ` Y ) ) ) ) |
13 |
|
eqid |
|- ( comp ` C ) = ( comp ` C ) |
14 |
5
|
adantr |
|- ( ( ph /\ g e. ( Y H X ) ) -> C e. Cat ) |
15 |
7
|
adantr |
|- ( ( ph /\ g e. ( Y H X ) ) -> Y e. B ) |
16 |
6
|
adantr |
|- ( ( ph /\ g e. ( Y H X ) ) -> X e. B ) |
17 |
|
simpr |
|- ( ( ph /\ g e. ( Y H X ) ) -> g e. ( Y H X ) ) |
18 |
8
|
adantr |
|- ( ( ph /\ g e. ( Y H X ) ) -> F e. ( X H Y ) ) |
19 |
1 2 13 9 4 14 15 16 17 18
|
issect2 |
|- ( ( ph /\ g e. ( Y H X ) ) -> ( g ( Y S X ) F <-> ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( ( Id ` C ) ` Y ) ) ) |
20 |
1 2 13 9 4 14 16 15 18 17
|
issect2 |
|- ( ( ph /\ g e. ( Y H X ) ) -> ( F ( X S Y ) g <-> ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) ) |
21 |
19 20
|
anbi12d |
|- ( ( ph /\ g e. ( Y H X ) ) -> ( ( g ( Y S X ) F /\ F ( X S Y ) g ) <-> ( ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( ( Id ` C ) ` Y ) /\ ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) ) ) |
22 |
|
ancom |
|- ( ( ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( ( Id ` C ) ` Y ) /\ ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) <-> ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( ( Id ` C ) ` Y ) ) ) |
23 |
21 22
|
bitr2di |
|- ( ( ph /\ g e. ( Y H X ) ) -> ( ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( ( Id ` C ) ` Y ) ) <-> ( g ( Y S X ) F /\ F ( X S Y ) g ) ) ) |
24 |
23
|
rexbidva |
|- ( ph -> ( E. g e. ( Y H X ) ( ( g ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) g ) = ( ( Id ` C ) ` Y ) ) <-> E. g e. ( Y H X ) ( g ( Y S X ) F /\ F ( X S Y ) g ) ) ) |
25 |
12 24
|
bitrd |
|- ( ph -> ( F e. ( X I Y ) <-> E. g e. ( Y H X ) ( g ( Y S X ) F /\ F ( X S Y ) g ) ) ) |