Metamath Proof Explorer


Theorem setcinv

Description: An inverse in the category of sets is the converse operation. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses setcmon.c
|- C = ( SetCat ` U )
setcmon.u
|- ( ph -> U e. V )
setcmon.x
|- ( ph -> X e. U )
setcmon.y
|- ( ph -> Y e. U )
setcinv.n
|- N = ( Inv ` C )
Assertion setcinv
|- ( ph -> ( F ( X N Y ) G <-> ( F : X -1-1-onto-> Y /\ G = `' F ) ) )

Proof

Step Hyp Ref Expression
1 setcmon.c
 |-  C = ( SetCat ` U )
2 setcmon.u
 |-  ( ph -> U e. V )
3 setcmon.x
 |-  ( ph -> X e. U )
4 setcmon.y
 |-  ( ph -> Y e. U )
5 setcinv.n
 |-  N = ( Inv ` C )
6 eqid
 |-  ( Base ` C ) = ( Base ` C )
7 1 setccat
 |-  ( U e. V -> C e. Cat )
8 2 7 syl
 |-  ( ph -> C e. Cat )
9 1 2 setcbas
 |-  ( ph -> U = ( Base ` C ) )
10 3 9 eleqtrd
 |-  ( ph -> X e. ( Base ` C ) )
11 4 9 eleqtrd
 |-  ( ph -> Y e. ( Base ` C ) )
12 eqid
 |-  ( Sect ` C ) = ( Sect ` C )
13 6 5 8 10 11 12 isinv
 |-  ( ph -> ( F ( X N Y ) G <-> ( F ( X ( Sect ` C ) Y ) G /\ G ( Y ( Sect ` C ) X ) F ) ) )
14 1 2 3 4 12 setcsect
 |-  ( ph -> ( F ( X ( Sect ` C ) Y ) G <-> ( F : X --> Y /\ G : Y --> X /\ ( G o. F ) = ( _I |` X ) ) ) )
15 df-3an
 |-  ( ( F : X --> Y /\ G : Y --> X /\ ( G o. F ) = ( _I |` X ) ) <-> ( ( F : X --> Y /\ G : Y --> X ) /\ ( G o. F ) = ( _I |` X ) ) )
16 14 15 bitrdi
 |-  ( ph -> ( F ( X ( Sect ` C ) Y ) G <-> ( ( F : X --> Y /\ G : Y --> X ) /\ ( G o. F ) = ( _I |` X ) ) ) )
17 1 2 4 3 12 setcsect
 |-  ( ph -> ( G ( Y ( Sect ` C ) X ) F <-> ( G : Y --> X /\ F : X --> Y /\ ( F o. G ) = ( _I |` Y ) ) ) )
18 3ancoma
 |-  ( ( G : Y --> X /\ F : X --> Y /\ ( F o. G ) = ( _I |` Y ) ) <-> ( F : X --> Y /\ G : Y --> X /\ ( F o. G ) = ( _I |` Y ) ) )
19 df-3an
 |-  ( ( F : X --> Y /\ G : Y --> X /\ ( F o. G ) = ( _I |` Y ) ) <-> ( ( F : X --> Y /\ G : Y --> X ) /\ ( F o. G ) = ( _I |` Y ) ) )
20 18 19 bitri
 |-  ( ( G : Y --> X /\ F : X --> Y /\ ( F o. G ) = ( _I |` Y ) ) <-> ( ( F : X --> Y /\ G : Y --> X ) /\ ( F o. G ) = ( _I |` Y ) ) )
21 17 20 bitrdi
 |-  ( ph -> ( G ( Y ( Sect ` C ) X ) F <-> ( ( F : X --> Y /\ G : Y --> X ) /\ ( F o. G ) = ( _I |` Y ) ) ) )
22 16 21 anbi12d
 |-  ( ph -> ( ( F ( X ( Sect ` C ) Y ) G /\ G ( Y ( Sect ` C ) X ) F ) <-> ( ( ( F : X --> Y /\ G : Y --> X ) /\ ( G o. F ) = ( _I |` X ) ) /\ ( ( F : X --> Y /\ G : Y --> X ) /\ ( F o. G ) = ( _I |` Y ) ) ) ) )
23 anandi
 |-  ( ( ( F : X --> Y /\ G : Y --> X ) /\ ( ( G o. F ) = ( _I |` X ) /\ ( F o. G ) = ( _I |` Y ) ) ) <-> ( ( ( F : X --> Y /\ G : Y --> X ) /\ ( G o. F ) = ( _I |` X ) ) /\ ( ( F : X --> Y /\ G : Y --> X ) /\ ( F o. G ) = ( _I |` Y ) ) ) )
24 22 23 bitr4di
 |-  ( ph -> ( ( F ( X ( Sect ` C ) Y ) G /\ G ( Y ( Sect ` C ) X ) F ) <-> ( ( F : X --> Y /\ G : Y --> X ) /\ ( ( G o. F ) = ( _I |` X ) /\ ( F o. G ) = ( _I |` Y ) ) ) ) )
25 fcof1o
 |-  ( ( ( F : X --> Y /\ G : Y --> X ) /\ ( ( F o. G ) = ( _I |` Y ) /\ ( G o. F ) = ( _I |` X ) ) ) -> ( F : X -1-1-onto-> Y /\ `' F = G ) )
26 eqcom
 |-  ( `' F = G <-> G = `' F )
27 26 anbi2i
 |-  ( ( F : X -1-1-onto-> Y /\ `' F = G ) <-> ( F : X -1-1-onto-> Y /\ G = `' F ) )
28 25 27 sylib
 |-  ( ( ( F : X --> Y /\ G : Y --> X ) /\ ( ( F o. G ) = ( _I |` Y ) /\ ( G o. F ) = ( _I |` X ) ) ) -> ( F : X -1-1-onto-> Y /\ G = `' F ) )
29 28 ancom2s
 |-  ( ( ( F : X --> Y /\ G : Y --> X ) /\ ( ( G o. F ) = ( _I |` X ) /\ ( F o. G ) = ( _I |` Y ) ) ) -> ( F : X -1-1-onto-> Y /\ G = `' F ) )
30 29 adantl
 |-  ( ( ph /\ ( ( F : X --> Y /\ G : Y --> X ) /\ ( ( G o. F ) = ( _I |` X ) /\ ( F o. G ) = ( _I |` Y ) ) ) ) -> ( F : X -1-1-onto-> Y /\ G = `' F ) )
31 f1of
 |-  ( F : X -1-1-onto-> Y -> F : X --> Y )
32 31 ad2antrl
 |-  ( ( ph /\ ( F : X -1-1-onto-> Y /\ G = `' F ) ) -> F : X --> Y )
33 f1ocnv
 |-  ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X )
34 33 ad2antrl
 |-  ( ( ph /\ ( F : X -1-1-onto-> Y /\ G = `' F ) ) -> `' F : Y -1-1-onto-> X )
35 f1oeq1
 |-  ( G = `' F -> ( G : Y -1-1-onto-> X <-> `' F : Y -1-1-onto-> X ) )
36 35 ad2antll
 |-  ( ( ph /\ ( F : X -1-1-onto-> Y /\ G = `' F ) ) -> ( G : Y -1-1-onto-> X <-> `' F : Y -1-1-onto-> X ) )
37 34 36 mpbird
 |-  ( ( ph /\ ( F : X -1-1-onto-> Y /\ G = `' F ) ) -> G : Y -1-1-onto-> X )
38 f1of
 |-  ( G : Y -1-1-onto-> X -> G : Y --> X )
39 37 38 syl
 |-  ( ( ph /\ ( F : X -1-1-onto-> Y /\ G = `' F ) ) -> G : Y --> X )
40 simprr
 |-  ( ( ph /\ ( F : X -1-1-onto-> Y /\ G = `' F ) ) -> G = `' F )
41 40 coeq1d
 |-  ( ( ph /\ ( F : X -1-1-onto-> Y /\ G = `' F ) ) -> ( G o. F ) = ( `' F o. F ) )
42 f1ococnv1
 |-  ( F : X -1-1-onto-> Y -> ( `' F o. F ) = ( _I |` X ) )
43 42 ad2antrl
 |-  ( ( ph /\ ( F : X -1-1-onto-> Y /\ G = `' F ) ) -> ( `' F o. F ) = ( _I |` X ) )
44 41 43 eqtrd
 |-  ( ( ph /\ ( F : X -1-1-onto-> Y /\ G = `' F ) ) -> ( G o. F ) = ( _I |` X ) )
45 40 coeq2d
 |-  ( ( ph /\ ( F : X -1-1-onto-> Y /\ G = `' F ) ) -> ( F o. G ) = ( F o. `' F ) )
46 f1ococnv2
 |-  ( F : X -1-1-onto-> Y -> ( F o. `' F ) = ( _I |` Y ) )
47 46 ad2antrl
 |-  ( ( ph /\ ( F : X -1-1-onto-> Y /\ G = `' F ) ) -> ( F o. `' F ) = ( _I |` Y ) )
48 45 47 eqtrd
 |-  ( ( ph /\ ( F : X -1-1-onto-> Y /\ G = `' F ) ) -> ( F o. G ) = ( _I |` Y ) )
49 44 48 jca
 |-  ( ( ph /\ ( F : X -1-1-onto-> Y /\ G = `' F ) ) -> ( ( G o. F ) = ( _I |` X ) /\ ( F o. G ) = ( _I |` Y ) ) )
50 32 39 49 jca31
 |-  ( ( ph /\ ( F : X -1-1-onto-> Y /\ G = `' F ) ) -> ( ( F : X --> Y /\ G : Y --> X ) /\ ( ( G o. F ) = ( _I |` X ) /\ ( F o. G ) = ( _I |` Y ) ) ) )
51 30 50 impbida
 |-  ( ph -> ( ( ( F : X --> Y /\ G : Y --> X ) /\ ( ( G o. F ) = ( _I |` X ) /\ ( F o. G ) = ( _I |` Y ) ) ) <-> ( F : X -1-1-onto-> Y /\ G = `' F ) ) )
52 13 24 51 3bitrd
 |-  ( ph -> ( F ( X N Y ) G <-> ( F : X -1-1-onto-> Y /\ G = `' F ) ) )