Theorem funcrcl2 49551

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 5087	. . . 4 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
3	2	biimpi 216	. . 3 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
4		funcrcl 17819	. . 3 ⊢ (⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
5	1, 3, 4	3syl 18	. 2 ⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
6	5	simpld 494	1 ⊢ (𝜑 → 𝐷 ∈ Cat)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ⟨cop 4574   class class class wbr 5086  (class class class)co 7358  Catccat 17619   Func cfunc 17810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5628  df-dm 5632  df-iota 6446  df-fv 6498  df-ov 7361  df-oprab 7362  df-mpo 7363  df-func 17814

This theorem is referenced by:  cofid1a  49584  cofid2a  49585  cofidvala  49588  cofidf2a  49589  cofidval  49591  imaid  49626  imaf1co  49627  fthcomf  49629  upciclem3  49640  upciclem4  49641  upeu  49643  upeu2  49644  uobrcl  49665  upeu4  49668  uptrlem1  49682  natoppfb  49703  fuco11  49798  fuco11cl  49799  fuco21  49808  fuco11b  49809  fuco11bALT  49810  fucoid  49820  fucolid  49833  fucorid  49834  postcofval  49836  postcofcl  49837  precofval  49839  precofvalALT  49840  precofcl  49842  prcof1  49860  prcof2a  49861  prcof2  49862  prcofdiag1  49865  prcofdiag  49866  fucoppclem  49879  fucoppcid  49880  thincciso2  49927  isinito2  49971  isinito3  49972  eufunclem  49993  funcsn  50013  cofuterm  50017  isinito4  50019  lanval  50091  ranval  50092  lmdpropd  50129  cmdpropd  50130  concl  50133  coccl  50134  concom  50135  coccom  50136  islmd  50137  iscmd  50138