Theorem catcinv

Description: The property " F is an inverse of G " in a category of small categories (in a universe). (Contributed by Zhi Wang, 14-Nov-2025)

	Ref	Expression
Hypotheses	catcinv.c	|- C = ( CatCat ` U )
	catcinv.n	|- N = ( Inv ` C )
	catcinv.h	|- H = ( Hom ` C )
	catcinv.i	|- I = ( idFunc ` X )
	catcinv.j	|- J = ( idFunc ` Y )
Assertion	catcinv	|- ( F ( X N Y ) G <-> ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( ( G o.func F ) = I /\ ( F o.func G ) = J ) ) )

Proof

Step	Hyp	Ref	Expression
1		catcinv.c	|- C = ( CatCat ` U )
2		catcinv.n	|- N = ( Inv ` C )
3		catcinv.h	|- H = ( Hom ` C )
4		catcinv.i	|- I = ( idFunc ` X )
5		catcinv.j	|- J = ( idFunc ` Y )
6		eqid	|- ( Sect ` C ) = ( Sect ` C )
7	1 3 4 6	catcsect	|- ( F ( X ( Sect ` C ) Y ) G <-> ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( G o.func F ) = I ) )
8	1 3 5 6	catcsect	|- ( G ( Y ( Sect ` C ) X ) F <-> ( ( G e. ( Y H X ) /\ F e. ( X H Y ) ) /\ ( F o.func G ) = J ) )
9		ancom	|- ( ( G e. ( Y H X ) /\ F e. ( X H Y ) ) <-> ( F e. ( X H Y ) /\ G e. ( Y H X ) ) )
10	8 9	bianbi	|- ( G ( Y ( Sect ` C ) X ) F <-> ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( F o.func G ) = J ) )
11	7 10	anbi12i	|- ( ( F ( X ( Sect ` C ) Y ) G /\ G ( Y ( Sect ` C ) X ) F ) <-> ( ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( G o.func F ) = I ) /\ ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( F o.func G ) = J ) ) )
12	2 6	isinv2	|- ( F ( X N Y ) G <-> ( F ( X ( Sect ` C ) Y ) G /\ G ( Y ( Sect ` C ) X ) F ) )
13		anandi	|- ( ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( ( G o.func F ) = I /\ ( F o.func G ) = J ) ) <-> ( ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( G o.func F ) = I ) /\ ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( F o.func G ) = J ) ) )
14	11 12 13	3bitr4i	|- ( F ( X N Y ) G <-> ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( ( G o.func F ) = I /\ ( F o.func G ) = J ) ) )