Theorem relfunc 17824

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

Syntax hints:   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3044  [wsbc 3753  ⟨cop 4595   × cxp 5636  Rel wrel 5643  ⟶wf 6507  ‘cfv 6511  (class class class)co 7387  1^st c1st 7966  2^nd c2nd 7967   ↑_m cmap 8799  Xcixp 8870  Basecbs 17179  Hom chom 17231  compcco 17232  Catccat 17625  Idccid 17626   Func cfunc 17816

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 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

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 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-1st 7968  df-2nd 7969  df-func 17820

This theorem is referenced by:  cofuval  17844  cofu1  17846  cofu2  17848  cofuval2  17849  cofucl  17850  cofuass  17851  cofulid  17852  cofurid  17853  funcres  17858  funcres2  17860  wunfunc  17863  funcpropd  17864  relfull  17872  relfth  17873  isfull  17874  isfth  17878  idffth  17897  cofull  17898  cofth  17899  ressffth  17902  isnat  17912  isnat2  17913  nat1st2nd  17916  fuccocl  17929  fucidcl  17930  fuclid  17931  fucrid  17932  fucass  17933  fucsect  17937  fucinv  17938  invfuc  17939  fuciso  17940  natpropd  17941  fucpropd  17942  catciso  18073  prfval  18160  prfcl  18164  prf1st  18165  prf2nd  18166  1st2ndprf  18167  evlfcllem  18182  evlfcl  18183  curf1cl  18189  curf2cl  18192  curfcl  18193  uncf1  18197  uncf2  18198  curfuncf  18199  uncfcurf  18200  diag1cl  18203  diag2cl  18207  curf2ndf  18208  yon1cl  18224  oyon1cl  18232  yonedalem1  18233  yonedalem21  18234  yonedalem3a  18235  yonedalem4c  18238  yonedalem22  18239  yonedalem3b  18240  yonedalem3  18241  yonedainv  18242  yonffthlem  18243  yoniso  18246  func1st2nd  49065  func1st  49066  func2nd  49067  0funcg  49074  0funcALT  49077  cofu1st2nd  49081  idfurcl  49087  oppfval  49125  oppfval2  49126  oppfoppc2  49131  funcoppc4  49133  funcoppc5  49134  oppff1  49137  oppff1o  49138  imassc  49142  imaid  49143  imaf1co  49144  imasubc3  49145  idfth  49147  upfval3  49167  up1st2nd  49174  up1st2ndr  49175  uptrlem2  49200  uptra  49204  uobeqw  49208  uobeq  49209  uptr2a  49211  natoppfb  49220  diag1  49293  fuco112  49318  fuco111  49319  fuco21  49325  fuco11bALT  49327  fuco22nat  49335  fucof21  49336  fucoid  49337  fucoid2  49338  fuco22a  49339  fucocolem4  49345  precofvalALT  49357  precofval3  49360  reldmprcof1  49370  prcoftposcurfuco  49372  prcoftposcurfucoa  49373  prcofdiag1  49382  prcofdiag  49383  oppfdiag1  49403  oppfdiag  49405  functhincfun  49438  functermc2  49498  eufunclem  49510  termcfuncval  49521  diagffth  49527  reldmlmd2  49642  reldmcmd2  49643  lmddu  49656  cmddu  49657  lmdran  49660  cmdlan  49661