Theorem relfunc 17771

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 17767	. 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 2113  ∀wral 3048  [wsbc 3737  ⟨cop 4581   × cxp 5617  Rel wrel 5624  ⟶wf 6482  ‘cfv 6486  (class class class)co 7352  1^st c1st 7925  2^nd c2nd 7926   ↑_m cmap 8756  Xcixp 8827  Basecbs 17122  Hom chom 17174  compcco 17175  Catccat 17572  Idccid 17573   Func cfunc 17763

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  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 6442  df-fun 6488  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357  df-1st 7927  df-2nd 7928  df-func 17767

This theorem is referenced by:  cofuval  17791  cofu1  17793  cofu2  17795  cofuval2  17796  cofucl  17797  cofuass  17798  cofulid  17799  cofurid  17800  funcres  17805  funcres2  17807  wunfunc  17810  funcpropd  17811  relfull  17819  relfth  17820  isfull  17821  isfth  17825  idffth  17844  cofull  17845  cofth  17846  ressffth  17849  isnat  17859  isnat2  17860  nat1st2nd  17863  fuccocl  17876  fucidcl  17877  fuclid  17878  fucrid  17879  fucass  17880  fucsect  17884  fucinv  17885  invfuc  17886  fuciso  17887  natpropd  17888  fucpropd  17889  catciso  18020  prfval  18107  prfcl  18111  prf1st  18112  prf2nd  18113  1st2ndprf  18114  evlfcllem  18129  evlfcl  18130  curf1cl  18136  curf2cl  18139  curfcl  18140  uncf1  18144  uncf2  18145  curfuncf  18146  uncfcurf  18147  diag1cl  18150  diag2cl  18154  curf2ndf  18155  yon1cl  18171  oyon1cl  18179  yonedalem1  18180  yonedalem21  18181  yonedalem3a  18182  yonedalem4c  18185  yonedalem22  18186  yonedalem3b  18187  yonedalem3  18188  yonedainv  18189  yonffthlem  18190  yoniso  18193  func1st2nd  49201  func1st  49202  func2nd  49203  0funcg  49210  0funcALT  49213  cofu1st2nd  49217  idfurcl  49223  oppfval  49261  oppfval2  49262  oppfoppc2  49267  funcoppc4  49269  funcoppc5  49270  oppff1  49273  oppff1o  49274  imassc  49278  imaid  49279  imaf1co  49280  imasubc3  49281  idfth  49283  upfval3  49303  up1st2nd  49310  up1st2ndr  49311  uptrlem2  49336  uptra  49340  uobeqw  49344  uobeq  49345  uptr2a  49347  natoppfb  49356  diag1  49429  fuco112  49454  fuco111  49455  fuco21  49461  fuco11bALT  49463  fuco22nat  49471  fucof21  49472  fucoid  49473  fucoid2  49474  fuco22a  49475  fucocolem4  49481  precofvalALT  49493  precofval3  49496  reldmprcof1  49506  prcoftposcurfuco  49508  prcoftposcurfucoa  49509  prcofdiag1  49518  prcofdiag  49519  oppfdiag1  49539  oppfdiag  49541  functhincfun  49574  functermc2  49634  eufunclem  49646  termcfuncval  49657  diagffth  49663  reldmlmd2  49778  reldmcmd2  49779  lmddu  49792  cmddu  49793  lmdran  49796  cmdlan  49797