Theorem lanrcl2

Description: Reverse closure for left Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		lanrcl2.l	⊢ ( 𝜑 → 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) 𝐴 )
2		df-br	⊢ ( 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) 𝐴 ↔ ⟨ 𝐿 , 𝐴 ⟩ ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) )
3	1 2	sylib	⊢ ( 𝜑 → ⟨ 𝐿 , 𝐴 ⟩ ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) )
4		lanrcl	⊢ ( ⟨ 𝐿 , 𝐴 ⟩ ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Lan 𝐸 ) 𝑋 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) )
5	3 4	syl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) )
6	5	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )