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 = {id}_{func} (X)$
	catcinv.j	$⊢ J = {id}_{func} (Y)$
Assertion	catcinv	$⊢ F (X N Y) G \leftrightarrow ((F \in (X H Y) \land G \in (Y H X)) \land (G \circ_{func} F = I \land F \circ_{func} G = J))$

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 = {id}_{func} (X)$
5		catcinv.j	$⊢ J = {id}_{func} (Y)$
6		eqid	$⊢ Sect (C) = Sect (C)$
7	1 3 4 6	catcsect	$⊢ F (X Sect (C) Y) G \leftrightarrow ((F \in (X H Y) \land G \in (Y H X)) \land G \circ_{func} F = I)$
8	1 3 5 6	catcsect	$⊢ G (Y Sect (C) X) F \leftrightarrow ((G \in (Y H X) \land F \in (X H Y)) \land F \circ_{func} G = J)$
9		ancom	$⊢ (G \in (Y H X) \land F \in (X H Y)) \leftrightarrow (F \in (X H Y) \land G \in (Y H X))$
10	8 9	bianbi	$⊢ G (Y Sect (C) X) F \leftrightarrow ((F \in (X H Y) \land G \in (Y H X)) \land F \circ_{func} G = J)$
11	7 10	anbi12i	$⊢ (F (X Sect (C) Y) G \land G (Y Sect (C) X) F) \leftrightarrow (((F \in (X H Y) \land G \in (Y H X)) \land G \circ_{func} F = I) \land ((F \in (X H Y) \land G \in (Y H X)) \land F \circ_{func} G = J))$
12	2 6	isinv2	$⊢ F (X N Y) G \leftrightarrow (F (X Sect (C) Y) G \land G (Y Sect (C) X) F)$
13		anandi	$⊢ ((F \in (X H Y) \land G \in (Y H X)) \land (G \circ_{func} F = I \land F \circ_{func} G = J)) \leftrightarrow (((F \in (X H Y) \land G \in (Y H X)) \land G \circ_{func} F = I) \land ((F \in (X H Y) \land G \in (Y H X)) \land F \circ_{func} G = J))$
14	11 12 13	3bitr4i	$⊢ F (X N Y) G \leftrightarrow ((F \in (X H Y) \land G \in (Y H X)) \land (G \circ_{func} F = I \land F \circ_{func} G = J))$

Metamath Proof Explorer