Theorem relfunc 17766

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

Syntax hints:   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  ∀wral 3047  [wsbc 3741  ⟨cop 4582   × cxp 5614  Rel wrel 5621  ⟶wf 6477  ‘cfv 6481  (class class class)co 7346  1^st c1st 7919  2^nd c2nd 7920   ↑_m cmap 8750  Xcixp 8821  Basecbs 17117  Hom chom 17169  compcco 17170  Catccat 17567  Idccid 17568   Func cfunc 17758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-1st 7921  df-2nd 7922  df-func 17762

This theorem is referenced by:  cofuval  17786  cofu1  17788  cofu2  17790  cofuval2  17791  cofucl  17792  cofuass  17793  cofulid  17794  cofurid  17795  funcres  17800  funcres2  17802  wunfunc  17805  funcpropd  17806  relfull  17814  relfth  17815  isfull  17816  isfth  17820  idffth  17839  cofull  17840  cofth  17841  ressffth  17844  isnat  17854  isnat2  17855  nat1st2nd  17858  fuccocl  17871  fucidcl  17872  fuclid  17873  fucrid  17874  fucass  17875  fucsect  17879  fucinv  17880  invfuc  17881  fuciso  17882  natpropd  17883  fucpropd  17884  catciso  18015  prfval  18102  prfcl  18106  prf1st  18107  prf2nd  18108  1st2ndprf  18109  evlfcllem  18124  evlfcl  18125  curf1cl  18131  curf2cl  18134  curfcl  18135  uncf1  18139  uncf2  18140  curfuncf  18141  uncfcurf  18142  diag1cl  18145  diag2cl  18149  curf2ndf  18150  yon1cl  18166  oyon1cl  18174  yonedalem1  18175  yonedalem21  18176  yonedalem3a  18177  yonedalem4c  18180  yonedalem22  18181  yonedalem3b  18182  yonedalem3  18183  yonedainv  18184  yonffthlem  18185  yoniso  18188  func1st2nd  49107  func1st  49108  func2nd  49109  0funcg  49116  0funcALT  49119  cofu1st2nd  49123  idfurcl  49129  oppfval  49167  oppfval2  49168  oppfoppc2  49173  funcoppc4  49175  funcoppc5  49176  oppff1  49179  oppff1o  49180  imassc  49184  imaid  49185  imaf1co  49186  imasubc3  49187  idfth  49189  upfval3  49209  up1st2nd  49216  up1st2ndr  49217  uptrlem2  49242  uptra  49246  uobeqw  49250  uobeq  49251  uptr2a  49253  natoppfb  49262  diag1  49335  fuco112  49360  fuco111  49361  fuco21  49367  fuco11bALT  49369  fuco22nat  49377  fucof21  49378  fucoid  49379  fucoid2  49380  fuco22a  49381  fucocolem4  49387  precofvalALT  49399  precofval3  49402  reldmprcof1  49412  prcoftposcurfuco  49414  prcoftposcurfucoa  49415  prcofdiag1  49424  prcofdiag  49425  oppfdiag1  49445  oppfdiag  49447  functhincfun  49480  functermc2  49540  eufunclem  49552  termcfuncval  49563  diagffth  49569  reldmlmd2  49684  reldmcmd2  49685  lmddu  49698  cmddu  49699  lmdran  49702  cmdlan  49703