MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  funcrcl Structured version   Visualization version   GIF version

Theorem funcrcl 16730
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.
StepHypRef Expression
1 df-func 16725 . 2 Func = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑢)(𝑓‘(2nd𝑧))) ↑𝑚 ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))})
21elmpt2cl 7023 1 (𝐹 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071   = wceq 1631  wcel 2145  wral 3061  [wsbc 3587  cop 4322  {copab 4846   × cxp 5247  wf 6027  cfv 6031  (class class class)co 6793  1st c1st 7313  2nd c2nd 7314  𝑚 cmap 8009  Xcixp 8062  Basecbs 16064  Hom chom 16160  compcco 16161  Catccat 16532  Idccid 16533   Func cfunc 16721
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-xp 5255  df-dm 5259  df-iota 5994  df-fv 6039  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-func 16725
This theorem is referenced by:  funcf1  16733  funcixp  16734  funcid  16737  funcco  16738  funcsect  16739  funcinv  16740  funciso  16741  funcoppc  16742  cofucl  16755  cofulid  16757  cofurid  16758  funcres  16763  funcres2b  16764  funcpropd  16767  funcres2c  16768  isfull  16777  isfth  16781  fthsect  16792  fthinv  16793  fthmon  16794  fthepi  16795  ffthiso  16796  natfval  16813  fucbas  16827  fuchom  16828  fucco  16829  fuccocl  16831  fucidcl  16832  fuclid  16833  fucrid  16834  fucass  16835  fucid  16838  fucsect  16839  fucinv  16840  invfuc  16841  fuciso  16842  funcsetcres2  16950  prfcl  17051  prf1st  17052  prf2nd  17053  curf1cl  17076  curfcl  17080  uncfval  17082  uncfcl  17083  uncf1  17084  uncf2  17085  curfuncf  17086  uncfcurf  17087  yonffthlem  17130  yoneda  17131
  Copyright terms: Public domain W3C validator