Theorem funcrcl 17680

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∀wral 3062  [wsbc 3734  ⟨cop 4587  {copab 5162   × cxp 5625  ⟶wf 6484  ‘cfv 6488  (class class class)co 7346  1^st c1st 7906  2^nd c2nd 7907   ↑_m cmap 8695  Xcixp 8765  Basecbs 17014  Hom chom 17075  compcco 17076  Catccat 17475  Idccid 17476   Func cfunc 17671

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 5251  ax-nul 5258  ax-pr 5379

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 3406  df-v 3445  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4278  df-if 4482  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4861  df-br 5101  df-opab 5163  df-xp 5633  df-dm 5637  df-iota 6440  df-fv 6496  df-ov 7349  df-oprab 7350  df-mpo 7351  df-func 17675

This theorem is referenced by:  funcf1  17683  funcixp  17684  funcid  17687  funcco  17688  funcsect  17689  funcinv  17690  funciso  17691  funcoppc  17692  cofucl  17705  cofulid  17707  cofurid  17708  funcres  17713  funcres2b  17714  funcpropd  17718  funcres2c  17719  isfull  17728  isfth  17732  fthsect  17743  fthinv  17744  fthmon  17745  fthepi  17746  ffthiso  17747  natfval  17764  fucbas  17779  fuchom  17780  fuchomOLD  17781  fucco  17782  fuccocl  17784  fucidcl  17785  fuclid  17786  fucrid  17787  fucass  17788  fucid  17791  fucsect  17792  fucinv  17793  invfuc  17794  fuciso  17795  funcsetcres2  17910  prfcl  18022  prf1st  18023  prf2nd  18024  curf1cl  18048  curfcl  18052  uncfval  18054  uncfcl  18055  uncf1  18056  uncf2  18057  curfuncf  18058  uncfcurf  18059  yonffthlem  18102  yoneda  18103