Theorem relfunc 17909

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

Syntax hints:   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  ∀wral 3079  [wsbc 3747  ⟨cop 4591   × cxp 5650  Rel wrel 5657  ⟶wf 6521  ‘cfv 6525  (class class class)co 7400  1^st c1st 7972  2^nd c2nd 7973   ↑_m cmap 8812  Xcixp 8883  Basecbs 17259  Hom chom 17311  compcco 17312  Catccat 17710  Idccid 17711   Func cfunc 17901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-1st 7974  df-2nd 7975  df-func 17905

This theorem is referenced by:  cofuval  17929  cofu1  17931  cofu2  17933  cofuval2  17934  cofucl  17935  cofuass  17936  cofulid  17937  cofurid  17938  funcres  17943  funcres2  17945  wunfunc  17948  funcpropd  17949  relfull  17957  relfth  17958  isfull  17959  isfth  17963  idffth  17982  cofull  17983  cofth  17984  ressffth  17987  isnat  17997  isnat2  17998  nat1st2nd  18001  fuccocl  18014  fucidcl  18015  fuclid  18016  fucrid  18017  fucass  18018  fucsect  18022  fucinv  18023  invfuc  18024  fuciso  18025  natpropd  18026  fucpropd  18027  catciso  18158  prfval  18245  prfcl  18249  prf1st  18250  prf2nd  18251  1st2ndprf  18252  evlfcllem  18267  evlfcl  18268  curf1cl  18274  curf2cl  18277  curfcl  18278  uncf1  18282  uncf2  18283  curfuncf  18284  uncfcurf  18285  diag1cl  18288  diag2cl  18292  curf2ndf  18293  yon1cl  18309  oyon1cl  18317  yonedalem1  18318  yonedalem21  18319  yonedalem3a  18320  yonedalem4c  18323  yonedalem22  18324  yonedalem3b  18325  yonedalem3  18326  yonedainv  18327  yonffthlem  18328  yoniso  18331  func1st2nd  49705  func1st  49706  func2nd  49707  0funcg  49714  0funcALT  49717  cofu1st2nd  49721  idfurcl  49727  oppfval  49765  oppfval2  49766  oppfoppc2  49771  funcoppc4  49773  funcoppc5  49774  oppff1  49777  oppff1o  49778  imassc  49782  imaid  49783  imaf1co  49784  imasubc3  49785  idfth  49787  upfval3  49807  up1st2nd  49814  up1st2ndr  49815  uptrlem2  49840  uptra  49844  uobeqw  49848  uobeq  49849  uptr2a  49851  natoppfb  49860  diag1  49933  fuco112  49958  fuco111  49959  fuco21  49965  fuco11bALT  49967  fuco22nat  49975  fucof21  49976  fucoid  49977  fucoid2  49978  fuco22a  49979  fucocolem4  49985  precofvalALT  49997  precofval3  50000  reldmprcof1  50010  prcoftposcurfuco  50012  prcoftposcurfucoa  50013  prcofdiag1  50022  prcofdiag  50023  oppfdiag1  50043  oppfdiag  50045  functhincfun  50078  functermc2  50138  eufunclem  50150  termcfuncval  50161  diagffth  50167  reldmlmd2  50282  reldmcmd2  50283  lmddu  50296  cmddu  50297  lmdran  50300  cmdlan  50301