Theorem ranrcl3

Description: Reverse closure for right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025)

	Ref	Expression
Hypothesis	ranrcl2.l	|- ( ph -> L ( F ( <. C , D >. Ran E ) X ) A )
Assertion	ranrcl3	|- ( ph -> X e. ( C Func E ) )

Proof

Step	Hyp	Ref	Expression
1		ranrcl2.l	|- ( ph -> L ( F ( <. C , D >. Ran E ) X ) A )
2		df-br	|- ( L ( F ( <. C , D >. Ran E ) X ) A <-> <. L , A >. e. ( F ( <. C , D >. Ran E ) X ) )
3	1 2	sylib	|- ( ph -> <. L , A >. e. ( F ( <. C , D >. Ran E ) X ) )
4		ranrcl	|- ( <. L , A >. e. ( F ( <. C , D >. Ran E ) X ) -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) )
5	3 4	syl	|- ( ph -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) )
6	5	simprd	|- ( ph -> X e. ( C Func E ) )