Metamath Proof Explorer

Theorem ranrcl

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

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

Proof

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