Theorem rellan

Description: The set of left Kan extensions is a relation. (Contributed by Zhi Wang, 3-Nov-2025)

	Ref	Expression
Assertion	rellan	Could not format assertion : No typesetting found for |- Rel ( F ( P Lan E ) X ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rel0	$$⊢\mathrm{Rel}\varnothing$$
2		releq	Could not format ( ( F ( P Lan E ) X ) = (/) -> ( Rel ( F ( P Lan E ) X ) <-> Rel (/) ) ) : No typesetting found for |- ( ( F ( P Lan E ) X ) = (/) -> ( Rel ( F ( P Lan E ) X ) <-> Rel (/) ) ) with typecode |-
3	1 2	mpbiri	Could not format ( ( F ( P Lan E ) X ) = (/) -> Rel ( F ( P Lan E ) X ) ) : No typesetting found for |- ( ( F ( P Lan E ) X ) = (/) -> Rel ( F ( P Lan E ) X ) ) with typecode |-
4		n0	Could not format ( ( F ( P Lan E ) X ) =/= (/) <-> E. x x e. ( F ( P Lan E ) X ) ) : No typesetting found for |- ( ( F ( P Lan E ) X ) =/= (/) <-> E. x x e. ( F ( P Lan E ) X ) ) with typecode |-
5		relup	Could not format Rel ( ( <. ( 2nd ` P ) , E >. -o.F F ) ( ( ( 2nd ` P ) FuncCat E ) UP ( ( 1st ` P ) FuncCat E ) ) X ) : No typesetting found for |- Rel ( ( <. ( 2nd ` P ) , E >. -o.F F ) ( ( ( 2nd ` P ) FuncCat E ) UP ( ( 1st ` P ) FuncCat E ) ) X ) with typecode |-
6		ne0i	Could not format ( x e. ( F ( P Lan E ) X ) -> ( F ( P Lan E ) X ) =/= (/) ) : No typesetting found for |- ( x e. ( F ( P Lan E ) X ) -> ( F ( P Lan E ) X ) =/= (/) ) with typecode |-
7		oveq	Could not format ( ( P Lan E ) = (/) -> ( F ( P Lan E ) X ) = ( F (/) X ) ) : No typesetting found for |- ( ( P Lan E ) = (/) -> ( F ( P Lan E ) X ) = ( F (/) X ) ) with typecode |-
8		0ov	$$⊢F\varnothing X=\varnothing$$
9	7 8	eqtrdi	Could not format ( ( P Lan E ) = (/) -> ( F ( P Lan E ) X ) = (/) ) : No typesetting found for |- ( ( P Lan E ) = (/) -> ( F ( P Lan E ) X ) = (/) ) with typecode |-
10	9	necon3i	Could not format ( ( F ( P Lan E ) X ) =/= (/) -> ( P Lan E ) =/= (/) ) : No typesetting found for |- ( ( F ( P Lan E ) X ) =/= (/) -> ( P Lan E ) =/= (/) ) with typecode |-
11		n0	Could not format ( ( P Lan E ) =/= (/) <-> E. x x e. ( P Lan E ) ) : No typesetting found for |- ( ( P Lan E ) =/= (/) <-> E. x x e. ( P Lan E ) ) with typecode |-
12		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 |-
13	12	elmpocl1	Could not format ( x e. ( P Lan E ) -> P e. ( _V X. _V ) ) : No typesetting found for |- ( x e. ( P Lan E ) -> P e. ( _V X. _V ) ) with typecode |-
14		1st2nd2	$$⊢P\in \left(\mathrm{V}\times \mathrm{V}\right)\to P=⟨1^{st}\left(P\right),2^{nd}\left(P\right)⟩$$
15	13 14	syl	Could not format ( x e. ( P Lan E ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) : No typesetting found for |- ( x e. ( P Lan E ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) with typecode |-
16	15	exlimiv	Could not format ( E. x x e. ( P Lan E ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) : No typesetting found for |- ( E. x x e. ( P Lan E ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) with typecode |-
17	11 16	sylbi	Could not format ( ( P Lan E ) =/= (/) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) : No typesetting found for |- ( ( P Lan E ) =/= (/) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) with typecode |-
18	6 10 17	3syl	Could not format ( x e. ( F ( P Lan E ) X ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) : No typesetting found for |- ( x e. ( F ( P Lan E ) X ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) with typecode |-
19	18	oveq1d	Could not format ( x e. ( F ( P Lan E ) X ) -> ( P Lan E ) = ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan E ) ) : No typesetting found for |- ( x e. ( F ( P Lan E ) X ) -> ( P Lan E ) = ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan E ) ) with typecode |-
20	19	oveqd	Could not format ( x e. ( F ( P Lan E ) X ) -> ( F ( P Lan E ) X ) = ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan E ) X ) ) : No typesetting found for |- ( x e. ( F ( P Lan E ) X ) -> ( F ( P Lan E ) X ) = ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan E ) X ) ) with typecode |-
21		eqid	$$⊢2^{nd}\left(P\right)\mathrm{FuncCat}E=2^{nd}\left(P\right)\mathrm{FuncCat}E$$
22		eqid	$$⊢1^{st}\left(P\right)\mathrm{FuncCat}E=1^{st}\left(P\right)\mathrm{FuncCat}E$$
23		id	Could not format ( x e. ( F ( P Lan E ) X ) -> x e. ( F ( P Lan E ) X ) ) : No typesetting found for |- ( x e. ( F ( P Lan E ) X ) -> x e. ( F ( P Lan E ) X ) ) with typecode |-
24	23 20	eleqtrd	Could not format ( x e. ( F ( P Lan E ) X ) -> x e. ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan E ) X ) ) : No typesetting found for |- ( x e. ( F ( P Lan E ) X ) -> x e. ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan E ) X ) ) with typecode |-
25		lanrcl	Could not format ( x e. ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan E ) X ) -> ( F e. ( ( 1st ` P ) Func ( 2nd ` P ) ) /\ X e. ( ( 1st ` P ) Func E ) ) ) : No typesetting found for |- ( x e. ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan E ) X ) -> ( F e. ( ( 1st ` P ) Func ( 2nd ` P ) ) /\ X e. ( ( 1st ` P ) Func E ) ) ) with typecode |-
26	24 25	syl	Could not format ( x e. ( F ( P Lan E ) X ) -> ( F e. ( ( 1st ` P ) Func ( 2nd ` P ) ) /\ X e. ( ( 1st ` P ) Func E ) ) ) : No typesetting found for |- ( x e. ( F ( P Lan E ) X ) -> ( F e. ( ( 1st ` P ) Func ( 2nd ` P ) ) /\ X e. ( ( 1st ` P ) Func E ) ) ) with typecode |-
27	26	simpld	Could not format ( x e. ( F ( P Lan E ) X ) -> F e. ( ( 1st ` P ) Func ( 2nd ` P ) ) ) : No typesetting found for |- ( x e. ( F ( P Lan E ) X ) -> F e. ( ( 1st ` P ) Func ( 2nd ` P ) ) ) with typecode |-
28	26	simprd	Could not format ( x e. ( F ( P Lan E ) X ) -> X e. ( ( 1st ` P ) Func E ) ) : No typesetting found for |- ( x e. ( F ( P Lan E ) X ) -> X e. ( ( 1st ` P ) Func E ) ) with typecode |-
29		eqidd	Could not format ( x e. ( F ( P Lan E ) X ) -> ( <. ( 2nd ` P ) , E >. -o.F F ) = ( <. ( 2nd ` P ) , E >. -o.F F ) ) : No typesetting found for |- ( x e. ( F ( P Lan E ) X ) -> ( <. ( 2nd ` P ) , E >. -o.F F ) = ( <. ( 2nd ` P ) , E >. -o.F F ) ) with typecode |-
30	21 22 27 28 29	lanval	Could not format ( x e. ( F ( P Lan E ) X ) -> ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan E ) X ) = ( ( <. ( 2nd ` P ) , E >. -o.F F ) ( ( ( 2nd ` P ) FuncCat E ) UP ( ( 1st ` P ) FuncCat E ) ) X ) ) : No typesetting found for |- ( x e. ( F ( P Lan E ) X ) -> ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan E ) X ) = ( ( <. ( 2nd ` P ) , E >. -o.F F ) ( ( ( 2nd ` P ) FuncCat E ) UP ( ( 1st ` P ) FuncCat E ) ) X ) ) with typecode |-
31	20 30	eqtrd	Could not format ( x e. ( F ( P Lan E ) X ) -> ( F ( P Lan E ) X ) = ( ( <. ( 2nd ` P ) , E >. -o.F F ) ( ( ( 2nd ` P ) FuncCat E ) UP ( ( 1st ` P ) FuncCat E ) ) X ) ) : No typesetting found for |- ( x e. ( F ( P Lan E ) X ) -> ( F ( P Lan E ) X ) = ( ( <. ( 2nd ` P ) , E >. -o.F F ) ( ( ( 2nd ` P ) FuncCat E ) UP ( ( 1st ` P ) FuncCat E ) ) X ) ) with typecode |-
32	31	releqd	Could not format ( x e. ( F ( P Lan E ) X ) -> ( Rel ( F ( P Lan E ) X ) <-> Rel ( ( <. ( 2nd ` P ) , E >. -o.F F ) ( ( ( 2nd ` P ) FuncCat E ) UP ( ( 1st ` P ) FuncCat E ) ) X ) ) ) : No typesetting found for |- ( x e. ( F ( P Lan E ) X ) -> ( Rel ( F ( P Lan E ) X ) <-> Rel ( ( <. ( 2nd ` P ) , E >. -o.F F ) ( ( ( 2nd ` P ) FuncCat E ) UP ( ( 1st ` P ) FuncCat E ) ) X ) ) ) with typecode |-
33	5 32	mpbiri	Could not format ( x e. ( F ( P Lan E ) X ) -> Rel ( F ( P Lan E ) X ) ) : No typesetting found for |- ( x e. ( F ( P Lan E ) X ) -> Rel ( F ( P Lan E ) X ) ) with typecode |-
34	33	exlimiv	Could not format ( E. x x e. ( F ( P Lan E ) X ) -> Rel ( F ( P Lan E ) X ) ) : No typesetting found for |- ( E. x x e. ( F ( P Lan E ) X ) -> Rel ( F ( P Lan E ) X ) ) with typecode |-
35	4 34	sylbi	Could not format ( ( F ( P Lan E ) X ) =/= (/) -> Rel ( F ( P Lan E ) X ) ) : No typesetting found for |- ( ( F ( P Lan E ) X ) =/= (/) -> Rel ( F ( P Lan E ) X ) ) with typecode |-
36	3 35	pm2.61ine	Could not format Rel ( F ( P Lan E ) X ) : No typesetting found for |- Rel ( F ( P Lan E ) X ) with typecode |-