Theorem natrcl2

Description: Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025)

	Ref	Expression
Hypotheses	natrcl2.n	|- N = ( C Nat D )
	natrcl2.a	|- ( ph -> A e. ( <. F , G >. N <. K , L >. ) )
Assertion	natrcl2	|- ( ph -> F ( C Func D ) G )

Proof

Step	Hyp	Ref	Expression
1		natrcl2.n	|- N = ( C Nat D )
2		natrcl2.a	|- ( ph -> A e. ( <. F , G >. N <. K , L >. ) )
3	1	natrcl	|- ( A e. ( <. F , G >. N <. K , L >. ) -> ( <. F , G >. e. ( C Func D ) /\ <. K , L >. e. ( C Func D ) ) )
4	2 3	syl	|- ( ph -> ( <. F , G >. e. ( C Func D ) /\ <. K , L >. e. ( C Func D ) ) )
5	4	simpld	|- ( ph -> <. F , G >. e. ( C Func D ) )
6		df-br	|- ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
7	5 6	sylibr	|- ( ph -> F ( C Func D ) G )