Theorem funcrcl 17896

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1098   = wceq 1560   ∈ wcel 2142  ∀wral 3076  [wsbc 3744  ⟨cop 4588  {copab 5162   × cxp 5645  ⟶wf 6517  ‘cfv 6521  (class class class)co 7396  1^st c1st 7968  2^nd c2nd 7969   ↑_m cmap 8808  Xcixp 8879  Basecbs 17245  Hom chom 17297  compcco 17298  Catccat 17696  Idccid 17697   Func cfunc 17887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5653  df-dm 5657  df-iota 6477  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-func 17891

This theorem is referenced by:  funcf1  17899  funcixp  17900  funcid  17903  funcco  17904  funcsect  17905  funcinv  17906  funciso  17907  funcoppc  17908  cofucl  17921  cofulid  17923  cofurid  17924  funcres  17929  funcres2b  17930  funcpropd  17935  funcres2c  17936  isfull  17945  isfth  17949  fthsect  17960  fthinv  17961  fthmon  17962  fthepi  17963  ffthiso  17964  natfval  17982  fucbas  17996  fuchom  17997  fucco  17998  fuccocl  18000  fucidcl  18001  fuclid  18002  fucrid  18003  fucass  18004  fucid  18007  fucsect  18008  fucinv  18009  invfuc  18010  fuciso  18011  funcsetcres2  18126  prfcl  18235  prf1st  18236  prf2nd  18237  curf1cl  18260  curfcl  18264  uncfval  18266  uncfcl  18267  uncf1  18268  uncf2  18269  curfuncf  18270  uncfcurf  18271  yonffthlem  18314  yoneda  18315  funcrcl2  49700  funcrcl3  49701  initc  49712  prcofpropd  50000  termc2  50139  euendfunc  50147  lanpropd  50236  ranpropd  50237  ranval3  50252  lmddu  50288  cmddu  50289