Theorem relfunc 17775

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

Syntax hints:   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  ∀wral 3047  [wsbc 3736  ⟨cop 4581   × cxp 5617  Rel wrel 5624  ⟶wf 6483  ‘cfv 6487  (class class class)co 7352  1^st c1st 7925  2^nd c2nd 7926   ↑_m cmap 8756  Xcixp 8827  Basecbs 17126  Hom chom 17178  compcco 17179  Catccat 17576  Idccid 17577   Func cfunc 17767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6443  df-fun 6489  df-fv 6495  df-ov 7355  df-oprab 7356  df-mpo 7357  df-1st 7927  df-2nd 7928  df-func 17771

This theorem is referenced by:  cofuval  17795  cofu1  17797  cofu2  17799  cofuval2  17800  cofucl  17801  cofuass  17802  cofulid  17803  cofurid  17804  funcres  17809  funcres2  17811  wunfunc  17814  funcpropd  17815  relfull  17823  relfth  17824  isfull  17825  isfth  17829  idffth  17848  cofull  17849  cofth  17850  ressffth  17853  isnat  17863  isnat2  17864  nat1st2nd  17867  fuccocl  17880  fucidcl  17881  fuclid  17882  fucrid  17883  fucass  17884  fucsect  17888  fucinv  17889  invfuc  17890  fuciso  17891  natpropd  17892  fucpropd  17893  catciso  18024  prfval  18111  prfcl  18115  prf1st  18116  prf2nd  18117  1st2ndprf  18118  evlfcllem  18133  evlfcl  18134  curf1cl  18140  curf2cl  18143  curfcl  18144  uncf1  18148  uncf2  18149  curfuncf  18150  uncfcurf  18151  diag1cl  18154  diag2cl  18158  curf2ndf  18159  yon1cl  18175  oyon1cl  18183  yonedalem1  18184  yonedalem21  18185  yonedalem3a  18186  yonedalem4c  18189  yonedalem22  18190  yonedalem3b  18191  yonedalem3  18192  yonedainv  18193  yonffthlem  18194  yoniso  18197  func1st2nd  49182  func1st  49183  func2nd  49184  0funcg  49191  0funcALT  49194  cofu1st2nd  49198  idfurcl  49204  oppfval  49242  oppfval2  49243  oppfoppc2  49248  funcoppc4  49250  funcoppc5  49251  oppff1  49254  oppff1o  49255  imassc  49259  imaid  49260  imaf1co  49261  imasubc3  49262  idfth  49264  upfval3  49284  up1st2nd  49291  up1st2ndr  49292  uptrlem2  49317  uptra  49321  uobeqw  49325  uobeq  49326  uptr2a  49328  natoppfb  49337  diag1  49410  fuco112  49435  fuco111  49436  fuco21  49442  fuco11bALT  49444  fuco22nat  49452  fucof21  49453  fucoid  49454  fucoid2  49455  fuco22a  49456  fucocolem4  49462  precofvalALT  49474  precofval3  49477  reldmprcof1  49487  prcoftposcurfuco  49489  prcoftposcurfucoa  49490  prcofdiag1  49499  prcofdiag  49500  oppfdiag1  49520  oppfdiag  49522  functhincfun  49555  functermc2  49615  eufunclem  49627  termcfuncval  49638  diagffth  49644  reldmlmd2  49759  reldmcmd2  49760  lmddu  49773  cmddu  49774  lmdran  49777  cmdlan  49778