Theorem relran

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

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

Proof

Step	Hyp	Ref	Expression
1		rel0	$$⊢\mathrm{Rel}\varnothing$$
2		releq	Could not format ( ( F ( P Ran E ) X ) = (/) -> ( Rel ( F ( P Ran E ) X ) <-> Rel (/) ) ) : No typesetting found for |- ( ( F ( P Ran E ) X ) = (/) -> ( Rel ( F ( P Ran E ) X ) <-> Rel (/) ) ) with typecode |-
3	1 2	mpbiri	Could not format ( ( F ( P Ran E ) X ) = (/) -> Rel ( F ( P Ran E ) X ) ) : No typesetting found for |- ( ( F ( P Ran E ) X ) = (/) -> Rel ( F ( P Ran E ) X ) ) with typecode |-
4		n0	Could not format ( ( F ( P Ran E ) X ) =/= (/) <-> E. x x e. ( F ( P Ran E ) X ) ) : No typesetting found for |- ( ( F ( P Ran E ) X ) =/= (/) <-> E. x x e. ( F ( P Ran E ) X ) ) with typecode |-
5		relup	Could not format Rel ( <. ( 1st ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) , tpos ( 2nd ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) >. ( ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) UP ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) ) X ) : No typesetting found for |- Rel ( <. ( 1st ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) , tpos ( 2nd ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) >. ( ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) UP ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) ) X ) with typecode |-
6		ne0i	Could not format ( x e. ( F ( P Ran E ) X ) -> ( F ( P Ran E ) X ) =/= (/) ) : No typesetting found for |- ( x e. ( F ( P Ran E ) X ) -> ( F ( P Ran E ) X ) =/= (/) ) with typecode |-
7		oveq	Could not format ( ( P Ran E ) = (/) -> ( F ( P Ran E ) X ) = ( F (/) X ) ) : No typesetting found for |- ( ( P Ran E ) = (/) -> ( F ( P Ran E ) X ) = ( F (/) X ) ) with typecode |-
8		0ov	$$⊢F\varnothing X=\varnothing$$
9	7 8	eqtrdi	Could not format ( ( P Ran E ) = (/) -> ( F ( P Ran E ) X ) = (/) ) : No typesetting found for |- ( ( P Ran E ) = (/) -> ( F ( P Ran E ) X ) = (/) ) with typecode |-
10	9	necon3i	Could not format ( ( F ( P Ran E ) X ) =/= (/) -> ( P Ran E ) =/= (/) ) : No typesetting found for |- ( ( F ( P Ran E ) X ) =/= (/) -> ( P Ran E ) =/= (/) ) with typecode |-
11		n0	Could not format ( ( P Ran E ) =/= (/) <-> E. x x e. ( P Ran E ) ) : No typesetting found for |- ( ( P Ran E ) =/= (/) <-> E. x x e. ( P Ran E ) ) with typecode |-
12		df-ran	Could not format Ran = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( oppFunc ` ( <. d , e >. -o.F f ) ) ( ( oppCat ` ( d FuncCat e ) ) UP ( oppCat ` ( c FuncCat e ) ) ) x ) ) ) : No typesetting found for |- Ran = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( oppFunc ` ( <. d , e >. -o.F f ) ) ( ( oppCat ` ( d FuncCat e ) ) UP ( oppCat ` ( c FuncCat e ) ) ) x ) ) ) with typecode |-
13	12	elmpocl1	Could not format ( x e. ( P Ran E ) -> P e. ( _V X. _V ) ) : No typesetting found for |- ( x e. ( P Ran 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 Ran E ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) : No typesetting found for |- ( x e. ( P Ran E ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) with typecode |-
16	15	exlimiv	Could not format ( E. x x e. ( P Ran E ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) : No typesetting found for |- ( E. x x e. ( P Ran E ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) with typecode |-
17	11 16	sylbi	Could not format ( ( P Ran E ) =/= (/) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) : No typesetting found for |- ( ( P Ran E ) =/= (/) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) with typecode |-
18	6 10 17	3syl	Could not format ( x e. ( F ( P Ran E ) X ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) : No typesetting found for |- ( x e. ( F ( P Ran E ) X ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. ) with typecode |-
19	18	oveq1d	Could not format ( x e. ( F ( P Ran E ) X ) -> ( P Ran E ) = ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran E ) ) : No typesetting found for |- ( x e. ( F ( P Ran E ) X ) -> ( P Ran E ) = ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran E ) ) with typecode |-
20	19	oveqd	Could not format ( x e. ( F ( P Ran E ) X ) -> ( F ( P Ran E ) X ) = ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran E ) X ) ) : No typesetting found for |- ( x e. ( F ( P Ran E ) X ) -> ( F ( P Ran E ) X ) = ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran 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 Ran E ) X ) -> x e. ( F ( P Ran E ) X ) ) : No typesetting found for |- ( x e. ( F ( P Ran E ) X ) -> x e. ( F ( P Ran E ) X ) ) with typecode |-
24	23 20	eleqtrd	Could not format ( x e. ( F ( P Ran E ) X ) -> x e. ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran E ) X ) ) : No typesetting found for |- ( x e. ( F ( P Ran E ) X ) -> x e. ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran E ) X ) ) with typecode |-
25		ranrcl	Could not format ( x e. ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran 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 ) >. Ran 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 Ran E ) X ) -> ( F e. ( ( 1st ` P ) Func ( 2nd ` P ) ) /\ X e. ( ( 1st ` P ) Func E ) ) ) : No typesetting found for |- ( x e. ( F ( P Ran 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 Ran E ) X ) -> F e. ( ( 1st ` P ) Func ( 2nd ` P ) ) ) : No typesetting found for |- ( x e. ( F ( P Ran E ) X ) -> F e. ( ( 1st ` P ) Func ( 2nd ` P ) ) ) with typecode |-
28	26	simprd	Could not format ( x e. ( F ( P Ran E ) X ) -> X e. ( ( 1st ` P ) Func E ) ) : No typesetting found for |- ( x e. ( F ( P Ran E ) X ) -> X e. ( ( 1st ` P ) Func E ) ) with typecode |-
29		opex	$$⊢⟨2^{nd}\left(P\right),E⟩\in \mathrm{V}$$
30	29	a1i	Could not format ( x e. ( F ( P Ran E ) X ) -> <. ( 2nd ` P ) , E >. e. _V ) : No typesetting found for |- ( x e. ( F ( P Ran E ) X ) -> <. ( 2nd ` P ) , E >. e. _V ) with typecode |-
31	27 30	prcofelvv	Could not format ( x e. ( F ( P Ran E ) X ) -> ( <. ( 2nd ` P ) , E >. -o.F F ) e. ( _V X. _V ) ) : No typesetting found for |- ( x e. ( F ( P Ran E ) X ) -> ( <. ( 2nd ` P ) , E >. -o.F F ) e. ( _V X. _V ) ) with typecode |-
32		1st2nd2	Could not format ( ( <. ( 2nd ` P ) , E >. -o.F F ) e. ( _V X. _V ) -> ( <. ( 2nd ` P ) , E >. -o.F F ) = <. ( 1st ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) , ( 2nd ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) >. ) : No typesetting found for |- ( ( <. ( 2nd ` P ) , E >. -o.F F ) e. ( _V X. _V ) -> ( <. ( 2nd ` P ) , E >. -o.F F ) = <. ( 1st ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) , ( 2nd ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) >. ) with typecode |-
33	31 32	syl	Could not format ( x e. ( F ( P Ran E ) X ) -> ( <. ( 2nd ` P ) , E >. -o.F F ) = <. ( 1st ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) , ( 2nd ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) >. ) : No typesetting found for |- ( x e. ( F ( P Ran E ) X ) -> ( <. ( 2nd ` P ) , E >. -o.F F ) = <. ( 1st ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) , ( 2nd ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) >. ) with typecode |-
34		eqid	$$⊢\mathrm{oppCat}\left(2^{nd}\left(P\right)\mathrm{FuncCat}E\right)=\mathrm{oppCat}\left(2^{nd}\left(P\right)\mathrm{FuncCat}E\right)$$
35		eqid	$$⊢\mathrm{oppCat}\left(1^{st}\left(P\right)\mathrm{FuncCat}E\right)=\mathrm{oppCat}\left(1^{st}\left(P\right)\mathrm{FuncCat}E\right)$$
36	21 22 27 28 33 34 35	ranval	Could not format ( x e. ( F ( P Ran E ) X ) -> ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran E ) X ) = ( <. ( 1st ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) , tpos ( 2nd ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) >. ( ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) UP ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) ) X ) ) : No typesetting found for |- ( x e. ( F ( P Ran E ) X ) -> ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran E ) X ) = ( <. ( 1st ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) , tpos ( 2nd ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) >. ( ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) UP ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) ) X ) ) with typecode |-
37	20 36	eqtrd	Could not format ( x e. ( F ( P Ran E ) X ) -> ( F ( P Ran E ) X ) = ( <. ( 1st ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) , tpos ( 2nd ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) >. ( ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) UP ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) ) X ) ) : No typesetting found for |- ( x e. ( F ( P Ran E ) X ) -> ( F ( P Ran E ) X ) = ( <. ( 1st ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) , tpos ( 2nd ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) >. ( ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) UP ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) ) X ) ) with typecode |-
38	37	releqd	Could not format ( x e. ( F ( P Ran E ) X ) -> ( Rel ( F ( P Ran E ) X ) <-> Rel ( <. ( 1st ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) , tpos ( 2nd ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) >. ( ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) UP ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) ) X ) ) ) : No typesetting found for |- ( x e. ( F ( P Ran E ) X ) -> ( Rel ( F ( P Ran E ) X ) <-> Rel ( <. ( 1st ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) , tpos ( 2nd ` ( <. ( 2nd ` P ) , E >. -o.F F ) ) >. ( ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) UP ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) ) X ) ) ) with typecode |-
39	5 38	mpbiri	Could not format ( x e. ( F ( P Ran E ) X ) -> Rel ( F ( P Ran E ) X ) ) : No typesetting found for |- ( x e. ( F ( P Ran E ) X ) -> Rel ( F ( P Ran E ) X ) ) with typecode |-
40	39	exlimiv	Could not format ( E. x x e. ( F ( P Ran E ) X ) -> Rel ( F ( P Ran E ) X ) ) : No typesetting found for |- ( E. x x e. ( F ( P Ran E ) X ) -> Rel ( F ( P Ran E ) X ) ) with typecode |-
41	4 40	sylbi	Could not format ( ( F ( P Ran E ) X ) =/= (/) -> Rel ( F ( P Ran E ) X ) ) : No typesetting found for |- ( ( F ( P Ran E ) X ) =/= (/) -> Rel ( F ( P Ran E ) X ) ) with typecode |-
42	3 41	pm2.61ine	Could not format Rel ( F ( P Ran E ) X ) : No typesetting found for |- Rel ( F ( P Ran E ) X ) with typecode |-