Theorem relfunc 17831

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 17827	. 2 ⊢ Func = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))})
2	1	relmpoopab 8076	1 ⊢ Rel (𝐷 Func 𝐸)

Syntax hints:   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3045  [wsbc 3756  ⟨cop 4598   × cxp 5639  Rel wrel 5646  ⟶wf 6510  ‘cfv 6514  (class class class)co 7390  1^st c1st 7969  2^nd c2nd 7970   ↑_m cmap 8802  Xcixp 8873  Basecbs 17186  Hom chom 17238  compcco 17239  Catccat 17632  Idccid 17633   Func cfunc 17823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-1st 7971  df-2nd 7972  df-func 17827

This theorem is referenced by:  cofuval  17851  cofu1  17853  cofu2  17855  cofuval2  17856  cofucl  17857  cofuass  17858  cofulid  17859  cofurid  17860  funcres  17865  funcres2  17867  wunfunc  17870  funcpropd  17871  relfull  17879  relfth  17880  isfull  17881  isfth  17885  idffth  17904  cofull  17905  cofth  17906  ressffth  17909  isnat  17919  isnat2  17920  nat1st2nd  17923  fuccocl  17936  fucidcl  17937  fuclid  17938  fucrid  17939  fucass  17940  fucsect  17944  fucinv  17945  invfuc  17946  fuciso  17947  natpropd  17948  fucpropd  17949  catciso  18080  prfval  18167  prfcl  18171  prf1st  18172  prf2nd  18173  1st2ndprf  18174  evlfcllem  18189  evlfcl  18190  curf1cl  18196  curf2cl  18199  curfcl  18200  uncf1  18204  uncf2  18205  curfuncf  18206  uncfcurf  18207  diag1cl  18210  diag2cl  18214  curf2ndf  18215  yon1cl  18231  oyon1cl  18239  yonedalem1  18240  yonedalem21  18241  yonedalem3a  18242  yonedalem4c  18245  yonedalem22  18246  yonedalem3b  18247  yonedalem3  18248  yonedainv  18249  yonffthlem  18250  yoniso  18253  func1st2nd  49069  func1st  49070  func2nd  49071  0funcg  49078  0funcALT  49081  cofu1st2nd  49085  idfurcl  49091  oppfval  49129  oppfval2  49130  oppfoppc2  49135  funcoppc4  49137  funcoppc5  49138  oppff1  49141  oppff1o  49142  imassc  49146  imaid  49147  imaf1co  49148  imasubc3  49149  idfth  49151  upfval3  49171  up1st2nd  49178  up1st2ndr  49179  uptrlem2  49204  uptra  49208  uobeqw  49212  uobeq  49213  uptr2a  49215  natoppfb  49224  diag1  49297  fuco112  49322  fuco111  49323  fuco21  49329  fuco11bALT  49331  fuco22nat  49339  fucof21  49340  fucoid  49341  fucoid2  49342  fuco22a  49343  fucocolem4  49349  precofvalALT  49361  precofval3  49364  reldmprcof1  49374  prcoftposcurfuco  49376  prcoftposcurfucoa  49377  prcofdiag1  49386  prcofdiag  49387  oppfdiag1  49407  oppfdiag  49409  functhincfun  49442  functermc2  49502  eufunclem  49514  termcfuncval  49525  diagffth  49531  reldmlmd2  49646  reldmcmd2  49647  lmddu  49660  cmddu  49661  lmdran  49664  cmdlan  49665