Theorem lanrcl4

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

	Ref	Expression
Hypothesis	lanrcl2.l	⊢ ( 𝜑 → 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) 𝐴 )
Assertion	lanrcl4	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐷 Func 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		lanrcl2.l	⊢ ( 𝜑 → 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) 𝐴 )
2		df-br	⊢ ( 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) 𝐴 ↔ ⟨ 𝐿 , 𝐴 ⟩ ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) )
3	1 2	sylib	⊢ ( 𝜑 → ⟨ 𝐿 , 𝐴 ⟩ ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) )
4		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
5		eqid	⊢ ( 𝐶 FuncCat 𝐸 ) = ( 𝐶 FuncCat 𝐸 )
6		eqid	⊢ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 )
7	4 5 6	islan	⊢ ( ⟨ 𝐿 , 𝐴 ⟩ ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → ⟨ 𝐿 , 𝐴 ⟩ ∈ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑋 ) )
8	3 7	syl	⊢ ( 𝜑 → ⟨ 𝐿 , 𝐴 ⟩ ∈ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑋 ) )
9		df-br	⊢ ( 𝐿 ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑋 ) 𝐴 ↔ ⟨ 𝐿 , 𝐴 ⟩ ∈ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑋 ) )
10	8 9	sylibr	⊢ ( 𝜑 → 𝐿 ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑋 ) 𝐴 )
11	10	up1st2nd	⊢ ( 𝜑 → 𝐿 ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( ( 𝐷 FuncCat 𝐸 ) UP ( 𝐶 FuncCat 𝐸 ) ) 𝑋 ) 𝐴 )
12	4	fucbas	⊢ ( 𝐷 Func 𝐸 ) = ( Base ‘ ( 𝐷 FuncCat 𝐸 ) )
13	11 12	uprcl4	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐷 Func 𝐸 ) )