Metamath Proof Explorer

Theorem lanrcl

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

Ref Expression
Assertion lanrcl 
|- ( L e. ( F ( <. C , D >. Lan E ) X ) -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( L e. ( F ( <. C , D >. Lan E ) X ) -> L e. ( F ( <. C , D >. Lan E ) X ) )
2 ne0i 
 |-  ( L e. ( F ( <. C , D >. Lan E ) X ) -> ( F ( <. C , D >. Lan E ) X ) =/= (/) )
3 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
4 eqid 
 |-  ( C FuncCat E ) = ( C FuncCat E )
5 df-ov 
 |-  ( <. C , D >. Lan E ) = ( Lan ` <. <. C , D >. , E >. )
6 5 eqeq1i 
 |-  ( ( <. C , D >. Lan E ) = (/) <-> ( Lan ` <. <. C , D >. , E >. ) = (/) )
7 oveq 
 |-  ( ( <. C , D >. Lan E ) = (/) -> ( F ( <. C , D >. Lan E ) X ) = ( F (/) X ) )
8 0ov 
 |-  ( F (/) X ) = (/)
9 7 8 eqtrdi 
 |-  ( ( <. C , D >. Lan E ) = (/) -> ( F ( <. C , D >. Lan E ) X ) = (/) )
10 6 9 sylbir 
 |-  ( ( Lan ` <. <. C , D >. , E >. ) = (/) -> ( F ( <. C , D >. Lan E ) X ) = (/) )
11 10 necon3i 
 |-  ( ( F ( <. C , D >. Lan E ) X ) =/= (/) -> ( Lan ` <. <. C , D >. , E >. ) =/= (/) )
12 fvfundmfvn0 
 |-  ( ( Lan ` <. <. C , D >. , E >. ) =/= (/) -> ( <. <. C , D >. , E >. e. dom Lan /\ Fun ( Lan |` { <. <. C , D >. , E >. } ) ) )
13 12 simpld 
 |-  ( ( Lan ` <. <. C , D >. , E >. ) =/= (/) -> <. <. C , D >. , E >. e. dom Lan )
14 lanfn 
 |-  Lan Fn ( ( _V X. _V ) X. _V )
15 14 fndmi 
 |-  dom Lan = ( ( _V X. _V ) X. _V )
16 13 15 eleqtrdi 
 |-  ( ( Lan ` <. <. C , D >. , E >. ) =/= (/) -> <. <. C , D >. , E >. e. ( ( _V X. _V ) X. _V ) )
17 opelxp1 
 |-  ( <. <. C , D >. , E >. e. ( ( _V X. _V ) X. _V ) -> <. C , D >. e. ( _V X. _V ) )
18 opelxp1 
 |-  ( <. C , D >. e. ( _V X. _V ) -> C e. _V )
19 11 16 17 18 4syl 
 |-  ( ( F ( <. C , D >. Lan E ) X ) =/= (/) -> C e. _V )
20 opelxp2 
 |-  ( <. C , D >. e. ( _V X. _V ) -> D e. _V )
21 11 16 17 20 4syl 
 |-  ( ( F ( <. C , D >. Lan E ) X ) =/= (/) -> D e. _V )
22 opelxp2 
 |-  ( <. <. C , D >. , E >. e. ( ( _V X. _V ) X. _V ) -> E e. _V )
23 11 16 22 3syl 
 |-  ( ( F ( <. C , D >. Lan E ) X ) =/= (/) -> E e. _V )
24 3 4 19 21 23 lanfval 
 |-  ( ( 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 ) ) )
25 2 24 syl 
 |-  ( 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 ) ) )
26 25 oveqd 
 |-  ( 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 ) )
27 1 26 eleqtrd 
 |-  ( 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 ) )
28 eqid 
 |-  ( 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 ) )
29 28 elmpocl 
 |-  ( 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 ) ) )
30 27 29 syl 
 |-  ( L e. ( F ( <. C , D >. Lan E ) X ) -> ( F e. ( C Func D ) /\ X e. ( C Func E ) ) )