Theorem funcrcl2 49700

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142  ⟨cop 4588   class class class wbr 5100  (class class class)co 7396  Catccat 17696   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:  cofid1a  49733  cofid2a  49734  cofidvala  49737  cofidf2a  49738  cofidval  49740  imaid  49775  imaf1co  49776  fthcomf  49778  upciclem3  49789  upciclem4  49790  upeu  49792  upeu2  49793  uobrcl  49814  upeu4  49817  uptrlem1  49831  natoppfb  49852  fuco11  49947  fuco11cl  49948  fuco21  49957  fuco11b  49958  fuco11bALT  49959  fucoid  49969  fucolid  49982  fucorid  49983  postcofval  49985  postcofcl  49986  precofval  49988  precofvalALT  49989  precofcl  49991  prcof1  50009  prcof2a  50010  prcof2  50011  prcofdiag1  50014  prcofdiag  50015  fucoppclem  50028  fucoppcid  50029  thincciso2  50076  isinito2  50120  isinito3  50121  eufunclem  50142  funcsn  50162  cofuterm  50166  isinito4  50168  lanval  50240  ranval  50241  lmdpropd  50278  cmdpropd  50279  concl  50282  coccl  50283  concom  50284  coccom  50285  islmd  50286  iscmd  50287