Theorem relfunc 16993

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

Syntax hints:   ∧ wa 387   ∧ w3a 1068   = wceq 1507   ∈ wcel 2050  ∀wral 3088  [wsbc 3683  ⟨cop 4448   × cxp 5406  Rel wrel 5413  ⟶wf 6186  ‘cfv 6190  (class class class)co 6978  1^st c1st 7501  2^nd c2nd 7502   ↑_𝑚 cmap 8208  Xcixp 8261  Basecbs 16342  Hom chom 16435  compcco 16436  Catccat 16796  Idccid 16797   Func cfunc 16985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-iun 4795  df-br 4931  df-opab 4993  df-mpt 5010  df-id 5313  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-iota 6154  df-fun 6192  df-fv 6198  df-ov 6981  df-oprab 6982  df-mpo 6983  df-1st 7503  df-2nd 7504  df-func 16989

This theorem is referenced by:  cofuval  17013  cofu1  17015  cofu2  17017  cofuval2  17018  cofucl  17019  cofuass  17020  cofulid  17021  cofurid  17022  funcres  17027  funcres2  17029  wunfunc  17030  funcpropd  17031  relfull  17039  relfth  17040  isfull  17041  isfth  17045  idffth  17064  cofull  17065  cofth  17066  ressffth  17069  isnat  17078  isnat2  17079  nat1st2nd  17082  fuccocl  17095  fucidcl  17096  fuclid  17097  fucrid  17098  fucass  17099  fucsect  17103  fucinv  17104  invfuc  17105  fuciso  17106  natpropd  17107  fucpropd  17108  catciso  17228  prfval  17310  prfcl  17314  prf1st  17315  prf2nd  17316  1st2ndprf  17317  evlfcllem  17332  evlfcl  17333  curf1cl  17339  curf2cl  17342  curfcl  17343  uncf1  17347  uncf2  17348  curfuncf  17349  uncfcurf  17350  diag1cl  17353  diag2cl  17357  curf2ndf  17358  yon1cl  17374  oyon1cl  17382  yonedalem1  17383  yonedalem21  17384  yonedalem3a  17385  yonedalem4c  17388  yonedalem22  17389  yonedalem3b  17390  yonedalem3  17391  yonedainv  17392  yonffthlem  17393  yoniso  17396