Theorem ranrcl5

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

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

Proof

Step	Hyp	Ref	Expression
1		ranrcl2.l	⊢ ( 𝜑 → 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) 𝐴 )
2		ranrcl5.n	⊢ 𝑁 = ( 𝐶 Nat 𝐸 )
3		eqid	⊢ ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) ) = ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) )
4		eqid	⊢ ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) ) = ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) )
5	1	ranrcl4lem	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ )
6	3 4 5 1	isran2	⊢ ( 𝜑 → 𝐿 ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) ) UP ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) ) ) 𝑋 ) 𝐴 )
7		eqid	⊢ ( 𝐶 FuncCat 𝐸 ) = ( 𝐶 FuncCat 𝐸 )
8	7 2	fuchom	⊢ 𝑁 = ( Hom ‘ ( 𝐶 FuncCat 𝐸 ) )
9	6 4 8	oppcuprcl5	⊢ ( 𝜑 → 𝐴 ∈ ( ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) 𝑁 𝑋 ) )
10	1	ranrcl4	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐷 Func 𝐸 ) )
11		eqidd	⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) )
12	10 11	prcof1	⊢ ( 𝜑 → ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) = ( 𝐿 ∘func 𝐹 ) )
13	12	oveq1d	⊢ ( 𝜑 → ( ( ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ‘ 𝐿 ) 𝑁 𝑋 ) = ( ( 𝐿 ∘func 𝐹 ) 𝑁 𝑋 ) )
14	9 13	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝐿 ∘func 𝐹 ) 𝑁 𝑋 ) )