Theorem thincsect2

Description: In a thin category, F is a section of G iff G is a section of F . (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 ) )