Metamath Proof Explorer

Theorem lmdran

Description: To each limit of a diagram there is a corresponding right Kan extention of the diagram along a functor to a terminal category. The morphism parts coincide, while the object parts are one-to-one correspondent ( diag1f1o ). (Contributed by Zhi Wang, 26-Nov-2025)

Ref Expression
Hypotheses lmdran.1 
|- ( ph -> .1. e. TermCat )
lmdran.g 
|- ( ph -> G e. ( D Func .1. ) )
lmdran.l 
|- L = ( C DiagFunc .1. )
lmdran.y 
|- ( ph -> Y = ( ( 1st ` L ) ` X ) )
Assertion lmdran 
|- ( ph -> ( X ( ( C Limit D ) ` F ) M <-> Y ( G ( <. D , .1. >. Ran C ) F ) M ) )

Proof

Step Hyp Ref Expression
1 lmdran.1 
 |-  ( ph -> .1. e. TermCat )
2 lmdran.g 
 |-  ( ph -> G e. ( D Func .1. ) )
3 lmdran.l 
 |-  L = ( C DiagFunc .1. )
4 lmdran.y 
 |-  ( ph -> Y = ( ( 1st ` L ) ` X ) )
5 lmdfval2 
 |-  ( ( C Limit D ) ` F ) = ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F )
6 5 breqi 
 |-  ( X ( ( C Limit D ) ` F ) M <-> X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M )
7 simpr 
 |-  ( ( ph /\ X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M )
8 7 up1st2nd 
 |-  ( ( ph /\ X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> X ( <. ( 1st ` ( oppFunc ` ( C DiagFunc D ) ) ) , ( 2nd ` ( oppFunc ` ( C DiagFunc D ) ) ) >. ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M )
9 eqid 
 |-  ( oppCat ` ( D FuncCat C ) ) = ( oppCat ` ( D FuncCat C ) )
10 eqid 
 |-  ( D FuncCat C ) = ( D FuncCat C )
11 10 fucbas 
 |-  ( D Func C ) = ( Base ` ( D FuncCat C ) )
12 8 9 11 oppcuprcl3 
 |-  ( ( ph /\ X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> F e. ( D Func C ) )
13 eqid 
 |-  ( oppCat ` C ) = ( oppCat ` C )
14 eqid 
 |-  ( Base ` C ) = ( Base ` C )
15 8 13 14 oppcuprcl4 
 |-  ( ( ph /\ X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> X e. ( Base ` C ) )
16 12 15 jca 
 |-  ( ( ph /\ X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) )
17 simpr 
 |-  ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M )
18 17 up1st2nd 
 |-  ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> Y ( <. ( 1st ` ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ) , ( 2nd ` ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ) >. ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M )
19 18 9 11 oppcuprcl3 
 |-  ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> F e. ( D Func C ) )
20 4 adantr 
 |-  ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> Y = ( ( 1st ` L ) ` X ) )
21 eqid 
 |-  ( oppCat ` ( .1. FuncCat C ) ) = ( oppCat ` ( .1. FuncCat C ) )
22 eqid 
 |-  ( .1. FuncCat C ) = ( .1. FuncCat C )
23 22 fucbas 
 |-  ( .1. Func C ) = ( Base ` ( .1. FuncCat C ) )
24 18 21 23 oppcuprcl4 
 |-  ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> Y e. ( .1. Func C ) )
25 relfunc 
 |-  Rel ( .1. Func C )
26 24 25 oppfrcllem 
 |-  ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> Y =/= (/) )
27 20 26 eqnetrrd 
 |-  ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> ( ( 1st ` L ) ` X ) =/= (/) )
28 fvfundmfvn0 
 |-  ( ( ( 1st ` L ) ` X ) =/= (/) -> ( X e. dom ( 1st ` L ) /\ Fun ( ( 1st ` L ) |` { X } ) ) )
29 28 simpld 
 |-  ( ( ( 1st ` L ) ` X ) =/= (/) -> X e. dom ( 1st ` L ) )
30 27 29 syl 
 |-  ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> X e. dom ( 1st ` L ) )
31 1 adantr 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> .1. e. TermCat )
32 simpr 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> F e. ( D Func C ) )
33 32 func1st2nd 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> ( 1st ` F ) ( D Func C ) ( 2nd ` F ) )
34 33 funcrcl3 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> C e. Cat )
35 14 31 34 3 diag1f1o 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> ( 1st ` L ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) )
36 f1of 
 |-  ( ( 1st ` L ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) -> ( 1st ` L ) : ( Base ` C ) --> ( .1. Func C ) )
37 35 36 syl 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> ( 1st ` L ) : ( Base ` C ) --> ( .1. Func C ) )
38 37 fdmd 
 |-  ( ( ph /\ F e. ( D Func C ) ) -> dom ( 1st ` L ) = ( Base ` C ) )
39 19 38 syldan 
 |-  ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> dom ( 1st ` L ) = ( Base ` C ) )
40 30 39 eleqtrd 
 |-  ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> X e. ( Base ` C ) )
41 19 40 jca 
 |-  ( ( ph /\ Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) -> ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) )
42 13 14 oppcbas 
 |-  ( Base ` C ) = ( Base ` ( oppCat ` C ) )
43 21 23 oppcbas 
 |-  ( .1. Func C ) = ( Base ` ( oppCat ` ( .1. FuncCat C ) ) )
44 4 adantr 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> Y = ( ( 1st ` L ) ` X ) )
45 34 adantrr 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> C e. Cat )
46 1 adantr 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> .1. e. TermCat )
47 46 termccd 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> .1. e. Cat )
48 3 45 47 22 diagcl 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> L e. ( C Func ( .1. FuncCat C ) ) )
49 48 oppf1 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( 1st ` ( oppFunc ` L ) ) = ( 1st ` L ) )
50 49 fveq1d 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( ( 1st ` ( oppFunc ` L ) ) ` X ) = ( ( 1st ` L ) ` X ) )
51 44 50 eqtr4d 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> Y = ( ( 1st ` ( oppFunc ` L ) ) ` X ) )
52 eqid 
 |-  ( C DiagFunc D ) = ( C DiagFunc D )
53 2 adantr 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> G e. ( D Func .1. ) )
54 eqidd 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( <. .1. , C >. -o.F G ) = ( <. .1. , C >. -o.F G ) )
55 3 52 53 45 54 prcofdiag 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( ( <. .1. , C >. -o.F G ) o.func L ) = ( C DiagFunc D ) )
56 22 45 10 53 prcoffunca 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( <. .1. , C >. -o.F G ) e. ( ( .1. FuncCat C ) Func ( D FuncCat C ) ) )
57 55 48 56 cofuoppf 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) o.func ( oppFunc ` L ) ) = ( oppFunc ` ( C DiagFunc D ) ) )
58 simprr 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> X e. ( Base ` C ) )
59 21 9 56 oppfoppc2 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( oppFunc ` ( <. .1. , C >. -o.F G ) ) e. ( ( oppCat ` ( .1. FuncCat C ) ) Func ( oppCat ` ( D FuncCat C ) ) ) )
60 45 46 22 3 diagffth 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> L e. ( ( C Full ( .1. FuncCat C ) ) i^i ( C Faith ( .1. FuncCat C ) ) ) )
61 13 21 60 ffthoppf 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( oppFunc ` L ) e. ( ( ( oppCat ` C ) Full ( oppCat ` ( .1. FuncCat C ) ) ) i^i ( ( oppCat ` C ) Faith ( oppCat ` ( .1. FuncCat C ) ) ) ) )
62 35 adantrr 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( 1st ` L ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) )
63 49 f1oeq1d 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( ( 1st ` ( oppFunc ` L ) ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) <-> ( 1st ` L ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) ) )
64 62 63 mpbird 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( 1st ` ( oppFunc ` L ) ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) )
65 f1ofo 
 |-  ( ( 1st ` ( oppFunc ` L ) ) : ( Base ` C ) -1-1-onto-> ( .1. Func C ) -> ( 1st ` ( oppFunc ` L ) ) : ( Base ` C ) -onto-> ( .1. Func C ) )
66 64 65 syl 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( 1st ` ( oppFunc ` L ) ) : ( Base ` C ) -onto-> ( .1. Func C ) )
67 42 43 51 57 58 59 61 66 uptr2a 
 |-  ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M <-> Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) )
68 16 41 67 bibiad 
 |-  ( ph -> ( X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M <-> Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) )
69 eqid 
 |-  ( <. .1. , C >. -o.F G ) = ( <. .1. , C >. -o.F G )
70 21 9 69 ranval3 
 |-  ( G e. ( D Func .1. ) -> ( G ( <. D , .1. >. Ran C ) F ) = ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) )
71 2 70 syl 
 |-  ( ph -> ( G ( <. D , .1. >. Ran C ) F ) = ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) )
72 71 breqd 
 |-  ( ph -> ( Y ( G ( <. D , .1. >. Ran C ) F ) M <-> Y ( ( oppFunc ` ( <. .1. , C >. -o.F G ) ) ( ( oppCat ` ( .1. FuncCat C ) ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M ) )
73 68 72 bitr4d 
 |-  ( ph -> ( X ( ( oppFunc ` ( C DiagFunc D ) ) ( ( oppCat ` C ) UP ( oppCat ` ( D FuncCat C ) ) ) F ) M <-> Y ( G ( <. D , .1. >. Ran C ) F ) M ) )
74 6 73 bitrid 
 |-  ( ph -> ( X ( ( C Limit D ) ` F ) M <-> Y ( G ( <. D , .1. >. Ran C ) F ) M ) )