Theorem ranup

Description: The universal property of the right Kan extension; expressed explicitly. (Contributed by Zhi Wang, 5-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)$$
	ranup.a	$$⊢\phi \to A\in \left(\left(L{\circ }_{\mathrm{func}}F\right)NX\right)$$
Assertion	ranup	Could not format assertion : No typesetting found for |- ( ph -> ( L ( F ( <. C , D >. Ran E ) X ) A <-> A. l e. ( D Func E ) A. a e. ( ( l o.func F ) N X ) E! b e. ( l M L ) a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) ) ) 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		ranup.a	$$⊢\phi \to A\in \left(\left(L{\circ }_{\mathrm{func}}F\right)NX\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(\left(L{\circ }_{\mathrm{func}}F\right)NX\right)\to \left(L{\circ }_{\mathrm{func}}F\in \left(C\mathrm{Func}E\right)\wedge X\in \left(C\mathrm{Func}E\right)\right)$$
14	7 13	syl	$$⊢\phi \to \left(L{\circ }_{\mathrm{func}}F\in \left(C\mathrm{Func}E\right)\wedge X\in \left(C\mathrm{Func}E\right)\right)$$
15	14	simprd	$$⊢\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		opex	$$⊢⟨D,E⟩\in \mathrm{V}$$
19	18	a1i	$$⊢\phi \to ⟨D,E⟩\in \mathrm{V}$$
20	5 19	prcofelvv	Could not format ( ph -> ( <. D , E >. -o.F F ) e. ( _V X. _V ) ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) e. ( _V X. _V ) ) with typecode |-
21		1st2nd2	Could not format ( ( <. D , E >. -o.F F ) e. ( _V X. _V ) -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) : No typesetting found for |- ( ( <. D , E >. -o.F F ) e. ( _V X. _V ) -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) with typecode |-
22	20 21	syl	Could not format ( ph -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) = <. ( 1st ` ( <. D , E >. -o.F F ) ) , ( 2nd ` ( <. D , E >. -o.F F ) ) >. ) with typecode |-
23	8 17 1 5 22	prcoffunca2	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 |-
24		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 |-
25	6 24	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 |-
26	25	oveq1d	Could not format ( ph -> ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) N X ) = ( ( L o.func F ) N X ) ) : No typesetting found for |- ( ph -> ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) N X ) = ( ( L o.func F ) N X ) ) with typecode |-
27	7 26	eleqtrrd	Could not format ( ph -> A e. ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) N X ) ) : No typesetting found for |- ( ph -> A e. ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) N X ) ) with typecode |-
28		eqid	$$⊢\mathrm{oppCat}\left(D\mathrm{FuncCat}E\right)=\mathrm{oppCat}\left(D\mathrm{FuncCat}E\right)$$
29		eqid	$$⊢\mathrm{oppCat}\left(S\right)=\mathrm{oppCat}\left(S\right)$$
30	9 10 11 12 4 15 23 6 27 28 29	oppcup	Could not format ( ph -> ( L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( oppCat ` ( D FuncCat E ) ) UP ( oppCat ` S ) ) X ) A <-> A. l e. ( D Func E ) A. a e. ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) N X ) E! b e. ( l M L ) a = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) ) : No typesetting found for |- ( ph -> ( L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( oppCat ` ( D FuncCat E ) ) UP ( oppCat ` S ) ) X ) A <-> A. l e. ( D Func E ) A. a e. ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) N X ) E! b e. ( l M L ) a = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) ) with typecode |-
31	1	fveq2i	$$⊢\mathrm{oppCat}\left(S\right)=\mathrm{oppCat}\left(C\mathrm{FuncCat}E\right)$$
32	28 31 22 5	ranval2	Could not format ( ph -> ( F ( <. C , D >. Ran E ) X ) = ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( oppCat ` ( D FuncCat E ) ) UP ( oppCat ` S ) ) X ) ) : No typesetting found for |- ( ph -> ( F ( <. C , D >. Ran E ) X ) = ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( oppCat ` ( D FuncCat E ) ) UP ( oppCat ` S ) ) X ) ) with typecode |-
33	32	breqd	Could not format ( ph -> ( L ( F ( <. C , D >. Ran E ) X ) A <-> L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( oppCat ` ( D FuncCat E ) ) UP ( oppCat ` S ) ) X ) A ) ) : No typesetting found for |- ( ph -> ( L ( F ( <. C , D >. Ran E ) X ) A <-> L ( <. ( 1st ` ( <. D , E >. -o.F F ) ) , tpos ( 2nd ` ( <. D , E >. -o.F F ) ) >. ( ( oppCat ` ( D FuncCat E ) ) UP ( oppCat ` S ) ) X ) A ) ) with typecode |-
34		simpr	$$⊢\left(\phi \wedge l\in \left(D\mathrm{Func}E\right)\right)\to l\in \left(D\mathrm{Func}E\right)$$
35		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 |-
36	34 35	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 |-
37	36	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 |-
38	37	oveq1d	Could not format ( ( ph /\ l e. ( D Func E ) ) -> ( ( l o.func F ) N X ) = ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) N X ) ) : No typesetting found for |- ( ( ph /\ l e. ( D Func E ) ) -> ( ( l o.func F ) N X ) = ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) N X ) ) with typecode |-
39	36	ad2antrr	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ 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. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) = ( l o.func F ) ) with typecode |-
40	25	ad3antrrr	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ 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. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) = ( L o.func F ) ) with typecode |-
41	39 40	opeq12d	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. = <. ( l o.func F ) , ( L o.func F ) >. ) : No typesetting found for |- ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. = <. ( l o.func F ) , ( L o.func F ) >. ) with typecode |-
42	41	oveq1d	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) = ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ) : No typesetting found for |- ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) = ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ) with typecode |-
43		eqidd	$$⊢\left(\left(\left(\phi \wedge l\in \left(D\mathrm{Func}E\right)\right)\wedge a\in \left(\left(l{\circ }_{\mathrm{func}}F\right)NX\right)\right)\wedge b\in \left(lML\right)\right)\to A=A$$
44		simpr	$$⊢\left(\left(\left(\phi \wedge l\in \left(D\mathrm{Func}E\right)\right)\wedge a\in \left(\left(l{\circ }_{\mathrm{func}}F\right)NX\right)\right)\wedge b\in \left(lML\right)\right)\to b\in \left(lML\right)$$
45		eqidd	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ 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. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( 2nd ` ( <. D , E >. -o.F F ) ) = ( 2nd ` ( <. D , E >. -o.F F ) ) ) with typecode |-
46	5	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge l\in \left(D\mathrm{Func}E\right)\right)\wedge a\in \left(\left(l{\circ }_{\mathrm{func}}F\right)NX\right)\right)\wedge b\in \left(lML\right)\right)\to F\in \left(C\mathrm{Func}D\right)$$
47	2 44 45 46	prcof21a	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ 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. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) = ( b o. ( 1st ` F ) ) ) with typecode |-
48	42 43 47	oveq123d	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) ) : No typesetting found for |- ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) ) with typecode |-
49	48	eqcomd	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) : No typesetting found for |- ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) with typecode |-
50	49	eqeq2d	Could not format ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) <-> a = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) ) : No typesetting found for |- ( ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) /\ b e. ( l M L ) ) -> ( a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) <-> a = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) ) with typecode |-
51	50	reubidva	Could not format ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) -> ( E! b e. ( l M L ) a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) <-> E! b e. ( l M L ) a = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) ) : No typesetting found for |- ( ( ( ph /\ l e. ( D Func E ) ) /\ a e. ( ( l o.func F ) N X ) ) -> ( E! b e. ( l M L ) a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) <-> E! b e. ( l M L ) a = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) ) with typecode |-
52	38 51	raleqbidva	Could not format ( ( ph /\ l e. ( D Func E ) ) -> ( A. a e. ( ( l o.func F ) N X ) E! b e. ( l M L ) a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) <-> A. a e. ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) N X ) E! b e. ( l M L ) a = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) ) : No typesetting found for |- ( ( ph /\ l e. ( D Func E ) ) -> ( A. a e. ( ( l o.func F ) N X ) E! b e. ( l M L ) a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) <-> A. a e. ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) N X ) E! b e. ( l M L ) a = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) ) with typecode |-
53	52	ralbidva	Could not format ( ph -> ( A. l e. ( D Func E ) A. a e. ( ( l o.func F ) N X ) E! b e. ( l M L ) a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) <-> A. l e. ( D Func E ) A. a e. ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) N X ) E! b e. ( l M L ) a = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) ) : No typesetting found for |- ( ph -> ( A. l e. ( D Func E ) A. a e. ( ( l o.func F ) N X ) E! b e. ( l M L ) a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) <-> A. l e. ( D Func E ) A. a e. ( ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) N X ) E! b e. ( l M L ) a = ( A ( <. ( ( 1st ` ( <. D , E >. -o.F F ) ) ` l ) , ( ( 1st ` ( <. D , E >. -o.F F ) ) ` L ) >. .xb X ) ( ( l ( 2nd ` ( <. D , E >. -o.F F ) ) L ) ` b ) ) ) ) with typecode |-
54	30 33 53	3bitr4d	Could not format ( ph -> ( L ( F ( <. C , D >. Ran E ) X ) A <-> A. l e. ( D Func E ) A. a e. ( ( l o.func F ) N X ) E! b e. ( l M L ) a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) ) ) : No typesetting found for |- ( ph -> ( L ( F ( <. C , D >. Ran E ) X ) A <-> A. l e. ( D Func E ) A. a e. ( ( l o.func F ) N X ) E! b e. ( l M L ) a = ( A ( <. ( l o.func F ) , ( L o.func F ) >. .xb X ) ( b o. ( 1st ` F ) ) ) ) ) with typecode |-