Theorem lanup

Description: The universal property of the left Kan extension; expressed explicitly. (Contributed by Zhi Wang, 4-Nov-2025)

	Ref	Expression
Hypotheses	lanup.s	$$⊢S=C\mathrm{FuncCat}E$$
	lanup.m	$$⊢M=D\mathrm{Nat}E$$
	lanup.n	$$⊢N=C\mathrm{Nat}E$$
	lanup.x	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(S\right)$$
	lanup.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	lanup.l	$$⊢\phi \to L\in \left(D\mathrm{Func}E\right)$$
	lanup.a	$$⊢\phi \to A\in \left(XN\left(L{\circ }_{\mathrm{func}}F\right)\right)$$
Assertion	lanup	Could not format assertion : No typesetting found for |- ( ph -> ( L ( F ( <. C , D >. Lan E ) X ) A <-> A. l e. ( D Func E ) A. a e. ( X N ( l o.func F ) ) E! b e. ( L M l ) a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		lanup.s	$$⊢S=C\mathrm{FuncCat}E$$
2		lanup.m	$$⊢M=D\mathrm{Nat}E$$
3		lanup.n	$$⊢N=C\mathrm{Nat}E$$
4		lanup.x	$$⊢\underset{\dot{}}{\bullet }=\mathrm{comp}\left(S\right)$$
5		lanup.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
6		lanup.l	$$⊢\phi \to L\in \left(D\mathrm{Func}E\right)$$
7		lanup.a	$$⊢\phi \to A\in \left(XN\left(L{\circ }_{\mathrm{func}}F\right)\right)$$
8		eqid	$$⊢D\mathrm{FuncCat}E=D\mathrm{FuncCat}E$$
9	8	fucbas	$$⊢D\mathrm{Func}E={\mathrm{Base}}_{\left(D\mathrm{FuncCat}E\right)}$$
10	1	fucbas	$$⊢C\mathrm{Func}E={\mathrm{Base}}_S$$
11	8 2	fuchom	$$⊢M=\mathrm{Hom}\left(D\mathrm{FuncCat}E\right)$$
12	1 3	fuchom	$$⊢N=\mathrm{Hom}\left(S\right)$$
13	3	natrcl	$$⊢A\in \left(XN\left(L{\circ }_{\mathrm{func}}F\right)\right)\to \left(X\in \left(C\mathrm{Func}E\right)\wedge L{\circ }_{\mathrm{func}}F\in \left(C\mathrm{Func}E\right)\right)$$
14	7 13	syl	$$⊢\phi \to \left(X\in \left(C\mathrm{Func}E\right)\wedge L{\circ }_{\mathrm{func}}F\in \left(C\mathrm{Func}E\right)\right)$$
15	14	simpld	$$⊢\phi \to X\in \left(C\mathrm{Func}E\right)$$
16	15	func1st2nd	$$⊢\phi \to 1^{st}\left(X\right)\left(C\mathrm{Func}E\right)2^{nd}\left(X\right)$$
17	16	funcrcl3	$$⊢\phi \to E\in \mathrm{Cat}$$
18	8 17 1 5	prcoffunca	Could not format ( ph -> ( <. D , E >. -o.F F ) e. ( ( D FuncCat E ) Func S ) ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) e. ( ( D FuncCat E ) Func S ) ) with typecode |-
19	18	func1st2nd	Could not format ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) ( ( D FuncCat E ) Func S ) ( 2nd ` ( <. D , E >. -o.F F ) ) ) : No typesetting found for |- ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) ( ( D FuncCat E ) Func S ) ( 2nd ` ( <. D , E >. -o.F F ) ) ) with typecode |-
20		eqidd	Could not format ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` ( <. D , E >. -o.F F ) ) ) : No typesetting found for |- ( ph -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` ( <. D , E >. -o.F F ) ) ) with typecode |-
21	6 20	prcof1	Could not format ( ph -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) = ( L o.func F ) ) : No typesetting found for |- ( ph -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) = ( L o.func F ) ) with typecode |-
22	21	oveq2d	Could not format ( ph -> ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) ) = ( X N ( L o.func F ) ) ) : No typesetting found for |- ( ph -> ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) ) = ( X N ( L o.func F ) ) ) with typecode |-
23	7 22	eleqtrrd	Could not format ( ph -> A e. ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) ) ) : No typesetting found for |- ( ph -> A e. ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) ) ) with typecode |-
24	9 10 11 12 4 15 19 6 23	isup	Could not format ( ph -> ( L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( D FuncCat E ) UP S ) X ) A <-> A. l e. ( D Func E ) A. a e. ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) E! b e. ( L M l ) a = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) ) : No typesetting found for |- ( ph -> ( L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( D FuncCat E ) UP S ) X ) A <-> A. l e. ( D Func E ) A. a e. ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) E! b e. ( L M l ) a = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) ) with typecode |-
25		eqidd	Could not format ( ph -> ( <. D , E >. -o.F F ) = ( <. D , E >. -o.F F ) ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) = ( <. D , E >. -o.F F ) ) with typecode |-
26	8 1 5 15 25	lanval	Could not format ( ph -> ( F ( <. C , D >. Lan E ) X ) = ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP S ) X ) ) : No typesetting found for |- ( ph -> ( F ( <. C , D >. Lan E ) X ) = ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP S ) X ) ) with typecode |-
27	26	breqd	Could not format ( ph -> ( L ( F ( <. C , D >. Lan E ) X ) A <-> L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP S ) X ) A ) ) : No typesetting found for |- ( ph -> ( L ( F ( <. C , D >. Lan E ) X ) A <-> L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP S ) X ) A ) ) with typecode |-
28	18	up1st2ndb	Could not format ( ph -> ( L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP S ) X ) A <-> L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( D FuncCat E ) UP S ) X ) A ) ) : No typesetting found for |- ( ph -> ( L ( ( <. D , E >. -o.F F ) ( ( D FuncCat E ) UP S ) X ) A <-> L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( D FuncCat E ) UP S ) X ) A ) ) with typecode |-
29	27 28	bitrd	Could not format ( ph -> ( L ( F ( <. C , D >. Lan E ) X ) A <-> L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( D FuncCat E ) UP S ) X ) A ) ) : No typesetting found for |- ( ph -> ( L ( F ( <. C , D >. Lan E ) X ) A <-> L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( D FuncCat E ) UP S ) X ) A ) ) with typecode |-
30		simpr	$$⊢\left(\phi \wedge l\in \left(D\mathrm{Func}E\right)\right)\to l\in \left(D\mathrm{Func}E\right)$$
31		eqidd	Could not format ( ( ph /\ l e. ( D Func E ) ) -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` ( <. D , E >. -o.F F ) ) ) : No typesetting found for |- ( ( ph /\ l e. ( D Func E ) ) -> ( 1st ` ( <. D , E >. -o.F F ) ) = ( 1st ` ( <. D , E >. -o.F F ) ) ) with typecode |-
32	30 31	prcof1	Could not format ( ( ph /\ l e. ( D Func E ) ) -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) = ( l o.func F ) ) : No typesetting found for |- ( ( ph /\ l e. ( D Func E ) ) -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) = ( l o.func F ) ) with typecode |-
33	32	eqcomd	Could not format ( ( ph /\ l e. ( D Func E ) ) -> ( l o.func F ) = ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) : No typesetting found for |- ( ( ph /\ l e. ( D Func E ) ) -> ( l o.func F ) = ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) with typecode |-
34	33	oveq2d	Could not format ( ( ph /\ l e. ( D Func E ) ) -> ( X N ( l o.func F ) ) = ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) ) : No typesetting found for |- ( ( ph /\ l e. ( D Func E ) ) -> ( X N ( l o.func F ) ) = ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) ) with typecode |-
35	21	ad3antrrr	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) = ( L o.func F ) ) : No typesetting found for |- ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) = ( L o.func F ) ) with typecode |-
36	35	opeq2d	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. = <. X , ( L o.func F ) >. ) : No typesetting found for |- ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. = <. X , ( L o.func F ) >. ) with typecode |-
37	32	ad2antrr	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) = ( l o.func F ) ) : No typesetting found for |- ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) = ( l o.func F ) ) with typecode |-
38	36 37	oveq12d	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) = ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) ) : No typesetting found for |- ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) = ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) ) with typecode |-
39		simpr	$$⊢\left(\left(\left(\phi \wedge l\in \left(D\mathrm{Func}E\right)\right)\wedge a\in \left(XN\left(l{\circ }_{\mathrm{func}}F\right)\right)\right)\wedge b\in \left(LMl\right)\right)\to b\in \left(LMl\right)$$
40		eqidd	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( 2nd ` ( <. D , E >. -o.F F ) ) = ( 2nd ` ( <. D , E >. -o.F F ) ) ) : No typesetting found for |- ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( 2nd ` ( <. D , E >. -o.F F ) ) = ( 2nd ` ( <. D , E >. -o.F F ) ) ) with typecode |-
41	5	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge l\in \left(D\mathrm{Func}E\right)\right)\wedge a\in \left(XN\left(l{\circ }_{\mathrm{func}}F\right)\right)\right)\wedge b\in \left(LMl\right)\right)\to F\in \left(C\mathrm{Func}D\right)$$
42	2 39 40 41	prcof21a	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) = ( b o. ( 1st ` F ) ) ) : No typesetting found for |- ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) = ( b o. ( 1st ` F ) ) ) with typecode |-
43		eqidd	$$⊢\left(\left(\left(\phi \wedge l\in \left(D\mathrm{Func}E\right)\right)\wedge a\in \left(XN\left(l{\circ }_{\mathrm{func}}F\right)\right)\right)\wedge b\in \left(LMl\right)\right)\to A=A$$
44	38 42 43	oveq123d	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) ) : No typesetting found for |- ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) ) with typecode |-
45	44	eqcomd	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) : No typesetting found for |- ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) with typecode |-
46	45	eqeq2d	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) <-> a = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) ) : No typesetting found for |- ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) /\ b e. ( L M l ) ) -> ( a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) <-> a = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) ) with typecode |-
47	46	reubidva	Could not format ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) -> ( E! b e. ( L M l ) a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) <-> E! b e. ( L M l ) a = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) ) : No typesetting found for |- ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( X N ( l o.func F ) ) ) -> ( E! b e. ( L M l ) a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) <-> E! b e. ( L M l ) a = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) ) with typecode |-
48	34 47	raleqbidva	Could not format ( ( ph /\ l e. ( D Func E ) ) -> ( A. a e. ( X N ( l o.func F ) ) E! b e. ( L M l ) a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) <-> A. a e. ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) E! b e. ( L M l ) a = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) ) : No typesetting found for |- ( ( ph /\ l e. ( D Func E ) ) -> ( A. a e. ( X N ( l o.func F ) ) E! b e. ( L M l ) a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) <-> A. a e. ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) E! b e. ( L M l ) a = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) ) with typecode |-
49	48	ralbidva	Could not format ( ph -> ( A. l e. ( D Func E ) A. a e. ( X N ( l o.func F ) ) E! b e. ( L M l ) a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) <-> A. l e. ( D Func E ) A. a e. ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) E! b e. ( L M l ) a = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) ) : No typesetting found for |- ( ph -> ( A. l e. ( D Func E ) A. a e. ( X N ( l o.func F ) ) E! b e. ( L M l ) a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) <-> A. l e. ( D Func E ) A. a e. ( X N ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) E! b e. ( L M l ) a = ( ( ( L ( 2nd ` ( <. D , E >. -o.F F ) ) l ) ` b ) ( <. X , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) ) A ) ) ) with typecode |-
50	24 29 49	3bitr4d	Could not format ( ph -> ( L ( F ( <. C , D >. Lan E ) X ) A <-> A. l e. ( D Func E ) A. a e. ( X N ( l o.func F ) ) E! b e. ( L M l ) a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) ) ) : No typesetting found for |- ( ph -> ( L ( F ( <. C , D >. Lan E ) X ) A <-> A. l e. ( D Func E ) A. a e. ( X N ( l o.func F ) ) E! b e. ( L M l ) a = ( ( b o. ( 1st ` F ) ) ( <. X , ( L o.func F ) >. .xb ( l o.func F ) ) A ) ) ) with typecode |-