Theorem relfunc 17674

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

Syntax hints:   ∧ wa 397   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∀wral 3062  [wsbc 3730  ⟨cop 4583   × cxp 5622  Rel wrel 5629  ⟶wf 6479  ‘cfv 6483  (class class class)co 7341  1^st c1st 7901  2^nd c2nd 7902   ↑_m cmap 8690  Xcixp 8760  Basecbs 17009  Hom chom 17070  compcco 17071  Catccat 17470  Idccid 17471   Func cfunc 17666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5247  ax-nul 5254  ax-pr 5376  ax-un 7654

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-sbc 3731  df-csb 3847  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-iun 4947  df-br 5097  df-opab 5159  df-mpt 5180  df-id 5522  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6435  df-fun 6485  df-fv 6491  df-ov 7344  df-oprab 7345  df-mpo 7346  df-1st 7903  df-2nd 7904  df-func 17670

This theorem is referenced by:  cofuval  17694  cofu1  17696  cofu2  17698  cofuval2  17699  cofucl  17700  cofuass  17701  cofulid  17702  cofurid  17703  funcres  17708  funcres2  17710  wunfunc  17711  wunfuncOLD  17712  funcpropd  17713  relfull  17721  relfth  17722  isfull  17723  isfth  17727  idffth  17746  cofull  17747  cofth  17748  ressffth  17751  isnat  17760  isnat2  17761  nat1st2nd  17764  fuccocl  17779  fucidcl  17780  fuclid  17781  fucrid  17782  fucass  17783  fucsect  17787  fucinv  17788  invfuc  17789  fuciso  17790  natpropd  17791  fucpropd  17792  catciso  17923  prfval  18013  prfcl  18017  prf1st  18018  prf2nd  18019  1st2ndprf  18020  evlfcllem  18036  evlfcl  18037  curf1cl  18043  curf2cl  18046  curfcl  18047  uncf1  18051  uncf2  18052  curfuncf  18053  uncfcurf  18054  diag1cl  18057  diag2cl  18061  curf2ndf  18062  yon1cl  18078  oyon1cl  18086  yonedalem1  18087  yonedalem21  18088  yonedalem3a  18089  yonedalem4c  18092  yonedalem22  18093  yonedalem3b  18094  yonedalem3  18095  yonedainv  18096  yonffthlem  18097  yoniso  18100