Theorem relfunc 18017

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

This proof depends on syntax axioms:   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3077  [wsbc 3739  ⟨cop 4590   × cxp 5649  Rel wrel 5656  ⟶wf 6527  ‘cfv 6531  (class class class)co 7412  1^st c1st 7988  2^nd c2nd 7989   ↑_m cmap 8831  Xcixp 8909  Basecbs 17367  Hom chom 17419  compcco 17420  Catccat 17818  Idccid 17819   Func cfunc 18009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7990  df-2nd 7991  df-func 18013

This theorem is used by:  cofuval  18037  cofu1  18039  cofu2  18041  cofuval2  18042  cofucl  18043  cofuass  18044  cofulid  18045  cofurid  18046  funcres  18051  funcres2  18053  wunfunc  18056  funcpropd  18057  relfull  18065  relfth  18066  isfull  18067  isfth  18071  idffth  18090  cofull  18091  cofth  18092  ressffth  18095  isnat  18105  isnat2  18106  nat1st2nd  18109  fuccocl  18122  fucidcl  18123  fuclid  18124  fucrid  18125  fucass  18126  fucsect  18130  fucinv  18131  invfuc  18132  fuciso  18133  natpropd  18134  fucpropd  18135  catciso  18266  prfval  18353  prfcl  18357  prf1st  18358  prf2nd  18359  1st2ndprf  18360  evlfcllem  18375  evlfcl  18376  curf1cl  18382  curf2cl  18385  curfcl  18386  uncf1  18390  uncf2  18391  curfuncf  18392  uncfcurf  18393  diag1cl  18396  diag2cl  18400  curf2ndf  18401  yon1cl  18417  oyon1cl  18425  yonedalem1  18426  yonedalem21  18427  yonedalem3a  18428  yonedalem4c  18431  yonedalem22  18432  yonedalem3b  18433  yonedalem3  18434  yonedainv  18435  yonffthlem  18436  yoniso  18439  func1st2nd  50128  func1st  50129  func2nd  50130  0funcg  50137  0funcALT  50140  cofu1st2nd  50144  idfurcl  50150  oppfval  50188  oppfval2  50189  oppfoppc2  50194  funcoppc4  50196  funcoppc5  50197  oppff1  50200  oppff1o  50201  imassc  50205  imaid  50206  imaf1co  50207  imasubc3  50208  idfth  50210  upfval3  50230  up1st2nd  50237  up1st2ndr  50238  uptrlem2  50263  uptra  50267  uobeqw  50271  uobeq  50272  uptr2a  50274  natoppfb  50283  diag1  50356  fuco112  50381  fuco111  50382  fuco21  50388  fuco11bALT  50390  fuco22nat  50398  fucof21  50399  fucoid  50400  fucoid2  50401  fuco22a  50402  fucocolem4  50408  precofvalALT  50420  precofval3  50423  reldmprcof1  50433  prcoftposcurfuco  50435  prcoftposcurfucoa  50436  prcofdiag1  50445  prcofdiag  50446  oppfdiag1  50466  oppfdiag  50468  functhincfun  50501  functermc2  50561  eufunclem  50573  termcfuncval  50584  diagffth  50590  reldmlmd2  50705  reldmcmd2  50706  lmddu  50719  cmddu  50720  lmdran  50723  cmdlan  50724