Theorem funcrcl3 49325

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 5099	. . . 4 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
3	2	biimpi 216	. . 3 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
4		funcrcl 17787	. . 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 2113  ⟨cop 4586   class class class wbr 5098  (class class class)co 7358  Catccat 17587   Func cfunc 17778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-dm 5634  df-iota 6448  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-func 17782

This theorem is referenced by:  imasubc2  49397  imasubc3  49401  upciclem2  49412  upciclem3  49413  upeu2  49417  uobrcl  49438  natoppfb  49476  fuco11  49571  fuco11cl  49572  fuco21  49581  fuco11b  49582  fuco11bALT  49583  fuco22natlem2  49588  fuco22natlem  49590  fucoid  49593  fucocolem1  49598  fucolid  49606  fucorid  49607  postcofval  49609  postcofcl  49610  precofval  49612  precofvalALT  49613  precofcl  49615  prcoftposcurfuco  49628  prcof1  49633  prcof2a  49634  prcof2  49635  prcofdiag1  49638  prcofdiag  49639  fucoppclem  49652  fucoppcid  49653  eufunclem  49766  diag1f1olem  49778  diag2f1olem  49781  lanval  49864  ranval  49865  lanup  49886  ranup  49887  lmdpropd  49902  cmdpropd  49903  concl  49906  coccl  49907  concom  49908  coccom  49909  islmd  49910  iscmd  49911  termolmd  49915  lmdran  49916  cmdlan  49917