Theorem ranrcl3

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

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

Proof

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