This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem thincsect2

Description: In a thin category, F is a section of G iff G is a section of F . Example 7.25(4) of Adamek p. 108. (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 )
Assertion thincsect2 
|- ( ph -> ( F ( X S Y ) G <-> G ( Y S X ) F ) )

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 ancom 
 |-  ( ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) ) <-> ( G e. ( Y ( Hom ` C ) X ) /\ F e. ( X ( Hom ` C ) Y ) ) )
7 6 a1i 
 |-  ( ph -> ( ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) ) <-> ( G e. ( Y ( Hom ` C ) X ) /\ F e. ( X ( Hom ` C ) Y ) ) ) )
8 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
9 1 2 3 4 5 8 thincsect 
 |-  ( ph -> ( F ( X S Y ) G <-> ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) ) ) )
10 1 2 4 3 5 8 thincsect 
 |-  ( ph -> ( G ( Y S X ) F <-> ( G e. ( Y ( Hom ` C ) X ) /\ F e. ( X ( Hom ` C ) Y ) ) ) )
11 7 9 10 3bitr4d 
 |-  ( ph -> ( F ( X S Y ) G <-> G ( Y S X ) F ) )