Metamath Proof Explorer

Theorem lanval

Description: Value of the set of left Kan extensions. (Contributed by Zhi Wang, 3-Nov-2025)

		Ref	Expression
	Hypotheses	lanval.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
		lanval.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
		lanval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
		lanval.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 Func 𝐸 ) )
		lanval.k	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝐹 ) = 𝐾 )
	Assertion	lanval	⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) = ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		lanval.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
2		lanval.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
3		lanval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
4		lanval.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 Func 𝐸 ) )
5		lanval.k	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝐹 ) = 𝐾 )
6	3	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
7	6	funcrcl2	⊢ ( 𝜑 → 𝐶 ∈ Cat )
8	6	funcrcl3	⊢ ( 𝜑 → 𝐷 ∈ Cat )
9	4	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝑋 ) ( 𝐶 Func 𝐸 ) ( 2^nd ‘ 𝑋 ) )
10	9	funcrcl3	⊢ ( 𝜑 → 𝐸 ∈ Cat )
11	1 2 7 8 10	lanfval	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝑓 ) ( 𝑅 UP 𝑆 ) 𝑥 ) ) )
12		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → 𝑓 = 𝐹 )
13	12	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝑓 ) = ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝐹 ) )
14	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝐹 ) = 𝐾 )
15	13 14	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝑓 ) = 𝐾 )
16		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → 𝑥 = 𝑋 )
17	15 16	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘_F 𝑓 ) ( 𝑅 UP 𝑆 ) 𝑥 ) = ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) )
18		ovexd	⊢ ( 𝜑 → ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) ∈ V )
19	11 17 3 4 18	ovmpod	⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) = ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) )