Theorem funcrcl2

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

	Ref	Expression
Hypothesis	funcrcl2.f	|- ( ph -> F ( D Func E ) G )
Assertion	funcrcl2	|- ( ph -> D e. Cat )

Proof

Step	Hyp	Ref	Expression
1		funcrcl2.f	|- ( ph -> F ( D Func E ) G )
2		df-br	|- ( F ( D Func E ) G <-> <. F , G >. e. ( D Func E ) )
3	2	biimpi	|- ( F ( D Func E ) G -> <. F , G >. e. ( D Func E ) )
4		funcrcl	|- ( <. F , G >. e. ( D Func E ) -> ( D e. Cat /\ E e. Cat ) )
5	1 3 4	3syl	|- ( ph -> ( D e. Cat /\ E e. Cat ) )
6	5	simpld	|- ( ph -> D e. Cat )