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\mathrm{FuncCat}E$$
	lanval.s	$$⊢S=C\mathrm{FuncCat}E$$
	lanval.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	lanval.x	$$⊢\phi \to X\in \left(C\mathrm{Func}E\right)$$
	lanval.k	No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) = K ) with typecode |-
Assertion	lanval	Could not format assertion : No typesetting found for |- ( ph -> ( F ( <. C , D >. Lan E ) X ) = ( K ( R UP S ) X ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		lanval.r	$$⊢R=D\mathrm{FuncCat}E$$
2		lanval.s	$$⊢S=C\mathrm{FuncCat}E$$
3		lanval.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
4		lanval.x	$$⊢\phi \to X\in \left(C\mathrm{Func}E\right)$$
5		lanval.k	Could not format ( ph -> ( <. D , E >. -o.F F ) = K ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) = K ) with typecode |-
6	3	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
7	6	funcrcl2	$$⊢\phi \to C\in \mathrm{Cat}$$
8	6	funcrcl3	$$⊢\phi \to D\in \mathrm{Cat}$$
9	4	func1st2nd	$$⊢\phi \to 1^{st}\left(X\right)\left(C\mathrm{Func}E\right)2^{nd}\left(X\right)$$
10	9	funcrcl3	$$⊢\phi \to E\in \mathrm{Cat}$$
11	1 2 7 8 10	lanfval	Could not format ( ph -> ( <. C , D >. Lan E ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) ) : No typesetting found for |- ( ph -> ( <. C , D >. Lan E ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) ) with typecode |-
12		simprl	$$⊢\left(\phi \wedge \left(f=F\wedge x=X\right)\right)\to f=F$$
13	12	oveq2d	Could not format ( ( ph /\ ( f = F /\ x = X ) ) -> ( <. D , E >. -o.F f ) = ( <. D , E >. -o.F F ) ) : No typesetting found for |- ( ( ph /\ ( f = F /\ x = X ) ) -> ( <. D , E >. -o.F f ) = ( <. D , E >. -o.F F ) ) with typecode |-
14	5	adantr	Could not format ( ( ph /\ ( f = F /\ x = X ) ) -> ( <. D , E >. -o.F F ) = K ) : No typesetting found for |- ( ( ph /\ ( f = F /\ x = X ) ) -> ( <. D , E >. -o.F F ) = K ) with typecode |-
15	13 14	eqtrd	Could not format ( ( ph /\ ( f = F /\ x = X ) ) -> ( <. D , E >. -o.F f ) = K ) : No typesetting found for |- ( ( ph /\ ( f = F /\ x = X ) ) -> ( <. D , E >. -o.F f ) = K ) with typecode |-
16		simprr	$$⊢\left(\phi \wedge \left(f=F\wedge x=X\right)\right)\to x=X$$
17	15 16	oveq12d	Could not format ( ( ph /\ ( f = F /\ x = X ) ) -> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) = ( K ( R UP S ) X ) ) : No typesetting found for |- ( ( ph /\ ( f = F /\ x = X ) ) -> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) = ( K ( R UP S ) X ) ) with typecode |-
18		ovexd	Could not format ( ph -> ( K ( R UP S ) X ) e. _V ) : No typesetting found for |- ( ph -> ( K ( R UP S ) X ) e. _V ) with typecode |-
19	11 17 3 4 18	ovmpod	Could not format ( ph -> ( F ( <. C , D >. Lan E ) X ) = ( K ( R UP S ) X ) ) : No typesetting found for |- ( ph -> ( F ( <. C , D >. Lan E ) X ) = ( K ( R UP S ) X ) ) with typecode |-