Theorem funcrcl2 49741

Description: Reverse closure for a functor. (Contributed by Zhi Wang, 17-Sep-2025.)

Hypothesis

Ref	Expression
funcrcl2.f	⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)

Assertion

Ref	Expression
funcrcl2	⊢ (𝜑 → 𝐷 ∈ Cat)

Proof of Theorem funcrcl2

Step	Hyp	Ref	Expression
1		funcrcl2.f	. . 3 ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)
2		df-br 5114	. . . 4 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
3	2	biimpi 219	. . 3 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
4		funcrcl 17919	. . 3 ⊢ (⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
5	1, 3, 4	3syl 19	. 2 ⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
6	5	simpld 499	1 ⊢ (𝜑 → 𝐷 ∈ Cat)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ⟨cop 4600   class class class wbr 5113  (class class class)co 7411  Catccat 17719   Func cfunc 17910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-xp 5668  df-dm 5672  df-iota 6493  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-func 17914

This theorem is referenced by:  cofid1a  49774  cofid2a  49775  cofidvala  49778  cofidf2a  49779  cofidval  49781  imaid  49816  imaf1co  49817  fthcomf  49819  upciclem3  49830  upciclem4  49831  upeu  49833  upeu2  49834  uobrcl  49855  upeu4  49858  uptrlem1  49872  natoppfb  49893  fuco11  49988  fuco11cl  49989  fuco21  49998  fuco11b  49999  fuco11bALT  50000  fucoid  50010  fucolid  50023  fucorid  50024  postcofval  50026  postcofcl  50027  precofval  50029  precofvalALT  50030  precofcl  50032  prcof1  50050  prcof2a  50051  prcof2  50052  prcofdiag1  50055  prcofdiag  50056  fucoppclem  50069  fucoppcid  50070  thincciso2  50117  isinito2  50161  isinito3  50162  eufunclem  50183  funcsn  50203  cofuterm  50207  isinito4  50209  lanval  50281  ranval  50282  lmdpropd  50319  cmdpropd  50320  concl  50323  coccl  50324  concom  50325  coccom  50326  islmd  50327  iscmd  50328