Theorem lanval

Description: Value of the set of left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025)

	Ref	Expression
Hypotheses	lanval.r	|- R = ( D FuncCat E )
	lanval.s	|- S = ( C FuncCat E )
	lanval.f	|- ( ph -> F e. ( C Func D ) )
	lanval.x	|- ( ph -> X e. ( C Func E ) )
	lanval.k	|- ( ph -> ( <. D , E >. -o.F F ) = K )
Assertion	lanval	|- ( ph -> ( F ( <. C , D >. Lan E ) X ) = ( K ( R UP S ) X ) )

Proof

Step	Hyp	Ref	Expression
1		lanval.r	|- R = ( D FuncCat E )
2		lanval.s	|- S = ( C FuncCat E )
3		lanval.f	|- ( ph -> F e. ( C Func D ) )
4		lanval.x	|- ( ph -> X e. ( C Func E ) )
5		lanval.k	|- ( ph -> ( <. D , E >. -o.F F ) = K )
6	3	func1st2nd	|- ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
7	6	funcrcl2	|- ( ph -> C e. Cat )
8	6	funcrcl3	|- ( ph -> D e. Cat )
9	4	func1st2nd	|- ( ph -> ( 1st ` X ) ( C Func E ) ( 2nd ` X ) )
10	9	funcrcl3	|- ( ph -> E e. Cat )
11	1 2 7 8 10	lanfval	|- ( ph -> ( <. C , D >. Lan E ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) )
12		simprl	|- ( ( ph /\ ( f = F /\ x = X ) ) -> f = F )
13	12	oveq2d	|- ( ( ph /\ ( f = F /\ x = X ) ) -> ( <. D , E >. -o.F f ) = ( <. D , E >. -o.F F ) )
14	5	adantr	|- ( ( ph /\ ( f = F /\ x = X ) ) -> ( <. D , E >. -o.F F ) = K )
15	13 14	eqtrd	|- ( ( ph /\ ( f = F /\ x = X ) ) -> ( <. D , E >. -o.F f ) = K )
16		simprr	|- ( ( ph /\ ( f = F /\ x = X ) ) -> x = X )
17	15 16	oveq12d	|- ( ( ph /\ ( f = F /\ x = X ) ) -> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) = ( K ( R UP S ) X ) )
18		ovexd	|- ( ph -> ( K ( R UP S ) X ) e. _V )
19	11 17 3 4 18	ovmpod	|- ( ph -> ( F ( <. C , D >. Lan E ) X ) = ( K ( R UP S ) X ) )