Metamath Proof Explorer

Theorem ranfval

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

Ref Expression
Hypotheses lanfval.r ⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
lanfval.s ⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
lanfval.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
lanfval.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
lanfval.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
ranfval.o ⊢ 𝑂 = ( oppCat ‘ 𝑅 )
ranfval.p ⊢ 𝑃 = ( oppCat ‘ 𝑆 )
Assertion ranfval ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ) ( 𝑂 UP 𝑃 ) 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 lanfval.r ⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
2 lanfval.s ⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
3 lanfval.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
4 lanfval.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
5 lanfval.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
6 ranfval.o ⊢ 𝑂 = ( oppCat ‘ 𝑅 )
7 ranfval.p ⊢ 𝑃 = ( oppCat ‘ 𝑆 )
8 df-ran ⊢ Ran = ( 𝑝 ∈ ( V × V ) , 𝑒 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) ) )
9 8 a1i ⊢ ( 𝜑 → Ran = ( 𝑝 ∈ ( V × V ) , 𝑒 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) ) ) )
10 fvexd ⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) → ( 1st ‘ 𝑝 ) ∈ V )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) → 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ )
12 11 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) → ( 1st ‘ 𝑝 ) = ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
13 op1stg ⊢ ( ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
14 3 4 13 syl2anc ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
15 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) → ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
16 12 15 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) → ( 1st ‘ 𝑝 ) = 𝐶 )
17 fvexd ⊢ ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → ( 2nd ‘ 𝑝 ) ∈ V )
18 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ )
19 18 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → ( 2nd ‘ 𝑝 ) = ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
20 op2ndg ⊢ ( ( 𝐶 ∈ 𝑈 ∧ 𝐷 ∈ 𝑉 ) → ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
21 3 4 20 syl2anc ⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
22 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
23 19 22 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → ( 2nd ‘ 𝑝 ) = 𝐷 )
24 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑐 = 𝐶 )
25 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
26 24 25 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑐 Func 𝑑 ) = ( 𝐶 Func 𝐷 ) )
27 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) )
28 27 simprd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑒 = 𝐸 )
29 24 28 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑐 Func 𝑒 ) = ( 𝐶 Func 𝐸 ) )
30 25 28 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑑 FuncCat 𝑒 ) = ( 𝐷 FuncCat 𝐸 ) )
31 30 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) = ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) ) )
32 1 fveq2i ⊢ ( oppCat ‘ 𝑅 ) = ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) )
33 6 32 eqtri ⊢ 𝑂 = ( oppCat ‘ ( 𝐷 FuncCat 𝐸 ) )
34 31 33 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) = 𝑂 )
35 24 28 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑐 FuncCat 𝑒 ) = ( 𝐶 FuncCat 𝐸 ) )
36 35 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) = ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) ) )
37 2 fveq2i ⊢ ( oppCat ‘ 𝑆 ) = ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) )
38 7 37 eqtri ⊢ 𝑃 = ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) )
39 36 38 eqtr4di ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) = 𝑃 )
40 34 39 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) = ( 𝑂 UP 𝑃 ) )
41 25 28 opeq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ⟨ 𝑑 , 𝑒 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ )
42 41 fvoveq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) = ( oppFunc ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ) )
43 eqidd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑥 = 𝑥 )
44 40 42 43 oveq123d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) = ( ( oppFunc ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ) ( 𝑂 UP 𝑃 ) 𝑥 ) )
45 26 29 44 mpoeq123dv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ) ( 𝑂 UP 𝑃 ) 𝑥 ) ) )
46 17 23 45 csbied2 ⊢ ( ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → ⦋ ( 2nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ) ( 𝑂 UP 𝑃 ) 𝑥 ) ) )
47 10 16 46 csbied2 ⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑒 = 𝐸 ) ) → ⦋ ( 1st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑑 ⦌ ( 𝑓 ∈ ( 𝑐 Func 𝑑 ) , 𝑥 ∈ ( 𝑐 Func 𝑒 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝑑 , 𝑒 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝑑 FuncCat 𝑒 ) ) UP ( oppCat ‘ ( 𝑐 FuncCat 𝑒 ) ) ) 𝑥 ) ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ) ( 𝑂 UP 𝑃 ) 𝑥 ) ) )
48 3 elexd ⊢ ( 𝜑 → 𝐶 ∈ V )
49 4 elexd ⊢ ( 𝜑 → 𝐷 ∈ V )
50 48 49 opelxpd ⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( V × V ) )
51 5 elexd ⊢ ( 𝜑 → 𝐸 ∈ V )
52 ovex ⊢ ( 𝐶 Func 𝐷 ) ∈ V
53 ovex ⊢ ( 𝐶 Func 𝐸 ) ∈ V
54 52 53 mpoex ⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ) ( 𝑂 UP 𝑃 ) 𝑥 ) ) ∈ V
55 54 a1i ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ) ( 𝑂 UP 𝑃 ) 𝑥 ) ) ∈ V )
56 9 47 50 51 55 ovmpod ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ Ran 𝐸 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) , 𝑥 ∈ ( 𝐶 Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝑓 ) ) ( 𝑂 UP 𝑃 ) 𝑥 ) ) )