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  49895  func1st  49896  func2nd  49897  0funcg  49904  0funcALT  49907  cofu1st2nd  49911  idfurcl  49917  oppfval  49955  oppfval2  49956  oppfoppc2  49961  funcoppc4  49963  funcoppc5  49964  oppff1  49967  oppff1o  49968  imassc  49972  imaid  49973  imaf1co  49974  imasubc3  49975  idfth  49977  upfval3  49997  up1st2nd  50004  up1st2ndr  50005  uptrlem2  50030  uptra  50034  uobeqw  50038  uobeq  50039  uptr2a  50041  natoppfb  50050  diag1  50123  fuco112  50148  fuco111  50149  fuco21  50155  fuco11bALT  50157  fuco22nat  50165  fucof21  50166  fucoid  50167  fucoid2  50168  fuco22a  50169  fucocolem4  50175  precofvalALT  50187  precofval3  50190  reldmprcof1  50200  prcoftposcurfuco  50202  prcoftposcurfucoa  50203  prcofdiag1  50212  prcofdiag  50213  oppfdiag1  50233  oppfdiag  50235  functhincfun  50268  functermc2  50328  eufunclem  50340  termcfuncval  50351  diagffth  50357  reldmlmd2  50472  reldmcmd2  50473  lmddu  50486  cmddu  50487  lmdran  50490  cmdlan  50491