Theorem isran

Description: A right Kan extension is a universal pair. (Contributed by Zhi Wang, 4-Nov-2025)

	Ref	Expression
Hypotheses	isran.o	⊢ 𝑂 = ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) )
	isran.p	⊢ 𝑃 = ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) )
	isran.k	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ 𝐽 , 𝐾 ⟩ )
	isran.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) )
Assertion	isran	⊢ ( 𝜑 → 𝐿 ∈ ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		isran.o	⊢ 𝑂 = ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) )
2		isran.p	⊢ 𝑃 = ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) )
3		isran.k	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ 𝐽 , 𝐾 ⟩ )
4		isran.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) )
5		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
6		eqid	⊢ ( 𝐶 FuncCat 𝐸 ) = ( 𝐶 FuncCat 𝐸 )
7		ranrcl	⊢ ( 𝐿 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) )
8	4 7	syl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) )
9	8	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
10	8	simprd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 Func 𝐸 ) )
11	5 6 9 10 3 1 2	ranval	⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) = ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) )
12	4 11	eleqtrd	⊢ ( 𝜑 → 𝐿 ∈ ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) )