Theorem relfunc 17944

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

This proof depends on syntax axioms:   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ∀wral 3082  [wsbc 3747  ⟨cop 4600   × cxp 5664  Rel wrel 5671  ⟶wf 6539  ‘cfv 6543  (class class class)co 7423  1^st c1st 7993  2^nd c2nd 7994   ↑_m cmap 8833  Xcixp 8904  Basecbs 17294  Hom chom 17346  compcco 17347  Catccat 17745  Idccid 17746   Func cfunc 17936

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-1st 7995  df-2nd 7996  df-func 17940

This theorem is used by:  cofuval  17964  cofu1  17966  cofu2  17968  cofuval2  17969  cofucl  17970  cofuass  17971  cofulid  17972  cofurid  17973  funcres  17978  funcres2  17980  wunfunc  17983  funcpropd  17984  relfull  17992  relfth  17993  isfull  17994  isfth  17998  idffth  18017  cofull  18018  cofth  18019  ressffth  18022  isnat  18032  isnat2  18033  nat1st2nd  18036  fuccocl  18049  fucidcl  18050  fuclid  18051  fucrid  18052  fucass  18053  fucsect  18057  fucinv  18058  invfuc  18059  fuciso  18060  natpropd  18061  fucpropd  18062  catciso  18193  prfval  18280  prfcl  18284  prf1st  18285  prf2nd  18286  1st2ndprf  18287  evlfcllem  18302  evlfcl  18303  curf1cl  18309  curf2cl  18312  curfcl  18313  uncf1  18317  uncf2  18318  curfuncf  18319  uncfcurf  18320  diag1cl  18323  diag2cl  18327  curf2ndf  18328  yon1cl  18344  oyon1cl  18352  yonedalem1  18353  yonedalem21  18354  yonedalem3a  18355  yonedalem4c  18358  yonedalem22  18359  yonedalem3b  18360  yonedalem3  18361  yonedainv  18362  yonffthlem  18363  yoniso  18366  func1st2nd  49894  func1st  49895  func2nd  49896  0funcg  49903  0funcALT  49906  cofu1st2nd  49910  idfurcl  49916  oppfval  49954  oppfval2  49955  oppfoppc2  49960  funcoppc4  49962  funcoppc5  49963  oppff1  49966  oppff1o  49967  imassc  49971  imaid  49972  imaf1co  49973  imasubc3  49974  idfth  49976  upfval3  49996  up1st2nd  50003  up1st2ndr  50004  uptrlem2  50029  uptra  50033  uobeqw  50037  uobeq  50038  uptr2a  50040  natoppfb  50049  diag1  50122  fuco112  50147  fuco111  50148  fuco21  50154  fuco11bALT  50156  fuco22nat  50164  fucof21  50165  fucoid  50166  fucoid2  50167  fuco22a  50168  fucocolem4  50174  precofvalALT  50186  precofval3  50189  reldmprcof1  50199  prcoftposcurfuco  50201  prcoftposcurfucoa  50202  prcofdiag1  50211  prcofdiag  50212  oppfdiag1  50232  oppfdiag  50234  functhincfun  50267  functermc2  50327  eufunclem  50339  termcfuncval  50350  diagffth  50356  reldmlmd2  50471  reldmcmd2  50472  lmddu  50485  cmddu  50486  lmdran  50489  cmdlan  50490