Theorem funcrcl 17801

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3044  [wsbc 3750  ⟨cop 4591  {copab 5164   × cxp 5629  ⟶wf 6495  ‘cfv 6499  (class class class)co 7369  1^st c1st 7945  2^nd c2nd 7946   ↑_m cmap 8776  Xcixp 8847  Basecbs 17155  Hom chom 17207  compcco 17208  Catccat 17601  Idccid 17602   Func cfunc 17792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-dm 5641  df-iota 6452  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-func 17796

This theorem is referenced by:  funcf1  17804  funcixp  17805  funcid  17808  funcco  17809  funcsect  17810  funcinv  17811  funciso  17812  funcoppc  17813  cofucl  17826  cofulid  17828  cofurid  17829  funcres  17834  funcres2b  17835  funcpropd  17840  funcres2c  17841  isfull  17850  isfth  17854  fthsect  17865  fthinv  17866  fthmon  17867  fthepi  17868  ffthiso  17869  natfval  17887  fucbas  17901  fuchom  17902  fucco  17903  fuccocl  17905  fucidcl  17906  fuclid  17907  fucrid  17908  fucass  17909  fucid  17912  fucsect  17913  fucinv  17914  invfuc  17915  fuciso  17916  funcsetcres2  18031  prfcl  18140  prf1st  18141  prf2nd  18142  curf1cl  18165  curfcl  18169  uncfval  18171  uncfcl  18172  uncf1  18173  uncf2  18174  curfuncf  18175  uncfcurf  18176  yonffthlem  18219  yoneda  18220  funcrcl2  49041  funcrcl3  49042  initc  49053  prcofpropd  49341  termc2  49480  euendfunc  49488  lanpropd  49577  ranpropd  49578  ranval3  49593  lmddu  49629  cmddu  49630