Theorem funcrcl3 49891

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 5112	. . . 4 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
3	2	biimpi 219	. . 3 ⊢ (𝐹(𝐷 Func 𝐸)𝐺 → ⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸))
4		funcrcl 17938	. . 3 ⊢ (⟨𝐹, 𝐺⟩ ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
5	1, 3, 4	3syl 19	. 2 ⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat))
6	5	simprd 501	1 ⊢ (𝜑 → 𝐸 ∈ Cat)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ⟨cop 4597   class class class wbr 5111  (class class class)co 7416  Catccat 17738   Func cfunc 17929

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-xp 5669  df-dm 5673  df-iota 6496  df-fv 6548  df-ov 7419  df-oprab 7420  df-mpo 7421  df-func 17933

This theorem is used by:  imasubc2  49963  imasubc3  49967  upciclem2  49978  upciclem3  49979  upeu2  49983  uobrcl  50004  natoppfb  50042  fuco11  50137  fuco11cl  50138  fuco21  50147  fuco11b  50148  fuco11bALT  50149  fuco22natlem2  50154  fuco22natlem  50156  fucoid  50159  fucocolem1  50164  fucolid  50172  fucorid  50173  postcofval  50175  postcofcl  50176  precofval  50178  precofvalALT  50179  precofcl  50181  prcoftposcurfuco  50194  prcof1  50199  prcof2a  50200  prcof2  50201  prcofdiag1  50204  prcofdiag  50205  fucoppclem  50218  fucoppcid  50219  eufunclem  50332  diag1f1olem  50344  diag2f1olem  50347  lanval  50430  ranval  50431  lanup  50452  ranup  50453  lmdpropd  50468  cmdpropd  50469  concl  50472  coccl  50473  concom  50474  coccom  50475  islmd  50476  iscmd  50477  termolmd  50481  lmdran  50482  cmdlan  50483