Theorem lanrcl

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

	Ref	Expression
Assertion	lanrcl	Could not format assertion : No typesetting found for |- ( L e. ( F ( <. C , D >. Lan 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 >. Lan E ) X ) -> L e. ( F ( <. C , D >. Lan E ) X ) ) : No typesetting found for |- ( L e. ( F ( <. C , D >. Lan E ) X ) -> L e. ( F ( <. C , D >. Lan E ) X ) ) with typecode |-
2		ne0i	Could not format ( L e. ( F ( <. C , D >. Lan E ) X ) -> ( F ( <. C , D >. Lan E ) X ) =/= (/) ) : No typesetting found for |- ( L e. ( F ( <. C , D >. Lan E ) X ) -> ( F ( <. C , D >. Lan 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 >. Lan E ) = ( Lan ` <. <. C , D >. , E >. ) : No typesetting found for |- ( <. C , D >. Lan E ) = ( Lan ` <. <. C , D >. , E >. ) with typecode |-
6	5	eqeq1i	Could not format ( ( <. C , D >. Lan E ) = (/) <-> ( Lan ` <. <. C , D >. , E >. ) = (/) ) : No typesetting found for |- ( ( <. C , D >. Lan E ) = (/) <-> ( Lan ` <. <. C , D >. , E >. ) = (/) ) with typecode |-
7		oveq	Could not format ( ( <. C , D >. Lan E ) = (/) -> ( F ( <. C , D >. Lan E ) X ) = ( F (/) X ) ) : No typesetting found for |- ( ( <. C , D >. Lan E ) = (/) -> ( F ( <. C , D >. Lan E ) X ) = ( F (/) X ) ) with typecode |-
8		0ov	$$⊢F\varnothing X=\varnothing$$
9	7 8	eqtrdi	Could not format ( ( <. C , D >. Lan E ) = (/) -> ( F ( <. C , D >. Lan E ) X ) = (/) ) : No typesetting found for |- ( ( <. C , D >. Lan E ) = (/) -> ( F ( <. C , D >. Lan E ) X ) = (/) ) with typecode |-
10	6 9	sylbir	Could not format ( ( Lan ` <. <. C , D >. , E >. ) = (/) -> ( F ( <. C , D >. Lan E ) X ) = (/) ) : No typesetting found for |- ( ( Lan ` <. <. C , D >. , E >. ) = (/) -> ( F ( <. C , D >. Lan E ) X ) = (/) ) with typecode |-
11	10	necon3i	Could not format ( ( F ( <. C , D >. Lan E ) X ) =/= (/) -> ( Lan ` <. <. C , D >. , E >. ) =/= (/) ) : No typesetting found for |- ( ( F ( <. C , D >. Lan E ) X ) =/= (/) -> ( Lan ` <. <. C , D >. , E >. ) =/= (/) ) with typecode |-
12		fvfundmfvn0	Could not format ( ( Lan ` <. <. C , D >. , E >. ) =/= (/) -> ( <. <. C , D >. , E >. e. dom Lan /\ Fun ( Lan |` { <. <. C , D >. , E >. } ) ) ) : No typesetting found for |- ( ( Lan ` <. <. C , D >. , E >. ) =/= (/) -> ( <. <. C , D >. , E >. e. dom Lan /\ Fun ( Lan |` { <. <. C , D >. , E >. } ) ) ) with typecode |-
13	12	simpld	Could not format ( ( Lan ` <. <. C , D >. , E >. ) =/= (/) -> <. <. C , D >. , E >. e. dom Lan ) : No typesetting found for |- ( ( Lan ` <. <. C , D >. , E >. ) =/= (/) -> <. <. C , D >. , E >. e. dom Lan ) with typecode |-
14		lanfn	Could not format Lan Fn ( ( _V X. _V ) X. _V ) : No typesetting found for |- Lan Fn ( ( _V X. _V ) X. _V ) with typecode |-
15	14	fndmi	Could not format dom Lan = ( ( _V X. _V ) X. _V ) : No typesetting found for |- dom Lan = ( ( _V X. _V ) X. _V ) with typecode |-
16	13 15	eleqtrdi	Could not format ( ( Lan ` <. <. C , D >. , E >. ) =/= (/) -> <. <. C , D >. , E >. e. ( ( _V X. _V ) X. _V ) ) : No typesetting found for |- ( ( Lan ` <. <. 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 >. Lan E ) X ) =/= (/) -> C e. _V ) : No typesetting found for |- ( ( F ( <. C , D >. Lan 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 >. Lan E ) X ) =/= (/) -> D e. _V ) : No typesetting found for |- ( ( F ( <. C , D >. Lan 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 >. Lan E ) X ) =/= (/) -> E e. _V ) : No typesetting found for |- ( ( F ( <. C , D >. Lan E ) X ) =/= (/) -> E e. _V ) with typecode |-
24	3 4 19 21 23	lanfval	Could not format ( ( F ( <. C , D >. Lan E ) X ) =/= (/) -> ( <. C , D >. Lan E ) = ( 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 |- ( ( F ( <. C , D >. Lan E ) X ) =/= (/) -> ( <. C , D >. Lan E ) = ( 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 |-
25	2 24	syl	Could not format ( L e. ( F ( <. C , D >. Lan E ) X ) -> ( <. C , D >. Lan E ) = ( 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 |- ( L e. ( F ( <. C , D >. Lan E ) X ) -> ( <. C , D >. Lan E ) = ( 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 |-
26	25	oveqd	Could not format ( L e. ( F ( <. C , D >. Lan E ) X ) -> ( F ( <. C , D >. Lan E ) X ) = ( F ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) x ) ) X ) ) : No typesetting found for |- ( L e. ( F ( <. C , D >. Lan E ) X ) -> ( F ( <. C , D >. Lan E ) X ) = ( F ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) x ) ) X ) ) with typecode |-
27	1 26	eleqtrd	Could not format ( L e. ( F ( <. C , D >. Lan E ) X ) -> L e. ( F ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) x ) ) X ) ) : No typesetting found for |- ( L e. ( F ( <. C , D >. Lan E ) X ) -> L e. ( F ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) x ) ) X ) ) with typecode |-
28		eqid	Could not format ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) x ) ) = ( 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 |- ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) x ) ) = ( 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 |-
29	28	elmpocl	Could not format ( L e. ( F ( f e. ( C Func D ) , x e. ( C Func E ) |-> ( ( <. D , E >. -o.F f ) ( ( D FuncCat E ) UP ( 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 ) |-> ( ( <. D , E >. -o.F f ) ( ( D FuncCat E ) UP ( C FuncCat E ) ) x ) ) X ) -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) ) with typecode |-
30	27 29	syl	Could not format ( L e. ( F ( <. C , D >. Lan E ) X ) -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) ) : No typesetting found for |- ( L e. ( F ( <. C , D >. Lan E ) X ) -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) ) with typecode |-