Metamath Proof Explorer

Theorem rellan

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

Ref Expression
Assertion rellan 
|- Rel ( F ( P Lan E ) X )

Proof

Step Hyp Ref Expression
1 rel0 
 |-  Rel (/)
2 releq 
 |-  ( ( F ( P Lan E ) X ) = (/) -> ( Rel ( F ( P Lan E ) X ) <-> Rel (/) ) )
3 1 2 mpbiri 
 |-  ( ( F ( P Lan E ) X ) = (/) -> Rel ( F ( P Lan E ) X ) )
4 n0 
 |-  ( ( F ( P Lan E ) X ) =/= (/) <-> E. x x e. ( F ( P Lan E ) X ) )
5 relup 
 |-  Rel ( ( <. ( 2nd ` P ) , E >. -o.F F ) ( ( ( 2nd ` P ) FuncCat E ) UP ( ( 1st ` P ) FuncCat E ) ) X )
6 ne0i 
 |-  ( x e. ( F ( P Lan E ) X ) -> ( F ( P Lan E ) X ) =/= (/) )
7 oveq 
 |-  ( ( P Lan E ) = (/) -> ( F ( P Lan E ) X ) = ( F (/) X ) )
8 0ov 
 |-  ( F (/) X ) = (/)
9 7 8 eqtrdi 
 |-  ( ( P Lan E ) = (/) -> ( F ( P Lan E ) X ) = (/) )
10 9 necon3i 
 |-  ( ( F ( P Lan E ) X ) =/= (/) -> ( P Lan E ) =/= (/) )
11 n0 
 |-  ( ( P Lan E ) =/= (/) <-> E. x x e. ( P Lan E ) )
12 df-lan 
 |-  Lan = ( p e. ( _V X. _V ) , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ ( f e. ( c Func d ) , x e. ( c Func e ) |-> ( ( <. d , e >. -o.F f ) ( ( d FuncCat e ) UP ( c FuncCat e ) ) x ) ) )
13 12 elmpocl1 
 |-  ( x e. ( P Lan 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 Lan E ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. )
16 15 exlimiv 
 |-  ( E. x x e. ( P Lan E ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. )
17 11 16 sylbi 
 |-  ( ( P Lan E ) =/= (/) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. )
18 6 10 17 3syl 
 |-  ( x e. ( F ( P Lan E ) X ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. )
19 18 oveq1d 
 |-  ( x e. ( F ( P Lan E ) X ) -> ( P Lan E ) = ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan E ) )
20 19 oveqd 
 |-  ( x e. ( F ( P Lan E ) X ) -> ( F ( P Lan E ) X ) = ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan 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 Lan E ) X ) -> x e. ( F ( P Lan E ) X ) )
24 23 20 eleqtrd 
 |-  ( x e. ( F ( P Lan E ) X ) -> x e. ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan E ) X ) )
25 lanrcl 
 |-  ( x e. ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan E ) X ) -> ( F e. ( ( 1st ` P ) Func ( 2nd ` P ) ) /\ X e. ( ( 1st ` P ) Func E ) ) )
26 24 25 syl 
 |-  ( x e. ( F ( P Lan E ) X ) -> ( F e. ( ( 1st ` P ) Func ( 2nd ` P ) ) /\ X e. ( ( 1st ` P ) Func E ) ) )
27 26 simpld 
 |-  ( x e. ( F ( P Lan E ) X ) -> F e. ( ( 1st ` P ) Func ( 2nd ` P ) ) )
28 26 simprd 
 |-  ( x e. ( F ( P Lan E ) X ) -> X e. ( ( 1st ` P ) Func E ) )
29 eqidd 
 |-  ( x e. ( F ( P Lan E ) X ) -> ( <. ( 2nd ` P ) , E >. -o.F F ) = ( <. ( 2nd ` P ) , E >. -o.F F ) )
30 21 22 27 28 29 lanval 
 |-  ( x e. ( F ( P Lan E ) X ) -> ( F ( <. ( 1st ` P ) , ( 2nd ` P ) >. Lan E ) X ) = ( ( <. ( 2nd ` P ) , E >. -o.F F ) ( ( ( 2nd ` P ) FuncCat E ) UP ( ( 1st ` P ) FuncCat E ) ) X ) )
31 20 30 eqtrd 
 |-  ( x e. ( F ( P Lan E ) X ) -> ( F ( P Lan E ) X ) = ( ( <. ( 2nd ` P ) , E >. -o.F F ) ( ( ( 2nd ` P ) FuncCat E ) UP ( ( 1st ` P ) FuncCat E ) ) X ) )
32 31 releqd 
 |-  ( x e. ( F ( P Lan E ) X ) -> ( Rel ( F ( P Lan E ) X ) <-> Rel ( ( <. ( 2nd ` P ) , E >. -o.F F ) ( ( ( 2nd ` P ) FuncCat E ) UP ( ( 1st ` P ) FuncCat E ) ) X ) ) )
33 5 32 mpbiri 
 |-  ( x e. ( F ( P Lan E ) X ) -> Rel ( F ( P Lan E ) X ) )
34 33 exlimiv 
 |-  ( E. x x e. ( F ( P Lan E ) X ) -> Rel ( F ( P Lan E ) X ) )
35 4 34 sylbi 
 |-  ( ( F ( P Lan E ) X ) =/= (/) -> Rel ( F ( P Lan E ) X ) )
36 3 35 pm2.61ine 
 |-  Rel ( F ( P Lan E ) X )