Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  catciso Structured version   Unicode version

Theorem catciso 15292
 Description: A functor is an isomorphism of categories if and only if it is full and faithful, and is a bijection on the objects. (Contributed by Mario Carneiro, 29-Jan-2017.)
Hypotheses
Ref Expression
catciso.c CatCat
catciso.b
catciso.r
catciso.s
catciso.u
catciso.x
catciso.y
catciso.i
Assertion
Ref Expression
catciso Full Faith

Proof of Theorem catciso
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relfunc 15089 . . . . 5
2 catciso.b . . . . . . . . . . . . . 14
3 eqid 2467 . . . . . . . . . . . . . 14 Inv Inv
4 catciso.u . . . . . . . . . . . . . . 15
5 catciso.c . . . . . . . . . . . . . . . 16 CatCat
65catccat 15289 . . . . . . . . . . . . . . 15
74, 6syl 16 . . . . . . . . . . . . . 14
8 catciso.x . . . . . . . . . . . . . 14
9 catciso.y . . . . . . . . . . . . . 14
10 catciso.i . . . . . . . . . . . . . 14
112, 3, 7, 8, 9, 10isoval 15020 . . . . . . . . . . . . 13 Inv
1211eleq2d 2537 . . . . . . . . . . . 12 Inv
1312biimpa 484 . . . . . . . . . . 11 Inv
147adantr 465 . . . . . . . . . . . . 13
158adantr 465 . . . . . . . . . . . . 13
169adantr 465 . . . . . . . . . . . . 13
172, 3, 14, 15, 16invfun 15019 . . . . . . . . . . . 12 Inv
18 funfvbrb 5994 . . . . . . . . . . . 12 Inv Inv InvInv
1917, 18syl 16 . . . . . . . . . . 11 Inv InvInv
2013, 19mpbid 210 . . . . . . . . . 10 InvInv
21 eqid 2467 . . . . . . . . . . 11 Sect Sect
222, 3, 14, 15, 16, 21isinv 15015 . . . . . . . . . 10 InvInv SectInv InvSect
2320, 22mpbid 210 . . . . . . . . 9 SectInv InvSect
2423simpld 459 . . . . . . . 8 SectInv
25 eqid 2467 . . . . . . . . 9
26 eqid 2467 . . . . . . . . 9 comp comp
27 eqid 2467 . . . . . . . . 9
282, 25, 26, 27, 21, 14, 15, 16issect 15009 . . . . . . . 8 SectInv Inv Inv comp
2924, 28mpbid 210 . . . . . . 7 Inv Inv comp
3029simp1d 1008 . . . . . 6
315, 2, 4, 25, 8, 9catchom 15284 . . . . . . 7
3231adantr 465 . . . . . 6
3330, 32eleqtrd 2557 . . . . 5
34 1st2nd 6830 . . . . 5
351, 33, 34sylancr 663 . . . 4
36 1st2ndbr 6833 . . . . . . 7
371, 33, 36sylancr 663 . . . . . 6
38 catciso.r . . . . . . . . . 10
39 eqid 2467 . . . . . . . . . 10
40 eqid 2467 . . . . . . . . . 10
4137adantr 465 . . . . . . . . . 10
42 simprl 755 . . . . . . . . . 10
43 simprr 756 . . . . . . . . . 10
4438, 39, 40, 41, 42, 43funcf2 15095 . . . . . . . . 9
45 catciso.s . . . . . . . . . . 11
46 relfunc 15089 . . . . . . . . . . . . 13
4729simp2d 1009 . . . . . . . . . . . . . 14 Inv
485, 2, 4, 25, 9, 8catchom 15284 . . . . . . . . . . . . . . 15
4948adantr 465 . . . . . . . . . . . . . 14
5047, 49eleqtrd 2557 . . . . . . . . . . . . 13 Inv
51 1st2ndbr 6833 . . . . . . . . . . . . 13 Inv Inv Inv
5246, 50, 51sylancr 663 . . . . . . . . . . . 12 Inv Inv
5352adantr 465 . . . . . . . . . . 11 Inv Inv
5438, 45, 41funcf1 15093 . . . . . . . . . . . 12
5554, 42ffvelrnd 6022 . . . . . . . . . . 11
5654, 43ffvelrnd 6022 . . . . . . . . . . 11
5745, 40, 39, 53, 55, 56funcf2 15095 . . . . . . . . . 10 Inv Inv Inv
58 eqidd 2468 . . . . . . . . . . 11
5929simp3d 1010 . . . . . . . . . . . . . . . . 17 Inv comp
604adantr 465 . . . . . . . . . . . . . . . . . 18
615, 2, 60, 26, 15, 16, 15, 33, 50catcco 15286 . . . . . . . . . . . . . . . . 17 Inv comp Inv func
62 eqid 2467 . . . . . . . . . . . . . . . . . . 19 idfunc idfunc
635, 2, 27, 62, 4, 8catcid 15288 . . . . . . . . . . . . . . . . . 18 idfunc
6463adantr 465 . . . . . . . . . . . . . . . . 17 idfunc
6559, 61, 643eqtr3d 2516 . . . . . . . . . . . . . . . 16 Inv func idfunc
6665adantr 465 . . . . . . . . . . . . . . 15 Inv func idfunc
6766fveq2d 5870 . . . . . . . . . . . . . 14 Inv func idfunc
6867fveq1d 5868 . . . . . . . . . . . . 13 Inv func idfunc
6933adantr 465 . . . . . . . . . . . . . 14
7050adantr 465 . . . . . . . . . . . . . 14 Inv
7138, 69, 70, 42cofu1 15111 . . . . . . . . . . . . 13 Inv func Inv
725, 2, 4catcbas 15282 . . . . . . . . . . . . . . . . 17
73 inss2 3719 . . . . . . . . . . . . . . . . 17
7472, 73syl6eqss 3554 . . . . . . . . . . . . . . . 16
7574, 8sseldd 3505 . . . . . . . . . . . . . . 15
7675ad2antrr 725 . . . . . . . . . . . . . 14
7762, 38, 76, 42idfu1 15107 . . . . . . . . . . . . 13 idfunc
7868, 71, 773eqtr3d 2516 . . . . . . . . . . . 12 Inv
7967fveq1d 5868 . . . . . . . . . . . . 13 Inv func idfunc
8038, 69, 70, 43cofu1 15111 . . . . . . . . . . . . 13 Inv func Inv
8162, 38, 76, 43idfu1 15107 . . . . . . . . . . . . 13 idfunc
8279, 80, 813eqtr3d 2516 . . . . . . . . . . . 12 Inv
8378, 82oveq12d 6302 . . . . . . . . . . 11 Inv Inv
8458, 83feq23d 5726 . . . . . . . . . 10 Inv Inv Inv Inv
8557, 84mpbid 210 . . . . . . . . 9 Inv
8623simprd 463 . . . . . . . . . . . . . . . 16 InvSect
872, 25, 26, 27, 21, 14, 16, 15issect 15009 . . . . . . . . . . . . . . . 16 InvSect Inv compInv
8886, 87mpbid 210 . . . . . . . . . . . . . . 15 Inv compInv
8988simp3d 1010 . . . . . . . . . . . . . 14 compInv
905, 2, 60, 26, 16, 15, 16, 50, 33catcco 15286 . . . . . . . . . . . . . 14 compInv func Inv
91 eqid 2467 . . . . . . . . . . . . . . . 16 idfunc idfunc
925, 2, 27, 91, 4, 9catcid 15288 . . . . . . . . . . . . . . 15 idfunc
9392adantr 465 . . . . . . . . . . . . . 14 idfunc
9489, 90, 933eqtr3d 2516 . . . . . . . . . . . . 13 func Inv idfunc
9594adantr 465 . . . . . . . . . . . 12 func Inv idfunc
9695fveq2d 5870 . . . . . . . . . . 11 func Inv idfunc
9796oveqd 6301 . . . . . . . . . 10 func Inv idfunc
9845, 70, 69, 55, 56cofu2nd 15112 . . . . . . . . . . 11 func Inv InvInv Inv
9978, 82oveq12d 6302 . . . . . . . . . . . 12 InvInv
10099coeq1d 5164 . . . . . . . . . . 11 InvInv Inv Inv
10198, 100eqtrd 2508 . . . . . . . . . 10 func Inv Inv
10274ad2antrr 725 . . . . . . . . . . . 12
1039ad2antrr 725 . . . . . . . . . . . 12
104102, 103sseldd 3505 . . . . . . . . . . 11
10591, 45, 104, 40, 55, 56idfu2nd 15104 . . . . . . . . . 10 idfunc
10697, 101, 1053eqtr3d 2516 . . . . . . . . 9 Inv
10766fveq2d 5870 . . . . . . . . . . 11 Inv func idfunc
108107oveqd 6301 . . . . . . . . . 10 Inv func idfunc
10938, 69, 70, 42, 43cofu2nd 15112 . . . . . . . . . 10 Inv func Inv
11062, 38, 76, 39, 42, 43idfu2nd 15104 . . . . . . . . . 10 idfunc
111108, 109, 1103eqtr3d 2516 . . . . . . . . 9 Inv
112 fcof1o 6187 . . . . . . . . 9 Inv Inv Inv Inv
11344, 85, 106, 111, 112syl22anc 1229 . . . . . . . 8 Inv
114113simpld 459 . . . . . . 7
115114ralrimivva 2885 . . . . . 6
11638, 39, 40isffth2 15143 . . . . . 6 Full Faith
11737, 115, 116sylanbrc 664 . . . . 5 Full Faith
118 df-br 4448 . . . . 5 Full Faith Full Faith
119117, 118sylib 196 . . . 4 Full Faith
12035, 119eqeltrd 2555 . . 3 Full Faith
12138, 45, 37funcf1 15093 . . . . 5
12245, 38, 52funcf1 15093 . . . . 5 Inv
12394fveq2d 5870 . . . . . 6 func Inv idfunc
12445, 50, 33cofu1st 15110 . . . . . 6 func Inv Inv
12574, 9sseldd 3505 . . . . . . . 8
126125adantr 465 . . . . . . 7
12791, 45, 126idfu1st 15106 . . . . . 6 idfunc
128123, 124, 1273eqtr3d 2516 . . . . 5 Inv
12965fveq2d 5870 . . . . . 6 Inv func idfunc
13038, 33, 50cofu1st 15110 . . . . . 6 Inv func Inv
13175adantr 465 . . . . . . 7
13262, 38, 131idfu1st 15106 . . . . . 6 idfunc
133129, 130, 1323eqtr3d 2516 . . . . 5 Inv
134 fcof1o 6187 . . . . 5 Inv Inv Inv Inv
135121, 122, 128, 133, 134syl22anc 1229 . . . 4 Inv
136135simpld 459 . . 3
137120, 136jca 532 . 2 Full Faith
1387adantr 465 . . 3 Full Faith
1398adantr 465 . . 3 Full Faith
1409adantr 465 . . 3 Full Faith
141 inss1 3718 . . . . . . 7 Full Faith Full
142 fullfunc 15133 . . . . . . 7 Full
143141, 142sstri 3513 . . . . . 6 Full Faith
144 simprl 755 . . . . . 6 Full Faith Full Faith
145143, 144sseldi 3502 . . . . 5 Full Faith
1461, 145, 34sylancr 663 . . . 4 Full Faith
1474adantr 465 . . . . 5 Full Faith
148 eqid 2467 . . . . 5
149146, 144eqeltrrd 2556 . . . . . 6 Full Faith Full Faith
150149, 118sylibr 212 . . . . 5 Full Faith Full Faith
151 simprr 756 . . . . 5 Full Faith
1525, 2, 38, 45, 147, 139, 140, 3, 148, 150, 151catcisolem 15291 . . . 4 Full Faith Inv
153146, 152eqbrtrd 4467 . . 3 Full Faith Inv
1542, 3, 138, 139, 140, 10, 153inviso1 15021 . 2 Full Faith
155137, 154impbida 830 1 Full Faith
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3a 973   wceq 1379   wcel 1767  wral 2814   cin 3475   wss 3476  cop 4033   class class class wbr 4447   cid 4790  ccnv 4998   cdm 4999   cres 5001   ccom 5003   wrel 5004   wfun 5582  wf 5584  wf1o 5587  cfv 5588  (class class class)co 6284   cmpt2 6286  c1st 6782  c2nd 6783  cbs 14490   chom 14566  compcco 14567  ccat 14919  ccid 14920  Sectcsect 15000  Invcinv 15001   ciso 15002   cfunc 15081  idfunccidfu 15082   func ccofu 15083   Full cful 15129   Faith cfth 15130  CatCatccatc 15279 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-om 6685  df-1st 6784  df-2nd 6785  df-recs 7042  df-rdg 7076  df-1o 7130  df-oadd 7134  df-er 7311  df-map 7422  df-ixp 7470  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-nn 10537  df-2 10594  df-3 10595  df-4 10596  df-5 10597  df-6 10598  df-7 10599  df-8 10600  df-9 10601  df-10 10602  df-n0 10796  df-z 10865  df-dec 10977  df-uz 11083  df-fz 11673  df-struct 14492  df-ndx 14493  df-slot 14494  df-base 14495  df-hom 14579  df-cco 14580  df-cat 14923  df-cid 14924  df-sect 15003  df-inv 15004  df-iso 15005  df-func 15085  df-idfu 15086  df-cofu 15087  df-full 15131  df-fth 15132  df-catc 15280 This theorem is referenced by:  yoniso  15412
 Copyright terms: Public domain W3C validator