Metamath Proof Explorer

Theorem ranval2

Description: The set of right Kan extensions is the set of universal pairs. Therefore, the explicit universal property can be recovered by oppcup2 and oppcup3lem . (Contributed by Zhi Wang, 4-Nov-2025)

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

Proof

Step Hyp Ref Expression
1 isran.o ⊢ 𝑂 = ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) )
2 isran.p ⊢ 𝑃 = ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) )
3 isran.k ⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ 𝐽 , 𝐾 ⟩ )
4 ranval2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ 𝐽 , 𝐾 ⟩ )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) ) → 𝑥 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) )
7 1 2 5 6 isran ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) ) → 𝑥 ∈ ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) ) → 𝑥 ∈ ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) )
9 eqid ⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
10 eqid ⊢ ( 𝐶 FuncCat 𝐸 ) = ( 𝐶 FuncCat 𝐸 )
11 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
12 10 fucbas ⊢ ( 𝐶 Func 𝐸 ) = ( Base ‘ ( 𝐶 FuncCat 𝐸 ) )
13 2 12 oppcbas ⊢ ( 𝐶 Func 𝐸 ) = ( Base ‘ 𝑃 )
14 13 uprcl ⊢ ( 𝑥 ∈ ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) → ( ⟨ 𝐽 , tpos 𝐾 ⟩ ∈ ( 𝑂 Func 𝑃 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) )
15 14 simprd ⊢ ( 𝑥 ∈ ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) → 𝑋 ∈ ( 𝐶 Func 𝐸 ) )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) ) → 𝑋 ∈ ( 𝐶 Func 𝐸 ) )
17 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ 𝐽 , 𝐾 ⟩ )
18 9 10 11 16 17 1 2 ranval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) ) → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) = ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) )
19 8 18 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) ) → 𝑥 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) )
20 7 19 impbida ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) ↔ 𝑥 ∈ ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) ) )
21 20 eqrdv ⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) = ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) )