Metamath Proof Explorer

Theorem lmdran

Description: To each limit of a diagram there is a corresponding right Kan extention of the diagram along a functor to a terminal category. The morphism parts coincide, while the object parts are one-to-one correspondent ( diag1f1o ). (Contributed by Zhi Wang, 26-Nov-2025)

Ref Expression
Hypotheses lmdran.1 ⊢ ( 𝜑 → 1 ∈ TermCat )
lmdran.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 1 ) )
lmdran.l ⊢ 𝐿 = ( 𝐶 Δfunc 1 )
lmdran.y ⊢ ( 𝜑 → 𝑌 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) )
Assertion lmdran ( 𝜑 → ( 𝑋 ( ( 𝐶 Limit 𝐷 ) ‘ 𝐹 ) 𝑀 ↔ 𝑌 ( 𝐺 ( ⟨ 𝐷 , 1 ⟩ Ran 𝐶 ) 𝐹 ) 𝑀 ) )

Proof

Step Hyp Ref Expression
1 lmdran.1 ⊢ ( 𝜑 → 1 ∈ TermCat )
2 lmdran.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 1 ) )
3 lmdran.l ⊢ 𝐿 = ( 𝐶 Δfunc 1 )
4 lmdran.y ⊢ ( 𝜑 → 𝑌 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) )
5 lmdfval2 ⊢ ( ( 𝐶 Limit 𝐷 ) ‘ 𝐹 ) = ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 )
6 5 breqi ⊢ ( 𝑋 ( ( 𝐶 Limit 𝐷 ) ‘ 𝐹 ) 𝑀 ↔ 𝑋 ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → 𝑋 ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 )
8 7 up1st2nd ⊢ ( ( 𝜑 ∧ 𝑋 ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → 𝑋 ( ⟨ ( 1st ‘ ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ) , ( 2nd ‘ ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ) ⟩ ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 )
9 eqid ⊢ ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) = ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) )
10 eqid ⊢ ( 𝐷 FuncCat 𝐶 ) = ( 𝐷 FuncCat 𝐶 )
11 10 fucbas ⊢ ( 𝐷 Func 𝐶 ) = ( Base ‘ ( 𝐷 FuncCat 𝐶 ) )
12 8 9 11 oppcuprcl3 ⊢ ( ( 𝜑 ∧ 𝑋 ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
13 eqid ⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
14 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
15 8 13 14 oppcuprcl4 ⊢ ( ( 𝜑 ∧ 𝑋 ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
16 12 15 jca ⊢ ( ( 𝜑 ∧ 𝑋 ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑌 ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → 𝑌 ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 )
18 17 up1st2nd ⊢ ( ( 𝜑 ∧ 𝑌 ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → 𝑌 ( ⟨ ( 1st ‘ ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ) , ( 2nd ‘ ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ) ⟩ ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 )
19 18 9 11 oppcuprcl3 ⊢ ( ( 𝜑 ∧ 𝑌 ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
20 4 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → 𝑌 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) )
21 eqid ⊢ ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) = ( oppCat ‘ ( 1 FuncCat 𝐶 ) )
22 eqid ⊢ ( 1 FuncCat 𝐶 ) = ( 1 FuncCat 𝐶 )
23 22 fucbas ⊢ ( 1 Func 𝐶 ) = ( Base ‘ ( 1 FuncCat 𝐶 ) )
24 18 21 23 oppcuprcl4 ⊢ ( ( 𝜑 ∧ 𝑌 ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → 𝑌 ∈ ( 1 Func 𝐶 ) )
25 relfunc ⊢ Rel ( 1 Func 𝐶 )
26 24 25 oppfrcllem ⊢ ( ( 𝜑 ∧ 𝑌 ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → 𝑌 ≠ ∅ )
27 20 26 eqnetrrd ⊢ ( ( 𝜑 ∧ 𝑌 ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) ≠ ∅ )
28 fvfundmfvn0 ⊢ ( ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) ≠ ∅ → ( 𝑋 ∈ dom ( 1st ‘ 𝐿 ) ∧ Fun ( ( 1st ‘ 𝐿 ) ↾ { 𝑋 } ) ) )
29 28 simpld ⊢ ( ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) ≠ ∅ → 𝑋 ∈ dom ( 1st ‘ 𝐿 ) )
30 27 29 syl ⊢ ( ( 𝜑 ∧ 𝑌 ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → 𝑋 ∈ dom ( 1st ‘ 𝐿 ) )
31 1 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → 1 ∈ TermCat )
32 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
33 32 func1st2nd ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → ( 1st ‘ 𝐹 ) ( 𝐷 Func 𝐶 ) ( 2nd ‘ 𝐹 ) )
34 33 funcrcl3 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → 𝐶 ∈ Cat )
35 14 31 34 3 diag1f1o ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( 1 Func 𝐶 ) )
36 f1of ⊢ ( ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( 1 Func 𝐶 ) → ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) ⟶ ( 1 Func 𝐶 ) )
37 35 36 syl ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) ⟶ ( 1 Func 𝐶 ) )
38 37 fdmd ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝐷 Func 𝐶 ) ) → dom ( 1st ‘ 𝐿 ) = ( Base ‘ 𝐶 ) )
39 19 38 syldan ⊢ ( ( 𝜑 ∧ 𝑌 ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → dom ( 1st ‘ 𝐿 ) = ( Base ‘ 𝐶 ) )
40 30 39 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑌 ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
41 19 40 jca ⊢ ( ( 𝜑 ∧ 𝑌 ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) → ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) )
42 13 14 oppcbas ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ ( oppCat ‘ 𝐶 ) )
43 21 23 oppcbas ⊢ ( 1 Func 𝐶 ) = ( Base ‘ ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) )
44 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑌 = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) )
45 34 adantrr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
46 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → 1 ∈ TermCat )
47 46 termccd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → 1 ∈ Cat )
48 3 45 47 22 diagcl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐿 ∈ ( 𝐶 Func ( 1 FuncCat 𝐶 ) ) )
49 48 oppf1 ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1st ‘ ( oppFunc ‘ 𝐿 ) ) = ( 1st ‘ 𝐿 ) )
50 49 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑋 ) = ( ( 1st ‘ 𝐿 ) ‘ 𝑋 ) )
51 44 50 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑌 = ( ( 1st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑋 ) )
52 eqid ⊢ ( 𝐶 Δfunc 𝐷 ) = ( 𝐶 Δfunc 𝐷 )
53 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐺 ∈ ( 𝐷 Func 1 ) )
54 eqidd ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) = ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) )
55 3 52 53 45 54 prcofdiag ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ∘func 𝐿 ) = ( 𝐶 Δfunc 𝐷 ) )
56 22 45 10 53 prcoffunca ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ∈ ( ( 1 FuncCat 𝐶 ) Func ( 𝐷 FuncCat 𝐶 ) ) )
57 55 48 56 cofuoppf ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ∘func ( oppFunc ‘ 𝐿 ) ) = ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) )
58 simprr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
59 21 9 56 oppfoppc2 ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ∈ ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) Func ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) )
60 45 46 22 3 diagffth ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐿 ∈ ( ( 𝐶 Full ( 1 FuncCat 𝐶 ) ) ∩ ( 𝐶 Faith ( 1 FuncCat 𝐶 ) ) ) )
61 13 21 60 ffthoppf ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( oppFunc ‘ 𝐿 ) ∈ ( ( ( oppCat ‘ 𝐶 ) Full ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) ) ∩ ( ( oppCat ‘ 𝐶 ) Faith ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) ) ) )
62 35 adantrr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( 1 Func 𝐶 ) )
63 49 f1oeq1d ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1st ‘ ( oppFunc ‘ 𝐿 ) ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( 1 Func 𝐶 ) ↔ ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( 1 Func 𝐶 ) ) )
64 62 63 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1st ‘ ( oppFunc ‘ 𝐿 ) ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( 1 Func 𝐶 ) )
65 f1ofo ⊢ ( ( 1st ‘ ( oppFunc ‘ 𝐿 ) ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( 1 Func 𝐶 ) → ( 1st ‘ ( oppFunc ‘ 𝐿 ) ) : ( Base ‘ 𝐶 ) –onto→ ( 1 Func 𝐶 ) )
66 64 65 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1st ‘ ( oppFunc ‘ 𝐿 ) ) : ( Base ‘ 𝐶 ) –onto→ ( 1 Func 𝐶 ) )
67 42 43 51 57 58 59 61 66 uptr2a ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) ∧ 𝑋 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑋 ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ↔ 𝑌 ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) )
68 16 41 67 bibiad ⊢ ( 𝜑 → ( 𝑋 ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ↔ 𝑌 ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) )
69 eqid ⊢ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) = ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 )
70 21 9 69 ranval3 ⊢ ( 𝐺 ∈ ( 𝐷 Func 1 ) → ( 𝐺 ( ⟨ 𝐷 , 1 ⟩ Ran 𝐶 ) 𝐹 ) = ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) )
71 2 70 syl ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝐷 , 1 ⟩ Ran 𝐶 ) 𝐹 ) = ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) )
72 71 breqd ⊢ ( 𝜑 → ( 𝑌 ( 𝐺 ( ⟨ 𝐷 , 1 ⟩ Ran 𝐶 ) 𝐹 ) 𝑀 ↔ 𝑌 ( ( oppFunc ‘ ( ⟨ 1 , 𝐶 ⟩ −∘F 𝐺 ) ) ( ( oppCat ‘ ( 1 FuncCat 𝐶 ) ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ) )
73 68 72 bitr4d ⊢ ( 𝜑 → ( 𝑋 ( ( oppFunc ‘ ( 𝐶 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐶 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) 𝐹 ) 𝑀 ↔ 𝑌 ( 𝐺 ( ⟨ 𝐷 , 1 ⟩ Ran 𝐶 ) 𝐹 ) 𝑀 ) )
74 6 73 bitrid ⊢ ( 𝜑 → ( 𝑋 ( ( 𝐶 Limit 𝐷 ) ‘ 𝐹 ) 𝑀 ↔ 𝑌 ( 𝐺 ( ⟨ 𝐷 , 1 ⟩ Ran 𝐶 ) 𝐹 ) 𝑀 ) )