Theorem funcrcl 17919

Description: Reverse closure for a functor. (Contributed by Mario Carneiro, 6-Jan-2017.)

Assertion

Ref	Expression
funcrcl	⊢ (𝐹 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))

Proof of Theorem funcrcl

Dummy variables 𝑓 𝑏 𝑔 𝑚 𝑛 𝑡 𝑢 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-func 17914	. 2 ⊢ Func = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑢)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑢)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))})
2	1	elmpocl 7652	1 ⊢ (𝐹 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  ∀wral 3085  [wsbc 3753  ⟨cop 4600  {copab 5177   × cxp 5660  ⟶wf 6533  ‘cfv 6537  (class class class)co 7411  1^st c1st 7983  2^nd c2nd 7984   ↑_m cmap 8823  Xcixp 8894  Basecbs 17268  Hom chom 17320  compcco 17321  Catccat 17719  Idccid 17720   Func cfunc 17910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-xp 5668  df-dm 5672  df-iota 6493  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-func 17914

This theorem is referenced by:  funcf1  17922  funcixp  17923  funcid  17926  funcco  17927  funcsect  17928  funcinv  17929  funciso  17930  funcoppc  17931  cofucl  17944  cofulid  17946  cofurid  17947  funcres  17952  funcres2b  17953  funcpropd  17958  funcres2c  17959  isfull  17968  isfth  17972  fthsect  17983  fthinv  17984  fthmon  17985  fthepi  17986  ffthiso  17987  natfval  18005  fucbas  18019  fuchom  18020  fucco  18021  fuccocl  18023  fucidcl  18024  fuclid  18025  fucrid  18026  fucass  18027  fucid  18030  fucsect  18031  fucinv  18032  invfuc  18033  fuciso  18034  funcsetcres2  18149  prfcl  18258  prf1st  18259  prf2nd  18260  curf1cl  18283  curfcl  18287  uncfval  18289  uncfcl  18290  uncf1  18291  uncf2  18292  curfuncf  18293  uncfcurf  18294  yonffthlem  18337  yoneda  18338  funcrcl2  49741  funcrcl3  49742  initc  49753  prcofpropd  50041  termc2  50180  euendfunc  50188  lanpropd  50277  ranpropd  50278  ranval3  50293  lmddu  50329  cmddu  50330