Theorem lanval2

Description: The set of left Kan extensions is the set of universal pairs. Therefore, the explicit universal property can be recovered by isup2 and upciclem1 . (Contributed by Zhi Wang, 3-Nov-2025)

	Ref	Expression
Hypotheses	islan.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
	islan.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
	islan.k	⊢ 𝐾 = ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 )
Assertion	lanval2	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ 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	4	adantl	⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑥 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) ) → 𝑥 ∈ ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) )
6		simpr	⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑥 ∈ ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) ) → 𝑥 ∈ ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) )
7		simpl	⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑥 ∈ ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
8	2	fucbas	⊢ ( 𝐶 Func 𝐸 ) = ( Base ‘ 𝑆 )
9	8	uprcl	⊢ ( 𝑥 ∈ ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) → ( 𝐾 ∈ ( 𝑅 Func 𝑆 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) )
10	9	simprd	⊢ ( 𝑥 ∈ ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) → 𝑋 ∈ ( 𝐶 Func 𝐸 ) )
11	10	adantl	⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑥 ∈ ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) ) → 𝑋 ∈ ( 𝐶 Func 𝐸 ) )
12	3	eqcomi	⊢ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = 𝐾
13	12	a1i	⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑥 ∈ ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = 𝐾 )
14	1 2 7 11 13	lanval	⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑥 ∈ ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) ) → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) = ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) )
15	6 14	eleqtrrd	⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑥 ∈ ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) ) → 𝑥 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) )
16	5 15	impbida	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝑥 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) ↔ 𝑥 ∈ ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) ) )
17	16	eqrdv	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) = ( 𝐾 ( 𝑅 UP 𝑆 ) 𝑋 ) )