Theorem thincinv

Description: In a thin category, F is an inverse of G iff F is a section of G (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 )
	thincinv.n	|- N = ( Inv ` C )
Assertion	thincinv	|- ( ph -> ( F ( X N Y ) G <-> F ( X S Y ) G ) )

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		thincinv.n	|- N = ( Inv ` C )
7	1	thinccd	|- ( ph -> C e. Cat )
8	2 6 7 3 4 5	isinv	|- ( ph -> ( F ( X N Y ) G <-> ( F ( X S Y ) G /\ G ( Y S X ) F ) ) )
9	1 2 3 4 5	thincsect2	|- ( ph -> ( F ( X S Y ) G <-> G ( Y S X ) F ) )
10	9	biimpa	|- ( ( ph /\ F ( X S Y ) G ) -> G ( Y S X ) F )
11	8 10	mpbiran3d	|- ( ph -> ( F ( X N Y ) G <-> F ( X S Y ) G ) )