Theorem funcrcl 17785

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 17780	. 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 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ∀wral 3049  [wsbc 3738  ⟨cop 4584  {copab 5158   × cxp 5620  ⟶wf 6486  ‘cfv 6490  (class class class)co 7356  1^st c1st 7929  2^nd c2nd 7930   ↑_m cmap 8761  Xcixp 8833  Basecbs 17134  Hom chom 17186  compcco 17187  Catccat 17585  Idccid 17586   Func cfunc 17776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-xp 5628  df-dm 5632  df-iota 6446  df-fv 6498  df-ov 7359  df-oprab 7360  df-mpo 7361  df-func 17780

This theorem is referenced by:  funcf1  17788  funcixp  17789  funcid  17792  funcco  17793  funcsect  17794  funcinv  17795  funciso  17796  funcoppc  17797  cofucl  17810  cofulid  17812  cofurid  17813  funcres  17818  funcres2b  17819  funcpropd  17824  funcres2c  17825  isfull  17834  isfth  17838  fthsect  17849  fthinv  17850  fthmon  17851  fthepi  17852  ffthiso  17853  natfval  17871  fucbas  17885  fuchom  17886  fucco  17887  fuccocl  17889  fucidcl  17890  fuclid  17891  fucrid  17892  fucass  17893  fucid  17896  fucsect  17897  fucinv  17898  invfuc  17899  fuciso  17900  funcsetcres2  18015  prfcl  18124  prf1st  18125  prf2nd  18126  curf1cl  18149  curfcl  18153  uncfval  18155  uncfcl  18156  uncf1  18157  uncf2  18158  curfuncf  18159  uncfcurf  18160  yonffthlem  18203  yoneda  18204  funcrcl2  49266  funcrcl3  49267  initc  49278  prcofpropd  49566  termc2  49705  euendfunc  49713  lanpropd  49802  ranpropd  49803  ranval3  49818  lmddu  49854  cmddu  49855