Metamath Proof Explorer

Theorem thinciso

Description: In a thin category, F : X --> Y is an isomorphism iff there is a morphism from Y to X . (Contributed by Zhi Wang, 25-Sep-2024)

Ref Expression
Hypotheses thincsect.c 
|- ( ph -> C e. ThinCat )
thincsect.b 
|- B = ( Base ` C )
thincsect.x 
|- ( ph -> X e. B )
thincsect.y 
|- ( ph -> Y e. B )
thinciso.h 
|- H = ( Hom ` C )
thinciso.i 
|- I = ( Iso ` C )
thinciso.f 
|- ( ph -> F e. ( X H Y ) )
Assertion thinciso 
|- ( ph -> ( F e. ( X I Y ) <-> ( Y H X ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 thincsect.c 
 |-  ( ph -> C e. ThinCat )
2 thincsect.b 
 |-  B = ( Base ` C )
3 thincsect.x 
 |-  ( ph -> X e. B )
4 thincsect.y 
 |-  ( ph -> Y e. B )
5 thinciso.h 
 |-  H = ( Hom ` C )
6 thinciso.i 
 |-  I = ( Iso ` C )
7 thinciso.f 
 |-  ( ph -> F e. ( X H Y ) )
8 eqid 
 |-  ( Sect ` C ) = ( Sect ` C )
9 1 thinccd 
 |-  ( ph -> C e. Cat )
10 2 5 6 8 9 3 4 7 dfiso3 
 |-  ( ph -> ( F e. ( X I Y ) <-> E. g e. ( Y H X ) ( g ( Y ( Sect ` C ) X ) F /\ F ( X ( Sect ` C ) Y ) g ) ) )
11 simprl 
 |-  ( ( ( ph /\ ( Y H X ) =/= (/) ) /\ ( g e. ( Y H X ) /\ T. ) ) -> g e. ( Y H X ) )
12 7 ad2antrr 
 |-  ( ( ( ph /\ ( Y H X ) =/= (/) ) /\ ( g e. ( Y H X ) /\ T. ) ) -> F e. ( X H Y ) )
13 1 ad2antrr 
 |-  ( ( ( ph /\ ( Y H X ) =/= (/) ) /\ ( g e. ( Y H X ) /\ T. ) ) -> C e. ThinCat )
14 4 ad2antrr 
 |-  ( ( ( ph /\ ( Y H X ) =/= (/) ) /\ ( g e. ( Y H X ) /\ T. ) ) -> Y e. B )
15 3 ad2antrr 
 |-  ( ( ( ph /\ ( Y H X ) =/= (/) ) /\ ( g e. ( Y H X ) /\ T. ) ) -> X e. B )
16 13 2 14 15 8 5 thincsect 
 |-  ( ( ( ph /\ ( Y H X ) =/= (/) ) /\ ( g e. ( Y H X ) /\ T. ) ) -> ( g ( Y ( Sect ` C ) X ) F <-> ( g e. ( Y H X ) /\ F e. ( X H Y ) ) ) )
17 11 12 16 mpbir2and 
 |-  ( ( ( ph /\ ( Y H X ) =/= (/) ) /\ ( g e. ( Y H X ) /\ T. ) ) -> g ( Y ( Sect ` C ) X ) F )
18 13 2 15 14 8 5 thincsect 
 |-  ( ( ( ph /\ ( Y H X ) =/= (/) ) /\ ( g e. ( Y H X ) /\ T. ) ) -> ( F ( X ( Sect ` C ) Y ) g <-> ( F e. ( X H Y ) /\ g e. ( Y H X ) ) ) )
19 12 11 18 mpbir2and 
 |-  ( ( ( ph /\ ( Y H X ) =/= (/) ) /\ ( g e. ( Y H X ) /\ T. ) ) -> F ( X ( Sect ` C ) Y ) g )
20 17 19 jca 
 |-  ( ( ( ph /\ ( Y H X ) =/= (/) ) /\ ( g e. ( Y H X ) /\ T. ) ) -> ( g ( Y ( Sect ` C ) X ) F /\ F ( X ( Sect ` C ) Y ) g ) )
21 trud 
 |-  ( ( ph /\ g e. ( Y H X ) ) -> T. )
22 21 reximdva0 
 |-  ( ( ph /\ ( Y H X ) =/= (/) ) -> E. g e. ( Y H X ) T. )
23 20 22 reximddv 
 |-  ( ( ph /\ ( Y H X ) =/= (/) ) -> E. g e. ( Y H X ) ( g ( Y ( Sect ` C ) X ) F /\ F ( X ( Sect ` C ) Y ) g ) )
24 rexn0 
 |-  ( E. g e. ( Y H X ) ( g ( Y ( Sect ` C ) X ) F /\ F ( X ( Sect ` C ) Y ) g ) -> ( Y H X ) =/= (/) )
25 24 adantl 
 |-  ( ( ph /\ E. g e. ( Y H X ) ( g ( Y ( Sect ` C ) X ) F /\ F ( X ( Sect ` C ) Y ) g ) ) -> ( Y H X ) =/= (/) )
26 23 25 impbida 
 |-  ( ph -> ( ( Y H X ) =/= (/) <-> E. g e. ( Y H X ) ( g ( Y ( Sect ` C ) X ) F /\ F ( X ( Sect ` C ) Y ) g ) ) )
27 10 26 bitr4d 
 |-  ( ph -> ( F e. ( X I Y ) <-> ( Y H X ) =/= (/) ) )