Metamath Proof Explorer

Theorem relran

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

Ref Expression
Assertion relran 
|- Rel ( F ( P Ran E ) X )

Proof

Step Hyp Ref Expression
1 rel0 
 |-  Rel (/)
2 releq 
 |-  ( ( F ( P Ran E ) X ) = (/) -> ( Rel ( F ( P Ran E ) X ) <-> Rel (/) ) )
3 1 2 mpbiri 
 |-  ( ( F ( P Ran E ) X ) = (/) -> Rel ( F ( P Ran E ) X ) )
4 n0 
 |-  ( ( F ( P Ran E ) X ) =/= (/) <-> E. x x e. ( F ( P Ran E ) X ) )
5 relup 
 |-  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 )
6 ne0i 
 |-  ( x e. ( F ( P Ran E ) X ) -> ( F ( P Ran E ) X ) =/= (/) )
7 oveq 
 |-  ( ( P Ran E ) = (/) -> ( F ( P Ran E ) X ) = ( F (/) X ) )
8 0ov 
 |-  ( F (/) X ) = (/)
9 7 8 eqtrdi 
 |-  ( ( P Ran E ) = (/) -> ( F ( P Ran E ) X ) = (/) )
10 9 necon3i 
 |-  ( ( F ( P Ran E ) X ) =/= (/) -> ( P Ran E ) =/= (/) )
11 n0 
 |-  ( ( P Ran E ) =/= (/) <-> E. x x e. ( P Ran E ) )
12 df-ran 
 |-  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 ) ) )
13 12 elmpocl1 
 |-  ( x e. ( P Ran E ) -> P e. ( _V X. _V ) )
14 1st2nd2 
 |-  ( P e. ( _V X. _V ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. )
15 13 14 syl 
 |-  ( x e. ( P Ran E ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. )
16 15 exlimiv 
 |-  ( E. x x e. ( P Ran E ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. )
17 11 16 sylbi 
 |-  ( ( P Ran E ) =/= (/) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. )
18 6 10 17 3syl 
 |-  ( x e. ( F ( P Ran E ) X ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. )
19 18 oveq1d 
 |-  ( x e. ( F ( P Ran E ) X ) -> ( P Ran E ) = ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran E ) )
20 19 oveqd 
 |-  ( x e. ( F ( P Ran E ) X ) -> ( F ( P Ran E ) X ) = ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran E ) X ) )
21 eqid 
 |-  ( ( 2nd ` P ) FuncCat E ) = ( ( 2nd ` P ) FuncCat E )
22 eqid 
 |-  ( ( 1st ` P ) FuncCat E ) = ( ( 1st ` P ) FuncCat E )
23 id 
 |-  ( x e. ( F ( P Ran E ) X ) -> x e. ( F ( P Ran E ) X ) )
24 23 20 eleqtrd 
 |-  ( x e. ( F ( P Ran E ) X ) -> x e. ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran E ) X ) )
25 ranrcl 
 |-  ( x e. ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Ran E ) X ) -> ( F e. ( ( 1st ` P ) Func ( 2nd ` P ) ) /\ X e. ( ( 1st ` P ) Func E ) ) )
26 24 25 syl 
 |-  ( x e. ( F ( P Ran E ) X ) -> ( F e. ( ( 1st ` P ) Func ( 2nd ` P ) ) /\ X e. ( ( 1st ` P ) Func E ) ) )
27 26 simpld 
 |-  ( x e. ( F ( P Ran E ) X ) -> F e. ( ( 1st ` P ) Func ( 2nd ` P ) ) )
28 26 simprd 
 |-  ( x e. ( F ( P Ran E ) X ) -> X e. ( ( 1st ` P ) Func E ) )
29 opex 
 |-  <. ( 2nd ` P ) , E >. e. _V
30 29 a1i 
 |-  ( x e. ( F ( P Ran E ) X ) -> <. ( 2nd ` P ) , E >. e. _V )
31 27 30 prcofelvv 
 |-  ( x e. ( F ( P Ran E ) X ) -> ( <. ( 2nd ` P ) , E >. -o.F F ) e. ( _V X. _V ) )
32 1st2nd2 
 |-  ( ( <. ( 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 ) ) >. )
33 31 32 syl 
 |-  ( 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 ) ) >. )
34 eqid 
 |-  ( oppCat ` ( ( 2nd ` P ) FuncCat E ) ) = ( oppCat ` ( ( 2nd ` P ) FuncCat E ) )
35 eqid 
 |-  ( oppCat ` ( ( 1st ` P ) FuncCat E ) ) = ( oppCat ` ( ( 1st ` P ) FuncCat E ) )
36 21 22 27 28 33 34 35 ranval 
 |-  ( 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 ) )
37 20 36 eqtrd 
 |-  ( 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 ) )
38 37 releqd 
 |-  ( 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 ) ) )
39 5 38 mpbiri 
 |-  ( x e. ( F ( P Ran E ) X ) -> Rel ( F ( P Ran E ) X ) )
40 39 exlimiv 
 |-  ( E. x x e. ( F ( P Ran E ) X ) -> Rel ( F ( P Ran E ) X ) )
41 4 40 sylbi 
 |-  ( ( F ( P Ran E ) X ) =/= (/) -> Rel ( F ( P Ran E ) X ) )
42 3 41 pm2.61ine 
 |-  Rel ( F ( P Ran E ) X )