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