Theorem thincinv

Description: In a thin category, F is an inverse of G iff F is a section of G . Example 7.20(7) of Adamek p. 107. (Contributed by Zhi Wang, 24-Sep-2024)

	Ref	Expression
Hypotheses	thincsect.c	$$⊢\phi \to C\in \mathrm{ThinCat}$$
	thincsect.b	$$⊢B={\mathrm{Base}}_C$$
	thincsect.x	$$⊢\phi \to X\in B$$
	thincsect.y	$$⊢\phi \to Y\in B$$
	thincsect.s	$$⊢S=\mathrm{Sect}\left(C\right)$$
	thincinv.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
Assertion	thincinv	$$⊢\phi \to \left(F\left(XNY\right)G\leftrightarrow F\left(XSY\right)G\right)$$

Proof

Step	Hyp	Ref	Expression
1		thincsect.c	$$⊢\phi \to C\in \mathrm{ThinCat}$$
2		thincsect.b	$$⊢B={\mathrm{Base}}_C$$
3		thincsect.x	$$⊢\phi \to X\in B$$
4		thincsect.y	$$⊢\phi \to Y\in B$$
5		thincsect.s	$$⊢S=\mathrm{Sect}\left(C\right)$$
6		thincinv.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
7	1	thinccatd	$$⊢\phi \to C\in \mathrm{Cat}$$
8	2 6 7 3 4 5	isinv	$$⊢\phi \to \left(F\left(XNY\right)G\leftrightarrow \left(F\left(XSY\right)G\wedge G\left(YSX\right)F\right)\right)$$
9	1 2 3 4 5	thincsect2	$$⊢\phi \to \left(F\left(XSY\right)G\leftrightarrow G\left(YSX\right)F\right)$$
10	9	biimpa	$$⊢\left(\phi \wedge F\left(XSY\right)G\right)\to G\left(YSX\right)F$$
11	8 10	mpbiran3d	$$⊢\phi \to \left(F\left(XNY\right)G\leftrightarrow F\left(XSY\right)G\right)$$