Theorem funcrcl3 49567

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

Hypothesis

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

Assertion

Ref	Expression
funcrcl3	⊢ (𝜑 → 𝐸 ∈ Cat)

Proof of Theorem funcrcl3

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 17821	. . 3 ⊢ (⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
5	1, 3, 4	3syl 18	. 2 ⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
6	5	simprd 495	1 ⊢ (𝜑 → 𝐸 ∈ Cat)

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

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 5370

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 5630  df-dm 5634  df-iota 6448  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-func 17816

This theorem is referenced by:  imasubc2  49639  imasubc3  49643  upciclem2  49654  upciclem3  49655  upeu2  49659  uobrcl  49680  natoppfb  49718  fuco11  49813  fuco11cl  49814  fuco21  49823  fuco11b  49824  fuco11bALT  49825  fuco22natlem2  49830  fuco22natlem  49832  fucoid  49835  fucocolem1  49840  fucolid  49848  fucorid  49849  postcofval  49851  postcofcl  49852  precofval  49854  precofvalALT  49855  precofcl  49857  prcoftposcurfuco  49870  prcof1  49875  prcof2a  49876  prcof2  49877  prcofdiag1  49880  prcofdiag  49881  fucoppclem  49894  fucoppcid  49895  eufunclem  50008  diag1f1olem  50020  diag2f1olem  50023  lanval  50106  ranval  50107  lanup  50128  ranup  50129  lmdpropd  50144  cmdpropd  50145  concl  50148  coccl  50149  concom  50150  coccom  50151  islmd  50152  iscmd  50153  termolmd  50157  lmdran  50158  cmdlan  50159