Theorem relfunc 17878

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

Syntax hints:   ∧ wa 399   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141  ∀wral 3075  [wsbc 3744  ⟨cop 4587   × cxp 5643  Rel wrel 5650  ⟶wf 6513  ‘cfv 6517  (class class class)co 7392  1^st c1st 7964  2^nd c2nd 7965   ↑_m cmap 8803  Xcixp 8875  Basecbs 17228  Hom chom 17280  compcco 17281  Catccat 17679  Idccid 17680   Func cfunc 17870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fv 6525  df-ov 7395  df-oprab 7396  df-mpo 7397  df-1st 7966  df-2nd 7967  df-func 17874

This theorem is referenced by:  cofuval  17898  cofu1  17900  cofu2  17902  cofuval2  17903  cofucl  17904  cofuass  17905  cofulid  17906  cofurid  17907  funcres  17912  funcres2  17914  wunfunc  17917  funcpropd  17918  relfull  17926  relfth  17927  isfull  17928  isfth  17932  idffth  17951  cofull  17952  cofth  17953  ressffth  17956  isnat  17966  isnat2  17967  nat1st2nd  17970  fuccocl  17983  fucidcl  17984  fuclid  17985  fucrid  17986  fucass  17987  fucsect  17991  fucinv  17992  invfuc  17993  fuciso  17994  natpropd  17995  fucpropd  17996  catciso  18127  prfval  18214  prfcl  18218  prf1st  18219  prf2nd  18220  1st2ndprf  18221  evlfcllem  18236  evlfcl  18237  curf1cl  18243  curf2cl  18246  curfcl  18247  uncf1  18251  uncf2  18252  curfuncf  18253  uncfcurf  18254  diag1cl  18257  diag2cl  18261  curf2ndf  18262  yon1cl  18278  oyon1cl  18286  yonedalem1  18287  yonedalem21  18288  yonedalem3a  18289  yonedalem4c  18292  yonedalem22  18293  yonedalem3b  18294  yonedalem3  18295  yonedainv  18296  yonffthlem  18297  yoniso  18300  func1st2nd  49661  func1st  49662  func2nd  49663  0funcg  49670  0funcALT  49673  cofu1st2nd  49677  idfurcl  49683  oppfval  49721  oppfval2  49722  oppfoppc2  49727  funcoppc4  49729  funcoppc5  49730  oppff1  49733  oppff1o  49734  imassc  49738  imaid  49739  imaf1co  49740  imasubc3  49741  idfth  49743  upfval3  49763  up1st2nd  49770  up1st2ndr  49771  uptrlem2  49796  uptra  49800  uobeqw  49804  uobeq  49805  uptr2a  49807  natoppfb  49816  diag1  49889  fuco112  49914  fuco111  49915  fuco21  49921  fuco11bALT  49923  fuco22nat  49931  fucof21  49932  fucoid  49933  fucoid2  49934  fuco22a  49935  fucocolem4  49941  precofvalALT  49953  precofval3  49956  reldmprcof1  49966  prcoftposcurfuco  49968  prcoftposcurfucoa  49969  prcofdiag1  49978  prcofdiag  49979  oppfdiag1  49999  oppfdiag  50001  functhincfun  50034  functermc2  50094  eufunclem  50106  termcfuncval  50117  diagffth  50123  reldmlmd2  50238  reldmcmd2  50239  lmddu  50252  cmddu  50253  lmdran  50256  cmdlan  50257