Theorem relfunc 17798

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

Syntax hints:   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3052  [wsbc 3742  ⟨cop 4588   × cxp 5630  Rel wrel 5637  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368  1^st c1st 7941  2^nd c2nd 7942   ↑_m cmap 8775  Xcixp 8847  Basecbs 17148  Hom chom 17200  compcco 17201  Catccat 17599  Idccid 17600   Func cfunc 17790

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 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

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 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-1st 7943  df-2nd 7944  df-func 17794

This theorem is referenced by:  cofuval  17818  cofu1  17820  cofu2  17822  cofuval2  17823  cofucl  17824  cofuass  17825  cofulid  17826  cofurid  17827  funcres  17832  funcres2  17834  wunfunc  17837  funcpropd  17838  relfull  17846  relfth  17847  isfull  17848  isfth  17852  idffth  17871  cofull  17872  cofth  17873  ressffth  17876  isnat  17886  isnat2  17887  nat1st2nd  17890  fuccocl  17903  fucidcl  17904  fuclid  17905  fucrid  17906  fucass  17907  fucsect  17911  fucinv  17912  invfuc  17913  fuciso  17914  natpropd  17915  fucpropd  17916  catciso  18047  prfval  18134  prfcl  18138  prf1st  18139  prf2nd  18140  1st2ndprf  18141  evlfcllem  18156  evlfcl  18157  curf1cl  18163  curf2cl  18166  curfcl  18167  uncf1  18171  uncf2  18172  curfuncf  18173  uncfcurf  18174  diag1cl  18177  diag2cl  18181  curf2ndf  18182  yon1cl  18198  oyon1cl  18206  yonedalem1  18207  yonedalem21  18208  yonedalem3a  18209  yonedalem4c  18212  yonedalem22  18213  yonedalem3b  18214  yonedalem3  18215  yonedainv  18216  yonffthlem  18217  yoniso  18220  func1st2nd  49429  func1st  49430  func2nd  49431  0funcg  49438  0funcALT  49441  cofu1st2nd  49445  idfurcl  49451  oppfval  49489  oppfval2  49490  oppfoppc2  49495  funcoppc4  49497  funcoppc5  49498  oppff1  49501  oppff1o  49502  imassc  49506  imaid  49507  imaf1co  49508  imasubc3  49509  idfth  49511  upfval3  49531  up1st2nd  49538  up1st2ndr  49539  uptrlem2  49564  uptra  49568  uobeqw  49572  uobeq  49573  uptr2a  49575  natoppfb  49584  diag1  49657  fuco112  49682  fuco111  49683  fuco21  49689  fuco11bALT  49691  fuco22nat  49699  fucof21  49700  fucoid  49701  fucoid2  49702  fuco22a  49703  fucocolem4  49709  precofvalALT  49721  precofval3  49724  reldmprcof1  49734  prcoftposcurfuco  49736  prcoftposcurfucoa  49737  prcofdiag1  49746  prcofdiag  49747  oppfdiag1  49767  oppfdiag  49769  functhincfun  49802  functermc2  49862  eufunclem  49874  termcfuncval  49885  diagffth  49891  reldmlmd2  50006  reldmcmd2  50007  lmddu  50020  cmddu  50021  lmdran  50024  cmdlan  50025