Theorem islan2

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

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

Proof

Step	Hyp	Ref	Expression
1		islan.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
2		islan.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
3		islan.k	⊢ 𝐾 = ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 )
4	1 2 3	islan	⊢ ( ⟨ 𝐿 , 𝐴 ⟩ ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → ⟨ 𝐿 , 𝐴 ⟩ ∈ ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) )
5		df-br	⊢ ( 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) 𝐴 ↔ ⟨ 𝐿 , 𝐴 ⟩ ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) )
6		df-br	⊢ ( 𝐿 ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) 𝐴 ↔ ⟨ 𝐿 , 𝐴 ⟩ ∈ ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) )
7	4 5 6	3imtr4i	⊢ ( 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) 𝐴 → 𝐿 ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) 𝐴 )