Theorem funcrcl 18031

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3077  [wsbc 3739  ⟨cop 4590  {copab 5167   × cxp 5649  ⟶wf 6533  ‘cfv 6537  (class class class)co 7418  1^st c1st 7997  2^nd c2nd 7998   ↑_m cmap 8840  Xcixp 8918  Basecbs 17380  Hom chom 17432  compcco 17433  Catccat 17831  Idccid 17832   Func cfunc 18022

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5657  df-dm 5661  df-iota 6493  df-fv 6545  df-ov 7421  df-oprab 7422  df-mpo 7423  df-func 18026

This theorem is used by:  funcf1  18034  funcixp  18035  funcid  18038  funcco  18039  funcsect  18040  funcinv  18041  funciso  18042  funcoppc  18043  cofucl  18056  cofulid  18058  cofurid  18059  funcres  18064  funcres2b  18065  funcpropd  18070  funcres2c  18071  isfull  18080  isfth  18084  fthsect  18095  fthinv  18096  fthmon  18097  fthepi  18098  ffthiso  18099  natfval  18117  fucbas  18131  fuchom  18132  fucco  18133  fuccocl  18135  fucidcl  18136  fuclid  18137  fucrid  18138  fucass  18139  fucid  18142  fucsect  18143  fucinv  18144  invfuc  18145  fuciso  18146  funcsetcres2  18261  prfcl  18370  prf1st  18371  prf2nd  18372  curf1cl  18395  curfcl  18399  uncfval  18401  uncfcl  18402  uncf1  18403  uncf2  18404  curfuncf  18405  uncfcurf  18406  yonffthlem  18449  yoneda  18450  funcrcl2  50156  funcrcl3  50157  initc  50168  prcofpropd  50456  termc2  50595  euendfunc  50603  lanpropd  50692  ranpropd  50693  ranval3  50708  lmddu  50744  cmddu  50745