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