Theorem relfunc 17820

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

Syntax hints:   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3052  [wsbc 3729  ⟨cop 4574   × cxp 5622  Rel wrel 5629  ⟶wf 6488  ‘cfv 6492  (class class class)co 7360  1^st c1st 7933  2^nd c2nd 7934   ↑_m cmap 8766  Xcixp 8838  Basecbs 17170  Hom chom 17222  compcco 17223  Catccat 17621  Idccid 17622   Func cfunc 17812

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  df-func 17816

This theorem is referenced by:  cofuval  17840  cofu1  17842  cofu2  17844  cofuval2  17845  cofucl  17846  cofuass  17847  cofulid  17848  cofurid  17849  funcres  17854  funcres2  17856  wunfunc  17859  funcpropd  17860  relfull  17868  relfth  17869  isfull  17870  isfth  17874  idffth  17893  cofull  17894  cofth  17895  ressffth  17898  isnat  17908  isnat2  17909  nat1st2nd  17912  fuccocl  17925  fucidcl  17926  fuclid  17927  fucrid  17928  fucass  17929  fucsect  17933  fucinv  17934  invfuc  17935  fuciso  17936  natpropd  17937  fucpropd  17938  catciso  18069  prfval  18156  prfcl  18160  prf1st  18161  prf2nd  18162  1st2ndprf  18163  evlfcllem  18178  evlfcl  18179  curf1cl  18185  curf2cl  18188  curfcl  18189  uncf1  18193  uncf2  18194  curfuncf  18195  uncfcurf  18196  diag1cl  18199  diag2cl  18203  curf2ndf  18204  yon1cl  18220  oyon1cl  18228  yonedalem1  18229  yonedalem21  18230  yonedalem3a  18231  yonedalem4c  18234  yonedalem22  18235  yonedalem3b  18236  yonedalem3  18237  yonedainv  18238  yonffthlem  18239  yoniso  18242  func1st2nd  49563  func1st  49564  func2nd  49565  0funcg  49572  0funcALT  49575  cofu1st2nd  49579  idfurcl  49585  oppfval  49623  oppfval2  49624  oppfoppc2  49629  funcoppc4  49631  funcoppc5  49632  oppff1  49635  oppff1o  49636  imassc  49640  imaid  49641  imaf1co  49642  imasubc3  49643  idfth  49645  upfval3  49665  up1st2nd  49672  up1st2ndr  49673  uptrlem2  49698  uptra  49702  uobeqw  49706  uobeq  49707  uptr2a  49709  natoppfb  49718  diag1  49791  fuco112  49816  fuco111  49817  fuco21  49823  fuco11bALT  49825  fuco22nat  49833  fucof21  49834  fucoid  49835  fucoid2  49836  fuco22a  49837  fucocolem4  49843  precofvalALT  49855  precofval3  49858  reldmprcof1  49868  prcoftposcurfuco  49870  prcoftposcurfucoa  49871  prcofdiag1  49880  prcofdiag  49881  oppfdiag1  49901  oppfdiag  49903  functhincfun  49936  functermc2  49996  eufunclem  50008  termcfuncval  50019  diagffth  50025  reldmlmd2  50140  reldmcmd2  50141  lmddu  50154  cmddu  50155  lmdran  50158  cmdlan  50159