Theorem relfunc 17827

Description: The set of functors is a relation. (Contributed by Mario Carneiro, 2-Jan-2017.)

Assertion

Ref	Expression
relfunc	⊢ Rel (𝐷 Func 𝐸)

Proof of Theorem relfunc

Dummy variables 𝑓 𝑏 𝑔 𝑚 𝑛 𝑡 𝑢 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-func 17823	. 2 ⊢ Func = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))})
2	1	relmpoopab 8040	1 ⊢ Rel (𝐷 Func 𝐸)

Syntax hints:   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ∀wral 3054  [wsbc 3730  ⟨cop 4568   × cxp 5623  Rel wrel 5630  ⟶wf 6488  ‘cfv 6492  (class class class)co 7363  1^st c1st 7936  2^nd c2nd 7937   ↑_m cmap 8770  Xcixp 8842  Basecbs 17177  Hom chom 17229  compcco 17230  Catccat 17628  Idccid 17629   Func cfunc 17819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-1st 7938  df-2nd 7939  df-func 17823

This theorem is referenced by:  cofuval  17847  cofu1  17849  cofu2  17851  cofuval2  17852  cofucl  17853  cofuass  17854  cofulid  17855  cofurid  17856  funcres  17861  funcres2  17863  wunfunc  17866  funcpropd  17867  relfull  17875  relfth  17876  isfull  17877  isfth  17881  idffth  17900  cofull  17901  cofth  17902  ressffth  17905  isnat  17915  isnat2  17916  nat1st2nd  17919  fuccocl  17932  fucidcl  17933  fuclid  17934  fucrid  17935  fucass  17936  fucsect  17940  fucinv  17941  invfuc  17942  fuciso  17943  natpropd  17944  fucpropd  17945  catciso  18076  prfval  18163  prfcl  18167  prf1st  18168  prf2nd  18169  1st2ndprf  18170  evlfcllem  18185  evlfcl  18186  curf1cl  18192  curf2cl  18195  curfcl  18196  uncf1  18200  uncf2  18201  curfuncf  18202  uncfcurf  18203  diag1cl  18206  diag2cl  18210  curf2ndf  18211  yon1cl  18227  oyon1cl  18235  yonedalem1  18236  yonedalem21  18237  yonedalem3a  18238  yonedalem4c  18241  yonedalem22  18242  yonedalem3b  18243  yonedalem3  18244  yonedainv  18245  yonffthlem  18246  yoniso  18249  func1st2nd  49573  func1st  49574  func2nd  49575  0funcg  49582  0funcALT  49585  cofu1st2nd  49589  idfurcl  49595  oppfval  49633  oppfval2  49634  oppfoppc2  49639  funcoppc4  49641  funcoppc5  49642  oppff1  49645  oppff1o  49646  imassc  49650  imaid  49651  imaf1co  49652  imasubc3  49653  idfth  49655  upfval3  49675  up1st2nd  49682  up1st2ndr  49683  uptrlem2  49708  uptra  49712  uobeqw  49716  uobeq  49717  uptr2a  49719  natoppfb  49728  diag1  49801  fuco112  49826  fuco111  49827  fuco21  49833  fuco11bALT  49835  fuco22nat  49843  fucof21  49844  fucoid  49845  fucoid2  49846  fuco22a  49847  fucocolem4  49853  precofvalALT  49865  precofval3  49868  reldmprcof1  49878  prcoftposcurfuco  49880  prcoftposcurfucoa  49881  prcofdiag1  49890  prcofdiag  49891  oppfdiag1  49911  oppfdiag  49913  functhincfun  49946  functermc2  50006  eufunclem  50018  termcfuncval  50029  diagffth  50035  reldmlmd2  50150  reldmcmd2  50151  lmddu  50164  cmddu  50165  lmdran  50168  cmdlan  50169