Theorem funcrcl 17821

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ∀wral 3053  [wsbc 3723  ⟨cop 4561  {copab 5134   × cxp 5616  ⟶wf 6481  ‘cfv 6485  (class class class)co 7356  1^st c1st 7929  2^nd c2nd 7930   ↑_m cmap 8763  Xcixp 8835  Basecbs 17170  Hom chom 17222  compcco 17223  Catccat 17621  Idccid 17622   Func cfunc 17812

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-xp 5624  df-dm 5628  df-iota 6441  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-func 17816

This theorem is referenced by:  funcf1  17824  funcixp  17825  funcid  17828  funcco  17829  funcsect  17830  funcinv  17831  funciso  17832  funcoppc  17833  cofucl  17846  cofulid  17848  cofurid  17849  funcres  17854  funcres2b  17855  funcpropd  17860  funcres2c  17861  isfull  17870  isfth  17874  fthsect  17885  fthinv  17886  fthmon  17887  fthepi  17888  ffthiso  17889  natfval  17907  fucbas  17921  fuchom  17922  fucco  17923  fuccocl  17925  fucidcl  17926  fuclid  17927  fucrid  17928  fucass  17929  fucid  17932  fucsect  17933  fucinv  17934  invfuc  17935  fuciso  17936  funcsetcres2  18051  prfcl  18160  prf1st  18161  prf2nd  18162  curf1cl  18185  curfcl  18189  uncfval  18191  uncfcl  18192  uncf1  18193  uncf2  18194  curfuncf  18195  uncfcurf  18196  yonffthlem  18239  yoneda  18240  funcrcl2  49569  funcrcl3  49570  initc  49581  prcofpropd  49869  termc2  50008  euendfunc  50016  lanpropd  50105  ranpropd  50106  ranval3  50121  lmddu  50157  cmddu  50158