Theorem funcrcl 18047

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  ∀wral 3076  [wsbc 3738  ⟨cop 4834  {copab 5166   × cxp 5649  ⟶wf 6539  ‘cfv 6543  (class class class)co 7424  1^st c1st 8003  2^nd c2nd 8004   ↑_m cmap 8854  Xcixp 8932  Basecbs 17396  Hom chom 17448  compcco 17449  Catccat 17847  Idccid 17848   Func cfunc 18038

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5657  df-dm 5661  df-iota 6497  df-fv 6551  df-ov 7427  df-oprab 7428  df-mpo 7429  df-func 18042

This theorem is used by:  funcf1  18050  funcixp  18051  funcid  18054  funcco  18055  funcsect  18056  funcinv  18057  funciso  18058  funcoppc  18059  cofucl  18072  cofulid  18074  cofurid  18075  funcres  18080  funcres2b  18081  funcpropd  18086  funcres2c  18087  isfull  18096  isfth  18100  fthsect  18111  fthinv  18112  fthmon  18113  fthepi  18114  ffthiso  18115  natfval  18133  fucbas  18147  fuchom  18148  fucco  18149  fuccocl  18151  fucidcl  18152  fuclid  18153  fucrid  18154  fucass  18155  fucid  18158  fucsect  18159  fucinv  18160  invfuc  18161  fuciso  18162  funcsetcres2  18277  prfcl  18386  prf1st  18387  prf2nd  18388  curf1cl  18411  curfcl  18415  uncfval  18417  uncfcl  18418  uncf1  18419  uncf2  18420  curfuncf  18421  uncfcurf  18422  yonffthlem  18465  yoneda  18466  funcrcl2  50301  funcrcl3  50302  initc  50314  prcofpropd  50622  termc2  50761  euendfunc  50769  lanpropd  50906  ranpropd  50907  ranval3  50922  lmddu  50958  cmddu  50959