Metamath Proof Explorer

Theorem dfiso3

Description: Alternate definition of an isomorphism of a category as a section in both directions. (Contributed by AV, 11-Apr-2020)

Ref Expression
Hypotheses dfiso3.b 
|- B = ( Base ` C )
dfiso3.h 
|- H = ( Hom ` C )
dfiso3.i 
|- I = ( Iso ` C )
dfiso3.s 
|- S = ( Sect ` C )
dfiso3.c 
|- ( ph -> C e. Cat )
dfiso3.x 
|- ( ph -> X e. B )
dfiso3.y 
|- ( ph -> Y e. B )
dfiso3.f 
|- ( ph -> F e. ( X H Y ) )
Assertion dfiso3 
|- ( ph -> ( F e. ( X I Y ) <-> E. g e. ( Y H X ) ( g ( Y S X ) F /\ F ( X S Y ) g ) ) )

Proof

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 ) ) )