Theorem relfunc 18042

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

This proof depends on syntax axioms:   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  ∀wral 3076  [wsbc 3738  ⟨cop 4834   × cxp 5648  Rel wrel 5655  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420  1^st c1st 7999  2^nd c2nd 8000   ↑_m cmap 8850  Xcixp 8928  Basecbs 17392  Hom chom 17444  compcco 17445  Catccat 17843  Idccid 17844   Func cfunc 18034

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-dm 5660  df-rn 5661  df-iota 6494  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-func 18038

This theorem is used by:  cofuval  18062  cofu1  18064  cofu2  18066  cofuval2  18067  cofucl  18068  cofuass  18069  cofulid  18070  cofurid  18071  funcres  18076  funcres2  18078  wunfunc  18081  funcpropd  18082  relfull  18090  relfth  18091  isfull  18092  isfth  18096  idffth  18115  cofull  18116  cofth  18117  ressffth  18120  isnat  18130  isnat2  18131  nat1st2nd  18134  fuccocl  18147  fucidcl  18148  fuclid  18149  fucrid  18150  fucass  18151  fucsect  18155  fucinv  18156  invfuc  18157  fuciso  18158  natpropd  18159  fucpropd  18160  catciso  18291  prfval  18378  prfcl  18382  prf1st  18383  prf2nd  18384  1st2ndprf  18385  evlfcllem  18400  evlfcl  18401  curf1cl  18407  curf2cl  18410  curfcl  18411  uncf1  18415  uncf2  18416  curfuncf  18417  uncfcurf  18418  diag1cl  18421  diag2cl  18425  curf2ndf  18426  yon1cl  18442  oyon1cl  18450  yonedalem1  18451  yonedalem21  18452  yonedalem3a  18453  yonedalem4c  18456  yonedalem22  18457  yonedalem3b  18458  yonedalem3  18459  yonedainv  18460  yonffthlem  18461  yoniso  18464  func1st2nd  50283  func1st  50284  func2nd  50285  0funcg  50293  0funcALT  50296  cofu1st2nd  50300  idfurcl  50307  oppfval  50345  oppfval2  50346  oppfoppc2  50351  funcoppc4  50353  funcoppc5  50354  oppff1  50357  oppff1o  50358  imassc  50362  imaid  50363  imaf1co  50364  imasubc3  50365  idfth  50367  upfval3  50387  up1st2nd  50394  up1st2ndr  50395  uptrlem2  50420  uptra  50424  uobeqw  50428  uobeq  50429  uptr2a  50431  natoppfb  50446  diag1  50519  fuco112  50544  fuco111  50545  fuco21  50551  fuco11bALT  50553  fuco22nat  50561  fucof21  50562  fucoid  50563  fucoid2  50564  fuco22a  50565  fucocolem4  50571  precofvalALT  50596  precofval3  50599  reldmprcof1  50609  prcoftposcurfuco  50611  prcoftposcurfucoa  50612  prcofdiag1  50621  prcofdiag  50622  oppfdiag1  50642  oppfdiag  50644  functhincfun  50677  functermc2  50737  eufunclem  50749  termcfuncval  50760  diagffth  50769  reldmlmd2  50929  reldmcmd2  50930  lmddu  50943  cmddu  50944  lmdran  50947  cmdlan  50948