Metamath Proof Explorer

Theorem ranval3

Description: The set of right Kan extensions is the set of universal pairs. (Contributed by Zhi Wang, 26-Nov-2025)

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

Proof

Step Hyp Ref Expression
1 ranval3.o ⊢ 𝑂 = ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) )
2 ranval3.p ⊢ 𝑃 = ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) )
3 ranval3.k ⊢ 𝐾 = ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 )
4 id ⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5 opex ⊢ ⟨ 𝐷 , 𝐸 ⟩ ∈ V
6 5 a1i ⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ⟨ 𝐷 , 𝐸 ⟩ ∈ V )
7 4 6 prcofelvv ⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ∈ ( V × V ) )
8 1st2nd2 ⊢ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ∈ ( V × V ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ )
9 7 8 syl ⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ )
10 1 2 9 4 ranval2 ⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) = ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) )
11 eqid ⊢ ( 𝐶 FuncCat 𝐸 ) = ( 𝐶 FuncCat 𝐸 )
12 11 fucbas ⊢ ( 𝐶 Func 𝐸 ) = ( Base ‘ ( 𝐶 FuncCat 𝐸 ) )
13 2 12 oppcbas ⊢ ( 𝐶 Func 𝐸 ) = ( Base ‘ 𝑃 )
14 13 uprcl ⊢ ( 𝑥 ∈ ( ( oppFunc ‘ 𝐾 ) ( 𝑂 UP 𝑃 ) 𝑋 ) → ( ( oppFunc ‘ 𝐾 ) ∈ ( 𝑂 Func 𝑃 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) )
15 14 simprd ⊢ ( 𝑥 ∈ ( ( oppFunc ‘ 𝐾 ) ( 𝑂 UP 𝑃 ) 𝑋 ) → 𝑋 ∈ ( 𝐶 Func 𝐸 ) )
16 15 adantl ⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑥 ∈ ( ( oppFunc ‘ 𝐾 ) ( 𝑂 UP 𝑃 ) 𝑋 ) ) → 𝑋 ∈ ( 𝐶 Func 𝐸 ) )
17 13 uprcl ⊢ ( 𝑥 ∈ ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) → ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ∈ ( 𝑂 Func 𝑃 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) )
18 17 simprd ⊢ ( 𝑥 ∈ ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) → 𝑋 ∈ ( 𝐶 Func 𝐸 ) )
19 18 adantl ⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑥 ∈ ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) ) → 𝑋 ∈ ( 𝐶 Func 𝐸 ) )
20 eqid ⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
21 funcrcl ⊢ ( 𝑋 ∈ ( 𝐶 Func 𝐸 ) → ( 𝐶 ∈ Cat ∧ 𝐸 ∈ Cat ) )
22 21 simprd ⊢ ( 𝑋 ∈ ( 𝐶 Func 𝐸 ) → 𝐸 ∈ Cat )
23 22 adantl ⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) → 𝐸 ∈ Cat )
24 simpl ⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
25 20 23 11 24 prcoffunca ⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ∈ ( ( 𝐷 FuncCat 𝐸 ) Func ( 𝐶 FuncCat 𝐸 ) ) )
26 3 fveq2i ⊢ ( oppFunc ‘ 𝐾 ) = ( oppFunc ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) )
27 oppfval2 ⊢ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ∈ ( ( 𝐷 FuncCat 𝐸 ) Func ( 𝐶 FuncCat 𝐸 ) ) → ( oppFunc ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ )
28 26 27 eqtrid ⊢ ( ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ∈ ( ( 𝐷 FuncCat 𝐸 ) Func ( 𝐶 FuncCat 𝐸 ) ) → ( oppFunc ‘ 𝐾 ) = ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ )
29 25 28 syl ⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) → ( oppFunc ‘ 𝐾 ) = ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ )
30 29 oveq1d ⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) → ( ( oppFunc ‘ 𝐾 ) ( 𝑂 UP 𝑃 ) 𝑋 ) = ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) )
31 30 eleq2d ⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑋 ∈ ( 𝐶 Func 𝐸 ) ) → ( 𝑥 ∈ ( ( oppFunc ‘ 𝐾 ) ( 𝑂 UP 𝑃 ) 𝑋 ) ↔ 𝑥 ∈ ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) ) )
32 16 19 31 bibiad ⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝑥 ∈ ( ( oppFunc ‘ 𝐾 ) ( 𝑂 UP 𝑃 ) 𝑋 ) ↔ 𝑥 ∈ ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) ) )
33 32 eqrdv ⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( ( oppFunc ‘ 𝐾 ) ( 𝑂 UP 𝑃 ) 𝑋 ) = ( ⟨ ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) , tpos ( 2nd ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) ⟩ ( 𝑂 UP 𝑃 ) 𝑋 ) )
34 10 33 eqtr4d ⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐹 ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) 𝑋 ) = ( ( oppFunc ‘ 𝐾 ) ( 𝑂 UP 𝑃 ) 𝑋 ) )