Metamath Proof Explorer

Theorem prcofdiag

Description: A diagonal functor post-composed by a pre-composition functor is another diagonal functor. (Contributed by Zhi Wang, 25-Nov-2025)

Ref Expression
Hypotheses prcofdiag.l ⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
prcofdiag.m ⊢ 𝑀 = ( 𝐶 Δfunc 𝐸 )
prcofdiag.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐸 Func 𝐷 ) )
prcofdiag.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
prcofdiag.g ⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐶 ⟩ −∘F 𝐹 ) = 𝐺 )
Assertion prcofdiag ( 𝜑 → ( 𝐺 ∘func 𝐿 ) = 𝑀 )

Proof

Step Hyp Ref Expression
1 prcofdiag.l ⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
2 prcofdiag.m ⊢ 𝑀 = ( 𝐶 Δfunc 𝐸 )
3 prcofdiag.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐸 Func 𝐷 ) )
4 prcofdiag.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 prcofdiag.g ⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐶 ⟩ −∘F 𝐹 ) = 𝐺 )
6 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7 eqid ⊢ ( Base ‘ ( 𝐸 FuncCat 𝐶 ) ) = ( Base ‘ ( 𝐸 FuncCat 𝐶 ) )
8 3 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐸 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
9 8 funcrcl3 ⊢ ( 𝜑 → 𝐷 ∈ Cat )
10 eqid ⊢ ( 𝐷 FuncCat 𝐶 ) = ( 𝐷 FuncCat 𝐶 )
11 1 4 9 10 diagcl ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) )
12 eqid ⊢ ( 𝐸 FuncCat 𝐶 ) = ( 𝐸 FuncCat 𝐶 )
13 10 4 12 3 prcoffunca ⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐶 ⟩ −∘F 𝐹 ) ∈ ( ( 𝐷 FuncCat 𝐶 ) Func ( 𝐸 FuncCat 𝐶 ) ) )
14 5 13 eqeltrrd ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐷 FuncCat 𝐶 ) Func ( 𝐸 FuncCat 𝐶 ) ) )
15 11 14 cofucl ⊢ ( 𝜑 → ( 𝐺 ∘func 𝐿 ) ∈ ( 𝐶 Func ( 𝐸 FuncCat 𝐶 ) ) )
16 15 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ ( 𝐺 ∘func 𝐿 ) ) ( 𝐶 Func ( 𝐸 FuncCat 𝐶 ) ) ( 2nd ‘ ( 𝐺 ∘func 𝐿 ) ) )
17 6 7 16 funcf1 ⊢ ( 𝜑 → ( 1st ‘ ( 𝐺 ∘func 𝐿 ) ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ ( 𝐸 FuncCat 𝐶 ) ) )
18 17 ffnd ⊢ ( 𝜑 → ( 1st ‘ ( 𝐺 ∘func 𝐿 ) ) Fn ( Base ‘ 𝐶 ) )
19 8 funcrcl2 ⊢ ( 𝜑 → 𝐸 ∈ Cat )
20 2 4 19 12 diagcl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝐶 Func ( 𝐸 FuncCat 𝐶 ) ) )
21 20 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝑀 ) ( 𝐶 Func ( 𝐸 FuncCat 𝐶 ) ) ( 2nd ‘ 𝑀 ) )
22 6 7 21 funcf1 ⊢ ( 𝜑 → ( 1st ‘ 𝑀 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ ( 𝐸 FuncCat 𝐶 ) ) )
23 22 ffnd ⊢ ( 𝜑 → ( 1st ‘ 𝑀 ) Fn ( Base ‘ 𝐶 ) )
24 11 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐿 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) )
25 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐺 ∈ ( ( 𝐷 FuncCat 𝐶 ) Func ( 𝐸 FuncCat 𝐶 ) ) )
26 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
27 6 24 25 26 cofu1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ ( 𝐺 ∘func 𝐿 ) ) ‘ 𝑥 ) = ( ( 1st ‘ 𝐺 ) ‘ ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ) )
28 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
29 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
30 eqid ⊢ ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) = ( ( 1st ‘ 𝐿 ) ‘ 𝑥 )
31 1 28 29 6 26 30 diag1cl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ∈ ( 𝐷 Func 𝐶 ) )
32 5 fveq2d ⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐷 , 𝐶 ⟩ −∘F 𝐹 ) ) = ( 1st ‘ 𝐺 ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1st ‘ ( ⟨ 𝐷 , 𝐶 ⟩ −∘F 𝐹 ) ) = ( 1st ‘ 𝐺 ) )
34 31 33 prcof1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ 𝐺 ) ‘ ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ) = ( ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ∘func 𝐹 ) )
35 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐹 ∈ ( 𝐸 Func 𝐷 ) )
36 1 2 35 28 6 26 prcofdiag1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ∘func 𝐹 ) = ( ( 1st ‘ 𝑀 ) ‘ 𝑥 ) )
37 27 34 36 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1st ‘ ( 𝐺 ∘func 𝐿 ) ) ‘ 𝑥 ) = ( ( 1st ‘ 𝑀 ) ‘ 𝑥 ) )
38 18 23 37 eqfnfvd ⊢ ( 𝜑 → ( 1st ‘ ( 𝐺 ∘func 𝐿 ) ) = ( 1st ‘ 𝑀 ) )
39 6 16 funcfn2 ⊢ ( 𝜑 → ( 2nd ‘ ( 𝐺 ∘func 𝐿 ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
40 6 21 funcfn2 ⊢ ( 𝜑 → ( 2nd ‘ 𝑀 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
41 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
42 eqid ⊢ ( Hom ‘ ( 𝐸 FuncCat 𝐶 ) ) = ( Hom ‘ ( 𝐸 FuncCat 𝐶 ) )
43 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1st ‘ ( 𝐺 ∘func 𝐿 ) ) ( 𝐶 Func ( 𝐸 FuncCat 𝐶 ) ) ( 2nd ‘ ( 𝐺 ∘func 𝐿 ) ) )
44 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
45 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
46 6 41 42 43 44 45 funcf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ ( 𝐺 ∘func 𝐿 ) ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1st ‘ ( 𝐺 ∘func 𝐿 ) ) ‘ 𝑥 ) ( Hom ‘ ( 𝐸 FuncCat 𝐶 ) ) ( ( 1st ‘ ( 𝐺 ∘func 𝐿 ) ) ‘ 𝑦 ) ) )
47 46 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ ( 𝐺 ∘func 𝐿 ) ) 𝑦 ) Fn ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
48 21 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1st ‘ 𝑀 ) ( 𝐶 Func ( 𝐸 FuncCat 𝐶 ) ) ( 2nd ‘ 𝑀 ) )
49 6 41 42 48 44 45 funcf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ 𝑀 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1st ‘ 𝑀 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐸 FuncCat 𝐶 ) ) ( ( 1st ‘ 𝑀 ) ‘ 𝑦 ) ) )
50 49 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ 𝑀 ) 𝑦 ) Fn ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
51 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
52 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
53 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐹 ∈ ( 𝐸 Func 𝐷 ) )
54 53 func1st2nd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 1st ‘ 𝐹 ) ( 𝐸 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
55 51 52 54 funcf1 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 1st ‘ 𝐹 ) : ( Base ‘ 𝐸 ) ⟶ ( Base ‘ 𝐷 ) )
56 xpco2 ⊢ ( ( 1st ‘ 𝐹 ) : ( Base ‘ 𝐸 ) ⟶ ( Base ‘ 𝐷 ) → ( ( ( Base ‘ 𝐷 ) × { 𝑓 } ) ∘ ( 1st ‘ 𝐹 ) ) = ( ( Base ‘ 𝐸 ) × { 𝑓 } ) )
57 55 56 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( Base ‘ 𝐷 ) × { 𝑓 } ) ∘ ( 1st ‘ 𝐹 ) ) = ( ( Base ‘ 𝐸 ) × { 𝑓 } ) )
58 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐿 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) )
59 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐺 ∈ ( ( 𝐷 FuncCat 𝐶 ) Func ( 𝐸 FuncCat 𝐶 ) ) )
60 44 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
61 45 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
62 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
63 6 58 59 60 61 41 62 cofu2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2nd ‘ ( 𝐺 ∘func 𝐿 ) ) 𝑦 ) ‘ 𝑓 ) = ( ( ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐿 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2nd ‘ 𝐿 ) 𝑦 ) ‘ 𝑓 ) ) )
64 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐶 ∈ Cat )
65 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐷 ∈ Cat )
66 1 6 52 41 64 65 60 61 62 diag2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2nd ‘ 𝐿 ) 𝑦 ) ‘ 𝑓 ) = ( ( Base ‘ 𝐷 ) × { 𝑓 } ) )
67 66 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐿 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2nd ‘ 𝐿 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐿 ) ‘ 𝑦 ) ) ‘ ( ( Base ‘ 𝐷 ) × { 𝑓 } ) ) )
68 eqid ⊢ ( 𝐷 Nat 𝐶 ) = ( 𝐷 Nat 𝐶 )
69 1 6 52 41 64 65 60 61 62 68 diag2cl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( Base ‘ 𝐷 ) × { 𝑓 } ) ∈ ( ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ( 𝐷 Nat 𝐶 ) ( ( 1st ‘ 𝐿 ) ‘ 𝑦 ) ) )
70 5 fveq2d ⊢ ( 𝜑 → ( 2nd ‘ ( ⟨ 𝐷 , 𝐶 ⟩ −∘F 𝐹 ) ) = ( 2nd ‘ 𝐺 ) )
71 70 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 2nd ‘ ( ⟨ 𝐷 , 𝐶 ⟩ −∘F 𝐹 ) ) = ( 2nd ‘ 𝐺 ) )
72 68 69 71 53 prcof21a ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( ( 1st ‘ 𝐿 ) ‘ 𝑥 ) ( 2nd ‘ 𝐺 ) ( ( 1st ‘ 𝐿 ) ‘ 𝑦 ) ) ‘ ( ( Base ‘ 𝐷 ) × { 𝑓 } ) ) = ( ( ( Base ‘ 𝐷 ) × { 𝑓 } ) ∘ ( 1st ‘ 𝐹 ) ) )
73 63 67 72 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2nd ‘ ( 𝐺 ∘func 𝐿 ) ) 𝑦 ) ‘ 𝑓 ) = ( ( ( Base ‘ 𝐷 ) × { 𝑓 } ) ∘ ( 1st ‘ 𝐹 ) ) )
74 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐸 ∈ Cat )
75 2 6 51 41 64 74 60 61 62 diag2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2nd ‘ 𝑀 ) 𝑦 ) ‘ 𝑓 ) = ( ( Base ‘ 𝐸 ) × { 𝑓 } ) )
76 57 73 75 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2nd ‘ ( 𝐺 ∘func 𝐿 ) ) 𝑦 ) ‘ 𝑓 ) = ( ( 𝑥 ( 2nd ‘ 𝑀 ) 𝑦 ) ‘ 𝑓 ) )
77 47 50 76 eqfnfvd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2nd ‘ ( 𝐺 ∘func 𝐿 ) ) 𝑦 ) = ( 𝑥 ( 2nd ‘ 𝑀 ) 𝑦 ) )
78 39 40 77 eqfnovd ⊢ ( 𝜑 → ( 2nd ‘ ( 𝐺 ∘func 𝐿 ) ) = ( 2nd ‘ 𝑀 ) )
79 38 78 opeq12d ⊢ ( 𝜑 → ⟨ ( 1st ‘ ( 𝐺 ∘func 𝐿 ) ) , ( 2nd ‘ ( 𝐺 ∘func 𝐿 ) ) ⟩ = ⟨ ( 1st ‘ 𝑀 ) , ( 2nd ‘ 𝑀 ) ⟩ )
80 relfunc ⊢ Rel ( 𝐶 Func ( 𝐸 FuncCat 𝐶 ) )
81 1st2nd ⊢ ( ( Rel ( 𝐶 Func ( 𝐸 FuncCat 𝐶 ) ) ∧ ( 𝐺 ∘func 𝐿 ) ∈ ( 𝐶 Func ( 𝐸 FuncCat 𝐶 ) ) ) → ( 𝐺 ∘func 𝐿 ) = ⟨ ( 1st ‘ ( 𝐺 ∘func 𝐿 ) ) , ( 2nd ‘ ( 𝐺 ∘func 𝐿 ) ) ⟩ )
82 80 15 81 sylancr ⊢ ( 𝜑 → ( 𝐺 ∘func 𝐿 ) = ⟨ ( 1st ‘ ( 𝐺 ∘func 𝐿 ) ) , ( 2nd ‘ ( 𝐺 ∘func 𝐿 ) ) ⟩ )
83 1st2nd ⊢ ( ( Rel ( 𝐶 Func ( 𝐸 FuncCat 𝐶 ) ) ∧ 𝑀 ∈ ( 𝐶 Func ( 𝐸 FuncCat 𝐶 ) ) ) → 𝑀 = ⟨ ( 1st ‘ 𝑀 ) , ( 2nd ‘ 𝑀 ) ⟩ )
84 80 20 83 sylancr ⊢ ( 𝜑 → 𝑀 = ⟨ ( 1st ‘ 𝑀 ) , ( 2nd ‘ 𝑀 ) ⟩ )
85 79 82 84 3eqtr4d ⊢ ( 𝜑 → ( 𝐺 ∘func 𝐿 ) = 𝑀 )