Theorem lanfval

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

	Ref	Expression
Hypotheses	lanfval.r	$$⊢R=D\mathrm{FuncCat}E$$
	lanfval.s	$$⊢S=C\mathrm{FuncCat}E$$
	lanfval.c	$$⊢\phi \to C\in U$$
	lanfval.d	$$⊢\phi \to D\in V$$
	lanfval.e	$$⊢\phi \to E\in W$$
Assertion	lanfval	Could not format assertion : 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 |-

Proof

Step	Hyp	Ref	Expression
1		lanfval.r	$$⊢R=D\mathrm{FuncCat}E$$
2		lanfval.s	$$⊢S=C\mathrm{FuncCat}E$$
3		lanfval.c	$$⊢\phi \to C\in U$$
4		lanfval.d	$$⊢\phi \to D\in V$$
5		lanfval.e	$$⊢\phi \to E\in W$$
6		df-lan	Could not format Lan = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) ) : No typesetting found for |- Lan = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) ) with typecode |-
7	6	a1i	Could not format ( ph -> Lan = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) ) ) : No typesetting found for |- ( ph -> Lan = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) ) ) with typecode |-
8		fvexd	$$⊢\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\to 1^{st}\left(p\right)\in \mathrm{V}$$
9		simprl	$$⊢\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\to p=⟨C,D⟩$$
10	9	fveq2d	$$⊢\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\to 1^{st}\left(p\right)=1^{st}\left(⟨C,D⟩\right)$$
11		op1stg	$$⊢\left(C\in U\wedge D\in V\right)\to 1^{st}\left(⟨C,D⟩\right)=C$$
12	3 4 11	syl2anc	$$⊢\phi \to 1^{st}\left(⟨C,D⟩\right)=C$$
13	12	adantr	$$⊢\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\to 1^{st}\left(⟨C,D⟩\right)=C$$
14	10 13	eqtrd	$$⊢\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\to 1^{st}\left(p\right)=C$$
15		fvexd	$$⊢\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\to 2^{nd}\left(p\right)\in \mathrm{V}$$
16		simplrl	$$⊢\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\to p=⟨C,D⟩$$
17	16	fveq2d	$$⊢\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\to 2^{nd}\left(p\right)=2^{nd}\left(⟨C,D⟩\right)$$
18		op2ndg	$$⊢\left(C\in U\wedge D\in V\right)\to 2^{nd}\left(⟨C,D⟩\right)=D$$
19	3 4 18	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨C,D⟩\right)=D$$
20	19	ad2antrr	$$⊢\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\to 2^{nd}\left(⟨C,D⟩\right)=D$$
21	17 20	eqtrd	$$⊢\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\to 2^{nd}\left(p\right)=D$$
22		simplr	$$⊢\left(\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\wedge d=D\right)\to c=C$$
23		simpr	$$⊢\left(\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\wedge d=D\right)\to d=D$$
24	22 23	oveq12d	$$⊢\left(\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\wedge d=D\right)\to c\mathrm{Func}d=C\mathrm{Func}D$$
25		simpllr	$$⊢\left(\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\wedge d=D\right)\to \left(p=⟨C,D⟩\wedge e=E\right)$$
26	25	simprd	$$⊢\left(\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\wedge d=D\right)\to e=E$$
27	22 26	oveq12d	$$⊢\left(\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\wedge d=D\right)\to c\mathrm{Func}e=C\mathrm{Func}E$$
28	23 26	oveq12d	$$⊢\left(\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\wedge d=D\right)\to d\mathrm{FuncCat}e=D\mathrm{FuncCat}E$$
29	28 1	eqtr4di	$$⊢\left(\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\wedge d=D\right)\to d\mathrm{FuncCat}e=R$$
30	22 26	oveq12d	$$⊢\left(\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\wedge d=D\right)\to c\mathrm{FuncCat}e=C\mathrm{FuncCat}E$$
31	30 2	eqtr4di	$$⊢\left(\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\wedge d=D\right)\to c\mathrm{FuncCat}e=S$$
32	29 31	oveq12d	Could not format ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( ( d FuncCat e ) UP ( c FuncCat e ) ) = ( R UP S ) ) : No typesetting found for |- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( ( d FuncCat e ) UP ( c FuncCat e ) ) = ( R UP S ) ) with typecode |-
33	23 26	opeq12d	$$⊢\left(\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\wedge d=D\right)\to ⟨d,e⟩=⟨D,E⟩$$
34	33	oveq1d	Could not format ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( <. d , e >. -o.F f ) = ( <. D , E >. -o.F f ) ) : No typesetting found for |- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( <. d , e >. -o.F f ) = ( <. D , E >. -o.F f ) ) with typecode |-
35		eqidd	$$⊢\left(\left(\left(\phi \wedge \left(p=⟨C,D⟩\wedge e=E\right)\right)\wedge c=C\right)\wedge d=D\right)\to x=x$$
36	32 34 35	oveq123d	Could not format ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) = ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) : No typesetting found for |- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) = ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) with typecode |-
37	24 27 36	mpoeq123dv	Could not format ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) ) : No typesetting found for |- ( ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) /\ d = D ) -> ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) ) with typecode |-
38	15 21 37	csbied2	Could not format ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) -> [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) ) : No typesetting found for |- ( ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) /\ c = C ) -> [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) ) with typecode |-
39	8 14 38	csbied2	Could not format ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) -> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) ) : No typesetting found for |- ( ( ph /\ ( p = <. C , D >. /\ e = E ) ) -> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) = ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) ) with typecode |-
40	3	elexd	$$⊢\phi \to C\in \mathrm{V}$$
41	4	elexd	$$⊢\phi \to D\in \mathrm{V}$$
42	40 41	opelxpd	$$⊢\phi \to ⟨C,D⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
43	5	elexd	$$⊢\phi \to E\in \mathrm{V}$$
44		ovex	$$⊢C\mathrm{Func}D\in \mathrm{V}$$
45		ovex	$$⊢C\mathrm{Func}E\in \mathrm{V}$$
46	44 45	mpoex	Could not format ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) e. _V : No typesetting found for |- ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) e. _V with typecode |-
47	46	a1i	Could not format ( ph -> ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) e. _V ) : No typesetting found for |- ( ph -> ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( R UP S ) x ) ) e. _V ) with typecode |-
48	7 39 42 43 47	ovmpod	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 |-