Theorem funcrcl 17942

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ∀wral 3081  [wsbc 3746  ⟨cop 4597  {copab 5175   × cxp 5661  ⟶wf 6536  ‘cfv 6540  (class class class)co 7419  1^st c1st 7990  2^nd c2nd 7991   ↑_m cmap 8830  Xcixp 8901  Basecbs 17291  Hom chom 17343  compcco 17344  Catccat 17742  Idccid 17743   Func cfunc 17933

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-xp 5669  df-dm 5673  df-iota 6496  df-fv 6548  df-ov 7422  df-oprab 7423  df-mpo 7424  df-func 17937

This theorem is used by:  funcf1  17945  funcixp  17946  funcid  17949  funcco  17950  funcsect  17951  funcinv  17952  funciso  17953  funcoppc  17954  cofucl  17967  cofulid  17969  cofurid  17970  funcres  17975  funcres2b  17976  funcpropd  17981  funcres2c  17982  isfull  17991  isfth  17995  fthsect  18006  fthinv  18007  fthmon  18008  fthepi  18009  ffthiso  18010  natfval  18028  fucbas  18042  fuchom  18043  fucco  18044  fuccocl  18046  fucidcl  18047  fuclid  18048  fucrid  18049  fucass  18050  fucid  18053  fucsect  18054  fucinv  18055  invfuc  18056  fuciso  18057  funcsetcres2  18172  prfcl  18281  prf1st  18282  prf2nd  18283  curf1cl  18306  curfcl  18310  uncfval  18312  uncfcl  18313  uncf1  18314  uncf2  18315  curfuncf  18316  uncfcurf  18317  yonffthlem  18360  yoneda  18361  funcrcl2  49914  funcrcl3  49915  initc  49926  prcofpropd  50214  termc2  50353  euendfunc  50361  lanpropd  50450  ranpropd  50451  ranval3  50466  lmddu  50502  cmddu  50503