Theorem isran2

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 𝐹 ) = ⟨ 𝐽 , 𝐾 ⟩ )
	isran2.l	⊢ ( 𝜑 → 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) 𝐴 )
Assertion	isran2	⊢ ( 𝜑 → 𝐿 ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		isran.o	⊢ 𝑂 = ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) )
2		isran.p	⊢ 𝑃 = ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) )
3		isran.k	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ 𝐽 , 𝐾 ⟩ )
4		isran2.l	⊢ ( 𝜑 → 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) 𝐴 )
5		df-br	⊢ ( 𝐿 ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) 𝐴 ↔ ⟨ 𝐿 , 𝐴 ⟩ ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) )
6	4 5	sylib	⊢ ( 𝜑 → ⟨ 𝐿 , 𝐴 ⟩ ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) )
7	1 2 3 6	isran	⊢ ( 𝜑 → ⟨ 𝐿 , 𝐴 ⟩ ∈ ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) )
8		df-br	⊢ ( 𝐿 ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) 𝐴 ↔ ⟨ 𝐿 , 𝐴 ⟩ ∈ ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) )
9	7 8	sylibr	⊢ ( 𝜑 → 𝐿 ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) 𝐴 )