Metamath Proof Explorer

Theorem thincsect

Description: In a thin category, one morphism is a section of another iff they are pointing towards each other. (Contributed by Zhi Wang, 24-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 )
thincsect.s 
|- S = ( Sect ` C )
thincsect.h 
|- H = ( Hom ` C )
Assertion thincsect 
|- ( ph -> ( F ( X S Y ) G <-> ( F e. ( X H Y ) /\ G e. ( 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 thincsect.s 
 |-  S = ( Sect ` C )
6 thincsect.h 
 |-  H = ( Hom ` C )
7 eqid 
 |-  ( comp ` C ) = ( comp ` C )
8 eqid 
 |-  ( Id ` C ) = ( Id ` C )
9 1 thinccd 
 |-  ( ph -> C e. Cat )
10 2 6 7 8 5 9 3 4 issect 
 |-  ( ph -> ( F ( X S Y ) G <-> ( F e. ( X H Y ) /\ G e. ( Y H X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) ) )
11 df-3an 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) <-> ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) )
12 10 11 bitrdi 
 |-  ( ph -> ( F ( X S Y ) G <-> ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) ) )
13 1 adantr 
 |-  ( ( ph /\ ( F e. ( X H Y ) /\ G e. ( Y H X ) ) ) -> C e. ThinCat )
14 3 adantr 
 |-  ( ( ph /\ ( F e. ( X H Y ) /\ G e. ( Y H X ) ) ) -> X e. B )
15 9 adantr 
 |-  ( ( ph /\ ( F e. ( X H Y ) /\ G e. ( Y H X ) ) ) -> C e. Cat )
16 4 adantr 
 |-  ( ( ph /\ ( F e. ( X H Y ) /\ G e. ( Y H X ) ) ) -> Y e. B )
17 simprl 
 |-  ( ( ph /\ ( F e. ( X H Y ) /\ G e. ( Y H X ) ) ) -> F e. ( X H Y ) )
18 simprr 
 |-  ( ( ph /\ ( F e. ( X H Y ) /\ G e. ( Y H X ) ) ) -> G e. ( Y H X ) )
19 2 6 7 15 14 16 14 17 18 catcocl 
 |-  ( ( ph /\ ( F e. ( X H Y ) /\ G e. ( Y H X ) ) ) -> ( G ( <. X , Y >. ( comp ` C ) X ) F ) e. ( X H X ) )
20 13 2 6 14 8 19 thincid 
 |-  ( ( ph /\ ( F e. ( X H Y ) /\ G e. ( Y H X ) ) ) -> ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) )
21 12 20 mpbiran3d 
 |-  ( ph -> ( F ( X S Y ) G <-> ( F e. ( X H Y ) /\ G e. ( Y H X ) ) ) )