Theorem funcrcl 17913

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105  ∀wral 3058  [wsbc 3790  ⟨cop 4636  {copab 5209   × cxp 5686  ⟶wf 6558  ‘cfv 6562  (class class class)co 7430  1^st c1st 8010  2^nd c2nd 8011   ↑_m cmap 8864  Xcixp 8935  Basecbs 17244  Hom chom 17308  compcco 17309  Catccat 17708  Idccid 17709   Func cfunc 17904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-xp 5694  df-dm 5698  df-iota 6515  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-func 17908

This theorem is referenced by:  funcf1  17916  funcixp  17917  funcid  17920  funcco  17921  funcsect  17922  funcinv  17923  funciso  17924  funcoppc  17925  cofucl  17938  cofulid  17940  cofurid  17941  funcres  17946  funcres2b  17947  funcpropd  17953  funcres2c  17954  isfull  17963  isfth  17967  fthsect  17978  fthinv  17979  fthmon  17980  fthepi  17981  ffthiso  17982  natfval  18000  fucbas  18015  fuchom  18016  fuchomOLD  18017  fucco  18018  fuccocl  18020  fucidcl  18021  fuclid  18022  fucrid  18023  fucass  18024  fucid  18027  fucsect  18028  fucinv  18029  invfuc  18030  fuciso  18031  funcsetcres2  18146  prfcl  18258  prf1st  18259  prf2nd  18260  curf1cl  18284  curfcl  18288  uncfval  18290  uncfcl  18291  uncf1  18292  uncf2  18293  curfuncf  18294  uncfcurf  18295  yonffthlem  18338  yoneda  18339  funcrcl2  48808  funcrcl3  48809