Theorem relfunc 17787

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

Syntax hints:   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3044  [wsbc 3744  ⟨cop 4585   × cxp 5621  Rel wrel 5628  ⟶wf 6482  ‘cfv 6486  (class class class)co 7353  1^st c1st 7929  2^nd c2nd 7930   ↑_m cmap 8760  Xcixp 8831  Basecbs 17138  Hom chom 17190  compcco 17191  Catccat 17588  Idccid 17589   Func cfunc 17779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358  df-1st 7931  df-2nd 7932  df-func 17783

This theorem is referenced by:  cofuval  17807  cofu1  17809  cofu2  17811  cofuval2  17812  cofucl  17813  cofuass  17814  cofulid  17815  cofurid  17816  funcres  17821  funcres2  17823  wunfunc  17826  funcpropd  17827  relfull  17835  relfth  17836  isfull  17837  isfth  17841  idffth  17860  cofull  17861  cofth  17862  ressffth  17865  isnat  17875  isnat2  17876  nat1st2nd  17879  fuccocl  17892  fucidcl  17893  fuclid  17894  fucrid  17895  fucass  17896  fucsect  17900  fucinv  17901  invfuc  17902  fuciso  17903  natpropd  17904  fucpropd  17905  catciso  18036  prfval  18123  prfcl  18127  prf1st  18128  prf2nd  18129  1st2ndprf  18130  evlfcllem  18145  evlfcl  18146  curf1cl  18152  curf2cl  18155  curfcl  18156  uncf1  18160  uncf2  18161  curfuncf  18162  uncfcurf  18163  diag1cl  18166  diag2cl  18170  curf2ndf  18171  yon1cl  18187  oyon1cl  18195  yonedalem1  18196  yonedalem21  18197  yonedalem3a  18198  yonedalem4c  18201  yonedalem22  18202  yonedalem3b  18203  yonedalem3  18204  yonedainv  18205  yonffthlem  18206  yoniso  18209  func1st2nd  49062  func1st  49063  func2nd  49064  0funcg  49071  0funcALT  49074  cofu1st2nd  49078  idfurcl  49084  oppfval  49122  oppfval2  49123  oppfoppc2  49128  funcoppc4  49130  funcoppc5  49131  oppff1  49134  oppff1o  49135  imassc  49139  imaid  49140  imaf1co  49141  imasubc3  49142  idfth  49144  upfval3  49164  up1st2nd  49171  up1st2ndr  49172  uptrlem2  49197  uptra  49201  uobeqw  49205  uobeq  49206  uptr2a  49208  natoppfb  49217  diag1  49290  fuco112  49315  fuco111  49316  fuco21  49322  fuco11bALT  49324  fuco22nat  49332  fucof21  49333  fucoid  49334  fucoid2  49335  fuco22a  49336  fucocolem4  49342  precofvalALT  49354  precofval3  49357  reldmprcof1  49367  prcoftposcurfuco  49369  prcoftposcurfucoa  49370  prcofdiag1  49379  prcofdiag  49380  oppfdiag1  49400  oppfdiag  49402  functhincfun  49435  functermc2  49495  eufunclem  49507  termcfuncval  49518  diagffth  49524  reldmlmd2  49639  reldmcmd2  49640  lmddu  49653  cmddu  49654  lmdran  49657  cmdlan  49658