Theorem funcrcl 17799

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3052  [wsbc 3742  ⟨cop 4588  {copab 5162   × cxp 5630  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368  1^st c1st 7941  2^nd c2nd 7942   ↑_m cmap 8775  Xcixp 8847  Basecbs 17148  Hom chom 17200  compcco 17201  Catccat 17599  Idccid 17600   Func cfunc 17790

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-dm 5642  df-iota 6456  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-func 17794

This theorem is referenced by:  funcf1  17802  funcixp  17803  funcid  17806  funcco  17807  funcsect  17808  funcinv  17809  funciso  17810  funcoppc  17811  cofucl  17824  cofulid  17826  cofurid  17827  funcres  17832  funcres2b  17833  funcpropd  17838  funcres2c  17839  isfull  17848  isfth  17852  fthsect  17863  fthinv  17864  fthmon  17865  fthepi  17866  ffthiso  17867  natfval  17885  fucbas  17899  fuchom  17900  fucco  17901  fuccocl  17903  fucidcl  17904  fuclid  17905  fucrid  17906  fucass  17907  fucid  17910  fucsect  17911  fucinv  17912  invfuc  17913  fuciso  17914  funcsetcres2  18029  prfcl  18138  prf1st  18139  prf2nd  18140  curf1cl  18163  curfcl  18167  uncfval  18169  uncfcl  18170  uncf1  18171  uncf2  18172  curfuncf  18173  uncfcurf  18174  yonffthlem  18217  yoneda  18218  funcrcl2  49438  funcrcl3  49439  initc  49450  prcofpropd  49738  termc2  49877  euendfunc  49885  lanpropd  49974  ranpropd  49975  ranval3  49990  lmddu  50026  cmddu  50027