Metamath Proof Explorer

Theorem setciso

Description: An isomorphism in the category of sets is a bijection. (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 )
setciso.n 
|- I = ( Iso ` C )
Assertion setciso 
|- ( ph -> ( F e. ( X I Y ) <-> F : X -1-1-onto-> Y ) )

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 setciso.n 
 |-  I = ( Iso ` C )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 eqid 
 |-  ( Inv ` C ) = ( Inv ` C )
8 1 setccat 
 |-  ( U e. V -> C e. Cat )
9 2 8 syl 
 |-  ( ph -> C e. Cat )
10 1 2 setcbas 
 |-  ( ph -> U = ( Base ` C ) )
11 3 10 eleqtrd 
 |-  ( ph -> X e. ( Base ` C ) )
12 4 10 eleqtrd 
 |-  ( ph -> Y e. ( Base ` C ) )
13 6 7 9 11 12 5 isoval 
 |-  ( ph -> ( X I Y ) = dom ( X ( Inv ` C ) Y ) )
14 13 eleq2d 
 |-  ( ph -> ( F e. ( X I Y ) <-> F e. dom ( X ( Inv ` C ) Y ) ) )
15 6 7 9 11 12 invfun 
 |-  ( ph -> Fun ( X ( Inv ` C ) Y ) )
16 funfvbrb 
 |-  ( Fun ( X ( Inv ` C ) Y ) -> ( F e. dom ( X ( Inv ` C ) Y ) <-> F ( X ( Inv ` C ) Y ) ( ( X ( Inv ` C ) Y ) ` F ) ) )
17 15 16 syl 
 |-  ( ph -> ( F e. dom ( X ( Inv ` C ) Y ) <-> F ( X ( Inv ` C ) Y ) ( ( X ( Inv ` C ) Y ) ` F ) ) )
18 1 2 3 4 7 setcinv 
 |-  ( ph -> ( F ( X ( Inv ` C ) Y ) ( ( X ( Inv ` C ) Y ) ` F ) <-> ( F : X -1-1-onto-> Y /\ ( ( X ( Inv ` C ) Y ) ` F ) = `' F ) ) )
19 simpl 
 |-  ( ( F : X -1-1-onto-> Y /\ ( ( X ( Inv ` C ) Y ) ` F ) = `' F ) -> F : X -1-1-onto-> Y )
20 18 19 biimtrdi 
 |-  ( ph -> ( F ( X ( Inv ` C ) Y ) ( ( X ( Inv ` C ) Y ) ` F ) -> F : X -1-1-onto-> Y ) )
21 17 20 sylbid 
 |-  ( ph -> ( F e. dom ( X ( Inv ` C ) Y ) -> F : X -1-1-onto-> Y ) )
22 eqid 
 |-  `' F = `' F
23 1 2 3 4 7 setcinv 
 |-  ( ph -> ( F ( X ( Inv ` C ) Y ) `' F <-> ( F : X -1-1-onto-> Y /\ `' F = `' F ) ) )
24 funrel 
 |-  ( Fun ( X ( Inv ` C ) Y ) -> Rel ( X ( Inv ` C ) Y ) )
25 15 24 syl 
 |-  ( ph -> Rel ( X ( Inv ` C ) Y ) )
26 releldm 
 |-  ( ( Rel ( X ( Inv ` C ) Y ) /\ F ( X ( Inv ` C ) Y ) `' F ) -> F e. dom ( X ( Inv ` C ) Y ) )
27 26 ex 
 |-  ( Rel ( X ( Inv ` C ) Y ) -> ( F ( X ( Inv ` C ) Y ) `' F -> F e. dom ( X ( Inv ` C ) Y ) ) )
28 25 27 syl 
 |-  ( ph -> ( F ( X ( Inv ` C ) Y ) `' F -> F e. dom ( X ( Inv ` C ) Y ) ) )
29 23 28 sylbird 
 |-  ( ph -> ( ( F : X -1-1-onto-> Y /\ `' F = `' F ) -> F e. dom ( X ( Inv ` C ) Y ) ) )
30 22 29 mpan2i 
 |-  ( ph -> ( F : X -1-1-onto-> Y -> F e. dom ( X ( Inv ` C ) Y ) ) )
31 21 30 impbid 
 |-  ( ph -> ( F e. dom ( X ( Inv ` C ) Y ) <-> F : X -1-1-onto-> Y ) )
32 14 31 bitrd 
 |-  ( ph -> ( F e. ( X I Y ) <-> F : X -1-1-onto-> Y ) )