Theorem islan

Description: A left Kan extension is a universal pair. (Contributed by Zhi Wang, 3-Nov-2025)

	Ref	Expression
Hypotheses	islan.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
	islan.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
	islan.k	⊢ 𝐾 = ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 )
Assertion	islan	⊢ ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → 𝐿 ∈ ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		islan.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
2		islan.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
3		islan.k	⊢ 𝐾 = ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 )
4		id	⊢ ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) )
5		lanrcl	⊢ ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) )
6	5	simpld	⊢ ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
7	5	simprd	⊢ ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → 𝑋 ∈ ( 𝐶 Func 𝐸 ) )
8	3	eqcomi	⊢ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = 𝐾
9	8	a1i	⊢ ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = 𝐾 )
10	1 2 6 7 9	lanval	⊢ ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) = ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) )
11	4 10	eleqtrd	⊢ ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → 𝐿 ∈ ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) )