Metamath Proof Explorer

Theorem ranval

Description: Value of the set of right Kan extensions. (Contributed by Zhi Wang, 4-Nov-2025)

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

Proof

Step Hyp Ref Expression
1 lanval.r ⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
2 lanval.s ⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
3 lanval.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
4 lanval.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 Func 𝐸 ) )
5 ranval.k ⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ 𝐽 , 𝐾 ⟩ )
6 ranval.o ⊢ 𝑂 = ( oppCat ‘ 𝑅 )
7 ranval.p ⊢ 𝑃 = ( oppCat ‘ 𝑆 )
8 3 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
9 8 funcrcl2 ⊢ ( 𝜑 → 𝐶 ∈ Cat )
10 8 funcrcl3 ⊢ ( 𝜑 → 𝐷 ∈ Cat )
11 4 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝑋 ) ( 𝐶 Func 𝐸 ) ( 2nd ‘ 𝑋 ) )
12 11 funcrcl3 ⊢ ( 𝜑 → 𝐸 ∈ Cat )
13 1 2 9 10 12 6 7 ranfval ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ) ( 𝑂 UP 𝑃 ) 𝑥 ) ) )
14 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → 𝑓 = 𝐹 )
15 14 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) = ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) )
16 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ 𝐽 , 𝐾 ⟩ )
17 15 16 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) = ⟨ 𝐽 , 𝐾 ⟩ )
18 17 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( oppFunc ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ) = ( oppFunc ‘ ⟨ 𝐽 , 𝐾 ⟩ ) )
19 df-ov ⊢ ( 𝐽 oppFunc 𝐾 ) = ( oppFunc ‘ ⟨ 𝐽 , 𝐾 ⟩ )
20 1 12 2 3 5 prcoffunca2 ⊢ ( 𝜑 → 𝐽 ( 𝑅 Func 𝑆 ) 𝐾 )
21 oppfval ⊢ ( 𝐽 ( 𝑅 Func 𝑆 ) 𝐾 → ( 𝐽 oppFunc 𝐾 ) = ⟨ 𝐽 , tpos 𝐾 ⟩ )
22 20 21 syl ⊢ ( 𝜑 → ( 𝐽 oppFunc 𝐾 ) = ⟨ 𝐽 , tpos 𝐾 ⟩ )
23 19 22 eqtr3id ⊢ ( 𝜑 → ( oppFunc ‘ ⟨ 𝐽 , 𝐾 ⟩ ) = ⟨ 𝐽 , tpos 𝐾 ⟩ )
24 23 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( oppFunc ‘ ⟨ 𝐽 , 𝐾 ⟩ ) = ⟨ 𝐽 , tpos 𝐾 ⟩ )
25 18 24 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( oppFunc ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ) = ⟨ 𝐽 , tpos 𝐾 ⟩ )
26 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → 𝑥 = 𝑋 )
27 25 26 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑋 ) ) → ( ( oppFunc ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ) ( 𝑂 UP 𝑃 ) 𝑥 ) = ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) )
28 ovexd ⊢ ( 𝜑 → ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) ∈ V )
29 13 27 3 4 28 ovmpod ⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) = ( ⟨ 𝐽 , tpos 𝐾 ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) )