This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )