Theorem cmdlan

Description: To each colimit of a diagram there is a corresponding left 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	No typesetting found for |- ( ph -> .1. e. TermCat ) with typecode |-
	lmdran.g	$$⊢\phi \to G\in \left(D\mathrm{Func}\underset{\dot{}}{1}\right)$$
	lmdran.l	$$⊢L=C{\Delta }_{\mathrm{func}}\underset{\dot{}}{1}$$
	lmdran.y	$$⊢\phi \to Y=1^{st}\left(L\right)\left(X\right)$$
Assertion	cmdlan	Could not format assertion : No typesetting found for |- ( ph -> ( X ( ( C Colimit D ) ` F ) M <-> Y ( G ( <. D , .1. >. Lan C ) F ) M ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		lmdran.1	Could not format ( ph -> .1. e. TermCat ) : No typesetting found for |- ( ph -> .1. e. TermCat ) with typecode |-
2		lmdran.g	$$⊢\phi \to G\in \left(D\mathrm{Func}\underset{\dot{}}{1}\right)$$
3		lmdran.l	$$⊢L=C{\Delta }_{\mathrm{func}}\underset{\dot{}}{1}$$
4		lmdran.y	$$⊢\phi \to Y=1^{st}\left(L\right)\left(X\right)$$
5		cmdfval2	Could not format ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) : No typesetting found for |- ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) with typecode |-
6	5	breqi	Could not format ( X ( ( C Colimit D ) ` F ) M <-> X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) : No typesetting found for |- ( X ( ( C Colimit D ) ` F ) M <-> X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) with typecode |-
7		simpr	Could not format ( ( ph /\ X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) -> X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) : No typesetting found for |- ( ( ph /\ X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) -> X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) with typecode |-
8	7	up1st2nd	Could not format ( ( ph /\ X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) -> X ( <. ( 1st ` ( C DiagFunc D ) ) , ( 2nd ` ( C DiagFunc D ) ) >. ( C UP ( D FuncCat C ) ) F ) M ) : No typesetting found for |- ( ( ph /\ X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) -> X ( <. ( 1st ` ( C DiagFunc D ) ) , ( 2nd ` ( C DiagFunc D ) ) >. ( C UP ( D FuncCat C ) ) F ) M ) with typecode |-
9		eqid	$$⊢D\mathrm{FuncCat}C=D\mathrm{FuncCat}C$$
10	9	fucbas	$$⊢D\mathrm{Func}C={\mathrm{Base}}_{\left(D\mathrm{FuncCat}C\right)}$$
11	8 10	uprcl3	Could not format ( ( ph /\ X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) -> F e. ( D Func C ) ) : No typesetting found for |- ( ( ph /\ X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) -> F e. ( D Func C ) ) with typecode |-
12		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
13	8 12	uprcl4	Could not format ( ( ph /\ X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) -> X e. ( Base ` C ) ) : No typesetting found for |- ( ( ph /\ X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) -> X e. ( Base ` C ) ) with typecode |-
14	11 13	jca	Could not format ( ( ph /\ X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) -> ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) : No typesetting found for |- ( ( ph /\ X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M ) -> ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) with typecode |-
15		simpr	Could not format ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) : No typesetting found for |- ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) with typecode |-
16	15	up1st2nd	Could not format ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> Y ( <. ( 1st ` ( <. .1. , C >. -o.F G ) ) , ( 2nd ` ( <. .1. , C >. -o.F G ) ) >. ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) : No typesetting found for |- ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> Y ( <. ( 1st ` ( <. .1. , C >. -o.F G ) ) , ( 2nd ` ( <. .1. , C >. -o.F G ) ) >. ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) with typecode |-
17	16 10	uprcl3	Could not format ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> F e. ( D Func C ) ) : No typesetting found for |- ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> F e. ( D Func C ) ) with typecode |-
18	4	adantr	Could not format ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> Y = ( ( 1st ` L ) ` X ) ) : No typesetting found for |- ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> Y = ( ( 1st ` L ) ` X ) ) with typecode |-
19		eqid	$$⊢\underset{\dot{}}{1}\mathrm{FuncCat}C=\underset{\dot{}}{1}\mathrm{FuncCat}C$$
20	19	fucbas	$$⊢\underset{\dot{}}{1}\mathrm{Func}C={\mathrm{Base}}_{\left(\underset{\dot{}}{1}\mathrm{FuncCat}C\right)}$$
21	16 20	uprcl4	Could not format ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> Y e. ( .1. Func C ) ) : No typesetting found for |- ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> Y e. ( .1. Func C ) ) with typecode |-
22		relfunc	$$⊢\mathrm{Rel}\left(\underset{\dot{}}{1}\mathrm{Func}C\right)$$
23	21 22	oppfrcllem	Could not format ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> Y =/= (/) ) : No typesetting found for |- ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> Y =/= (/) ) with typecode |-
24	18 23	eqnetrrd	Could not format ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> ( ( 1st ` L ) ` X ) =/= (/) ) : No typesetting found for |- ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> ( ( 1st ` L ) ` X ) =/= (/) ) with typecode |-
25		fvfundmfvn0	$$⊢1^{st}\left(L\right)\left(X\right)\ne \varnothing \to \left(X\in \mathrm{dom}{1}^{st}\left(L\right)\wedge \mathrm{Fun}\left({1^{st}\left(L\right)\upharpoonright }_{\left\{X\right\}}\right)\right)$$
26	25	simpld	$$⊢1^{st}\left(L\right)\left(X\right)\ne \varnothing \to X\in \mathrm{dom}{1}^{st}\left(L\right)$$
27	24 26	syl	Could not format ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> X e. dom ( 1st ` L ) ) : No typesetting found for |- ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> X e. dom ( 1st ` L ) ) with typecode |-
28	1	adantr	Could not format ( ( ph /\ F e. ( D Func C ) ) -> .1. e. TermCat ) : No typesetting found for |- ( ( ph /\ F e. ( D Func C ) ) -> .1. e. TermCat ) with typecode |-
29		simpr	$$⊢\left(\phi \wedge F\in \left(D\mathrm{Func}C\right)\right)\to F\in \left(D\mathrm{Func}C\right)$$
30	29	func1st2nd	$$⊢\left(\phi \wedge F\in \left(D\mathrm{Func}C\right)\right)\to 1^{st}\left(F\right)\left(D\mathrm{Func}C\right)2^{nd}\left(F\right)$$
31	30	funcrcl3	$$⊢\left(\phi \wedge F\in \left(D\mathrm{Func}C\right)\right)\to C\in \mathrm{Cat}$$
32	12 28 31 3	diag1f1o	$$⊢\left(\phi \wedge F\in \left(D\mathrm{Func}C\right)\right)\to 1^{st}\left(L\right):{\mathrm{Base}}_C\underset{1-1\; onto}{⟶}\underset{\dot{}}{1}\mathrm{Func}C$$
33		f1of	$$⊢1^{st}\left(L\right):{\mathrm{Base}}_C\underset{1-1\; onto}{⟶}\underset{\dot{}}{1}\mathrm{Func}C\to 1^{st}\left(L\right):{\mathrm{Base}}_C⟶\underset{\dot{}}{1}\mathrm{Func}C$$
34	32 33	syl	$$⊢\left(\phi \wedge F\in \left(D\mathrm{Func}C\right)\right)\to 1^{st}\left(L\right):{\mathrm{Base}}_C⟶\underset{\dot{}}{1}\mathrm{Func}C$$
35	34	fdmd	$$⊢\left(\phi \wedge F\in \left(D\mathrm{Func}C\right)\right)\to \mathrm{dom}{1}^{st}\left(L\right)={\mathrm{Base}}_C$$
36	17 35	syldan	Could not format ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> dom ( 1st ` L ) = ( Base ` C ) ) : No typesetting found for |- ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> dom ( 1st ` L ) = ( Base ` C ) ) with typecode |-
37	27 36	eleqtrd	Could not format ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> X e. ( Base ` C ) ) : No typesetting found for |- ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> X e. ( Base ` C ) ) with typecode |-
38	17 37	jca	Could not format ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) : No typesetting found for |- ( ( ph /\ Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) -> ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) with typecode |-
39	4	adantr	$$⊢\left(\phi \wedge \left(F\in \left(D\mathrm{Func}C\right)\wedge X\in {\mathrm{Base}}_C\right)\right)\to Y=1^{st}\left(L\right)\left(X\right)$$
40		eqid	$$⊢C{\Delta }_{\mathrm{func}}D=C{\Delta }_{\mathrm{func}}D$$
41	2	adantr	$$⊢\left(\phi \wedge \left(F\in \left(D\mathrm{Func}C\right)\wedge X\in {\mathrm{Base}}_C\right)\right)\to G\in \left(D\mathrm{Func}\underset{\dot{}}{1}\right)$$
42	31	adantrr	$$⊢\left(\phi \wedge \left(F\in \left(D\mathrm{Func}C\right)\wedge X\in {\mathrm{Base}}_C\right)\right)\to C\in \mathrm{Cat}$$
43		eqidd	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( <. .1. , C >. -o.F G ) = ( <. .1. , C >. -o.F G ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( <. .1. , C >. -o.F G ) = ( <. .1. , C >. -o.F G ) ) with typecode |-
44	3 40 41 42 43	prcofdiag	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( ( <. .1. , C >. -o.F G ) o.func L ) = ( C DiagFunc D ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( ( <. .1. , C >. -o.F G ) o.func L ) = ( C DiagFunc D ) ) with typecode |-
45		simprr	$$⊢\left(\phi \wedge \left(F\in \left(D\mathrm{Func}C\right)\wedge X\in {\mathrm{Base}}_C\right)\right)\to X\in {\mathrm{Base}}_C$$
46	19 42 9 41	prcoffunca	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( <. .1. , C >. -o.F G ) e. ( ( .1. FuncCat C ) Func ( D FuncCat C ) ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( <. .1. , C >. -o.F G ) e. ( ( .1. FuncCat C ) Func ( D FuncCat C ) ) ) with typecode |-
47	31 28 19 3	diagffth	$$⊢\left(\phi \wedge F\in \left(D\mathrm{Func}C\right)\right)\to L\in \left(\left(C\mathrm{Full}\left(\underset{\dot{}}{1}\mathrm{FuncCat}C\right)\right)\cap \left(C\mathrm{Faith}\left(\underset{\dot{}}{1}\mathrm{FuncCat}C\right)\right)\right)$$
48	47	adantrr	$$⊢\left(\phi \wedge \left(F\in \left(D\mathrm{Func}C\right)\wedge X\in {\mathrm{Base}}_C\right)\right)\to L\in \left(\left(C\mathrm{Full}\left(\underset{\dot{}}{1}\mathrm{FuncCat}C\right)\right)\cap \left(C\mathrm{Faith}\left(\underset{\dot{}}{1}\mathrm{FuncCat}C\right)\right)\right)$$
49		f1ofo	$$⊢1^{st}\left(L\right):{\mathrm{Base}}_C\underset{1-1\; onto}{⟶}\underset{\dot{}}{1}\mathrm{Func}C\to 1^{st}\left(L\right):{\mathrm{Base}}_C\underset{onto}{⟶}\underset{\dot{}}{1}\mathrm{Func}C$$
50	32 49	syl	$$⊢\left(\phi \wedge F\in \left(D\mathrm{Func}C\right)\right)\to 1^{st}\left(L\right):{\mathrm{Base}}_C\underset{onto}{⟶}\underset{\dot{}}{1}\mathrm{Func}C$$
51	50	adantrr	$$⊢\left(\phi \wedge \left(F\in \left(D\mathrm{Func}C\right)\wedge X\in {\mathrm{Base}}_C\right)\right)\to 1^{st}\left(L\right):{\mathrm{Base}}_C\underset{onto}{⟶}\underset{\dot{}}{1}\mathrm{Func}C$$
52	12 20 39 44 45 46 48 51	uptr2a	Could not format ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M <-> Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) ) : No typesetting found for |- ( ( ph /\ ( F e. ( D Func C ) /\ X e. ( Base ` C ) ) ) -> ( X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M <-> Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) ) with typecode |-
53	14 38 52	bibiad	Could not format ( ph -> ( X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M <-> Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) ) : No typesetting found for |- ( ph -> ( X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M <-> Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) ) with typecode |-
54		eqid	Could not format ( <. .1. , C >. -o.F G ) = ( <. .1. , C >. -o.F G ) : No typesetting found for |- ( <. .1. , C >. -o.F G ) = ( <. .1. , C >. -o.F G ) with typecode |-
55	19 9 54	lanval2	Could not format ( G e. ( D Func .1. ) -> ( G ( <. D , .1. >. Lan C ) F ) = ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) ) : No typesetting found for |- ( G e. ( D Func .1. ) -> ( G ( <. D , .1. >. Lan C ) F ) = ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) ) with typecode |-
56	2 55	syl	Could not format ( ph -> ( G ( <. D , .1. >. Lan C ) F ) = ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) ) : No typesetting found for |- ( ph -> ( G ( <. D , .1. >. Lan C ) F ) = ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) ) with typecode |-
57	56	breqd	Could not format ( ph -> ( Y ( G ( <. D , .1. >. Lan C ) F ) M <-> Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) ) : No typesetting found for |- ( ph -> ( Y ( G ( <. D , .1. >. Lan C ) F ) M <-> Y ( ( <. .1. , C >. -o.F G ) ( ( .1. FuncCat C ) UP ( D FuncCat C ) ) F ) M ) ) with typecode |-
58	53 57	bitr4d	Could not format ( ph -> ( X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M <-> Y ( G ( <. D , .1. >. Lan C ) F ) M ) ) : No typesetting found for |- ( ph -> ( X ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) M <-> Y ( G ( <. D , .1. >. Lan C ) F ) M ) ) with typecode |-
59	6 58	bitrid	Could not format ( ph -> ( X ( ( C Colimit D ) ` F ) M <-> Y ( G ( <. D , .1. >. Lan C ) F ) M ) ) : No typesetting found for |- ( ph -> ( X ( ( C Colimit D ) ` F ) M <-> Y ( G ( <. D , .1. >. Lan C ) F ) M ) ) with typecode |-