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=SetCatU
setcmon.u φUV
setcmon.x φXU
setcmon.y φYU
setciso.n I=IsoC
Assertion setciso φFXIYF:X1-1 ontoY

Proof

Step Hyp Ref Expression
1 setcmon.c C=SetCatU
2 setcmon.u φUV
3 setcmon.x φXU
4 setcmon.y φYU
5 setciso.n I=IsoC
6 eqid BaseC=BaseC
7 eqid InvC=InvC
8 1 setccat UVCCat
9 2 8 syl φCCat
10 1 2 setcbas φU=BaseC
11 3 10 eleqtrd φXBaseC
12 4 10 eleqtrd φYBaseC
13 6 7 9 11 12 5 isoval φXIY=domXInvCY
14 13 eleq2d φFXIYFdomXInvCY
15 6 7 9 11 12 invfun φFunXInvCY
16 funfvbrb FunXInvCYFdomXInvCYFXInvCYXInvCYF
17 15 16 syl φFdomXInvCYFXInvCYXInvCYF
18 1 2 3 4 7 setcinv φFXInvCYXInvCYFF:X1-1 ontoYXInvCYF=F-1
19 simpl F:X1-1 ontoYXInvCYF=F-1F:X1-1 ontoY
20 18 19 syl6bi φFXInvCYXInvCYFF:X1-1 ontoY
21 17 20 sylbid φFdomXInvCYF:X1-1 ontoY
22 eqid F-1=F-1
23 1 2 3 4 7 setcinv φFXInvCYF-1F:X1-1 ontoYF-1=F-1
24 funrel FunXInvCYRelXInvCY
25 15 24 syl φRelXInvCY
26 releldm RelXInvCYFXInvCYF-1FdomXInvCY
27 26 ex RelXInvCYFXInvCYF-1FdomXInvCY
28 25 27 syl φFXInvCYF-1FdomXInvCY
29 23 28 sylbird φF:X1-1 ontoYF-1=F-1FdomXInvCY
30 22 29 mpan2i φF:X1-1 ontoYFdomXInvCY
31 21 30 impbid φFdomXInvCYF:X1-1 ontoY
32 14 31 bitrd φFXIYF:X1-1 ontoY