Theorem lanrcl5

Description: The second component of a left Kan extension is a natural transformation. (Contributed by Zhi Wang, 4-Nov-2025)

	Ref	Expression
Hypotheses	lanrcl2.l	⊢ ( 𝜑 → 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) 𝐴 )
	lanrcl5.n	⊢ 𝑁 = ( 𝐶 Nat 𝐸 )
Assertion	lanrcl5	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝑁 ( 𝐿 ∘func 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lanrcl2.l	⊢ ( 𝜑 → 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) 𝐴 )
2		lanrcl5.n	⊢ 𝑁 = ( 𝐶 Nat 𝐸 )
3		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
4		eqid	⊢ ( 𝐶 FuncCat 𝐸 ) = ( 𝐶 FuncCat 𝐸 )
5		eqid	⊢ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 )
6	3 4 5	islan2	⊢ ( 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) 𝐴 → 𝐿 ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑋 ) 𝐴 )
7	1 6	syl	⊢ ( 𝜑 → 𝐿 ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑋 ) 𝐴 )
8	7	up1st2nd	⊢ ( 𝜑 → 𝐿 ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑋 ) 𝐴 )
9	4 2	fuchom	⊢ 𝑁 = ( Hom ‘ ( 𝐶 FuncCat 𝐸 ) )
10	8 9	uprcl5	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝑁 ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ) )
11	1	lanrcl4	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐷 Func 𝐸 ) )
12		eqidd	⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) )
13	11 12	prcof1	⊢ ( 𝜑 → ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) = ( 𝐿 ∘func 𝐹 ) )
14	13	oveq2d	⊢ ( 𝜑 → ( 𝑋 𝑁 ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) ) = ( 𝑋 𝑁 ( 𝐿 ∘func 𝐹 ) ) )
15	10 14	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝑁 ( 𝐿 ∘func 𝐹 ) ) )