Theorem ranrcl

Description: Reverse closure for right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025)

	Ref	Expression
Assertion	ranrcl	Could not format assertion : No typesetting found for |- ( L e. ( F ( <. C , D >. Ran E ) X ) -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		id	Could not format ( L e. ( F ( <. C , D >. Ran E ) X ) -> L e. ( F ( <. C , D >. Ran E ) X ) ) : No typesetting found for |- ( L e. ( F ( <. C , D >. Ran E ) X ) -> L e. ( F ( <. C , D >. Ran E ) X ) ) with typecode |-
2		ne0i	Could not format ( L e. ( F ( <. C , D >. Ran E ) X ) -> ( F ( <. C , D >. Ran E ) X ) =/= (/) ) : No typesetting found for |- ( L e. ( F ( <. C , D >. Ran E ) X ) -> ( F ( <. C , D >. Ran E ) X ) =/= (/) ) with typecode |-
3		eqid	$$⊢D\mathrm{FuncCat}E=D\mathrm{FuncCat}E$$
4		eqid	$$⊢C\mathrm{FuncCat}E=C\mathrm{FuncCat}E$$
5		df-ov	Could not format ( <. C , D >. Ran E ) = ( Ran ` <. <. C , D >. , E >. ) : No typesetting found for |- ( <. C , D >. Ran E ) = ( Ran ` <. <. C , D >. , E >. ) with typecode |-
6	5	eqeq1i	Could not format ( ( <. C , D >. Ran E ) = (/) <-> ( Ran ` <. <. C , D >. , E >. ) = (/) ) : No typesetting found for |- ( ( <. C , D >. Ran E ) = (/) <-> ( Ran ` <. <. C , D >. , E >. ) = (/) ) with typecode |-
7		oveq	Could not format ( ( <. C , D >. Ran E ) = (/) -> ( F ( <. C , D >. Ran E ) X ) = ( F (/) X ) ) : No typesetting found for |- ( ( <. C , D >. Ran E ) = (/) -> ( F ( <. C , D >. Ran E ) X ) = ( F (/) X ) ) with typecode |-
8		0ov	$$⊢F\varnothing X=\varnothing$$
9	7 8	eqtrdi	Could not format ( ( <. C , D >. Ran E ) = (/) -> ( F ( <. C , D >. Ran E ) X ) = (/) ) : No typesetting found for |- ( ( <. C , D >. Ran E ) = (/) -> ( F ( <. C , D >. Ran E ) X ) = (/) ) with typecode |-
10	6 9	sylbir	Could not format ( ( Ran ` <. <. C , D >. , E >. ) = (/) -> ( F ( <. C , D >. Ran E ) X ) = (/) ) : No typesetting found for |- ( ( Ran ` <. <. C , D >. , E >. ) = (/) -> ( F ( <. C , D >. Ran E ) X ) = (/) ) with typecode |-
11	10	necon3i	Could not format ( ( F ( <. C , D >. Ran E ) X ) =/= (/) -> ( Ran ` <. <. C , D >. , E >. ) =/= (/) ) : No typesetting found for |- ( ( F ( <. C , D >. Ran E ) X ) =/= (/) -> ( Ran ` <. <. C , D >. , E >. ) =/= (/) ) with typecode |-
12		fvfundmfvn0	Could not format ( ( Ran ` <. <. C , D >. , E >. ) =/= (/) -> ( <. <. C , D >. , E >. e. dom Ran /\ Fun ( Ran |` { <. <. C , D >. , E >. } ) ) ) : No typesetting found for |- ( ( Ran ` <. <. C , D >. , E >. ) =/= (/) -> ( <. <. C , D >. , E >. e. dom Ran /\ Fun ( Ran |` { <. <. C , D >. , E >. } ) ) ) with typecode |-
13	12	simpld	Could not format ( ( Ran ` <. <. C , D >. , E >. ) =/= (/) -> <. <. C , D >. , E >. e. dom Ran ) : No typesetting found for |- ( ( Ran ` <. <. C , D >. , E >. ) =/= (/) -> <. <. C , D >. , E >. e. dom Ran ) with typecode |-
14		ranfn	Could not format Ran Fn ( ( _V X. _V ) X. _V ) : No typesetting found for |- Ran Fn ( ( _V X. _V ) X. _V ) with typecode |-
15	14	fndmi	Could not format dom Ran = ( ( _V X. _V ) X. _V ) : No typesetting found for |- dom Ran = ( ( _V X. _V ) X. _V ) with typecode |-
16	13 15	eleqtrdi	Could not format ( ( Ran ` <. <. C , D >. , E >. ) =/= (/) -> <. <. C , D >. , E >. e. ( ( _V X. _V ) X. _V ) ) : No typesetting found for |- ( ( Ran ` <. <. C , D >. , E >. ) =/= (/) -> <. <. C , D >. , E >. e. ( ( _V X. _V ) X. _V ) ) with typecode |-
17		opelxp1	$$⊢⟨⟨C,D⟩,E⟩\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}\right)\to ⟨C,D⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
18		opelxp1	$$⊢⟨C,D⟩\in \left(\mathrm{V}\times \mathrm{V}\right)\to C\in \mathrm{V}$$
19	11 16 17 18	4syl	Could not format ( ( F ( <. C , D >. Ran E ) X ) =/= (/) -> C e. _V ) : No typesetting found for |- ( ( F ( <. C , D >. Ran E ) X ) =/= (/) -> C e. _V ) with typecode |-
20		opelxp2	$$⊢⟨C,D⟩\in \left(\mathrm{V}\times \mathrm{V}\right)\to D\in \mathrm{V}$$
21	11 16 17 20	4syl	Could not format ( ( F ( <. C , D >. Ran E ) X ) =/= (/) -> D e. _V ) : No typesetting found for |- ( ( F ( <. C , D >. Ran E ) X ) =/= (/) -> D e. _V ) with typecode |-
22		opelxp2	$$⊢⟨⟨C,D⟩,E⟩\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}\right)\to E\in \mathrm{V}$$
23	11 16 22	3syl	Could not format ( ( F ( <. C , D >. Ran E ) X ) =/= (/) -> E e. _V ) : No typesetting found for |- ( ( F ( <. C , D >. Ran E ) X ) =/= (/) -> E e. _V ) with typecode |-
24		eqid	$$⊢\mathrm{oppCat}\left(D\mathrm{FuncCat}E\right)=\mathrm{oppCat}\left(D\mathrm{FuncCat}E\right)$$
25		eqid	$$⊢\mathrm{oppCat}\left(C\mathrm{FuncCat}E\right)=\mathrm{oppCat}\left(C\mathrm{FuncCat}E\right)$$
26	3 4 19 21 23 24 25	ranfval	Could not format ( ( F ( <. C , D >. Ran E ) X ) =/= (/) -> ( <. C , D >. Ran E ) = ( 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 |- ( ( F ( <. C , D >. Ran E ) X ) =/= (/) -> ( <. C , D >. Ran E ) = ( 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 |-
27	2 26	syl	Could not format ( L e. ( F ( <. C , D >. Ran E ) X ) -> ( <. C , D >. Ran E ) = ( 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 |- ( L e. ( F ( <. C , D >. Ran E ) X ) -> ( <. C , D >. Ran E ) = ( 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 |-
28	27	oveqd	Could not format ( L e. ( F ( <. C , D >. Ran E ) X ) -> ( F ( <. C , D >. Ran E ) X ) = ( F ( 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 ) ) X ) ) : No typesetting found for |- ( L e. ( F ( <. C , D >. Ran E ) X ) -> ( F ( <. C , D >. Ran E ) X ) = ( F ( 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 ) ) X ) ) with typecode |-
29	1 28	eleqtrd	Could not format ( L e. ( F ( <. C , D >. Ran E ) X ) -> L e. ( F ( 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 ) ) X ) ) : No typesetting found for |- ( L e. ( F ( <. C , D >. Ran E ) X ) -> L e. ( F ( 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 ) ) X ) ) with typecode |-
30		eqid	Could not format ( 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 ) ) = ( 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 |- ( 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 ) ) = ( 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 |-
31	30	elmpocl	Could not format ( L e. ( F ( 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 ) ) X ) -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) ) : No typesetting found for |- ( L e. ( F ( 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 ) ) X ) -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) ) with typecode |-
32	29 31	syl	Could not format ( L e. ( F ( <. C , D >. Ran E ) X ) -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) ) : No typesetting found for |- ( L e. ( F ( <. C , D >. Ran E ) X ) -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) ) with typecode |-