Metamath Proof Explorer

Theorem fuco22natlem2

Description: Lemma for fuco22nat . The commutative square of natural transformation B in category E , combined with the commutative square of fuco22natlem1 . (Contributed by Zhi Wang, 30-Sep-2025)

Ref Expression
Hypotheses fuco22natlem1.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
fuco22natlem1.y ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
fuco22natlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
fuco22natlem1.h ⊢ ( 𝜑 → 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
fuco22natlem2.b ⊢ ( 𝜑 → 𝐵 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
Assertion fuco22natlem2 ( 𝜑 → ( ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( 𝐴 ‘ 𝑌 ) ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) = ( ( ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fuco22natlem1.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
2 fuco22natlem1.y ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
3 fuco22natlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
4 fuco22natlem1.h ⊢ ( 𝜑 → 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
5 fuco22natlem2.b ⊢ ( 𝜑 → 𝐵 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
6 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
7 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
8 eqid ⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
9 eqid ⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
10 9 5 natrcl2 ⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
11 10 funcrcl3 ⊢ ( 𝜑 → 𝐸 ∈ Cat )
12 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
13 12 6 10 funcf1 ⊢ ( 𝜑 → 𝐾 : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
14 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
15 eqid ⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
16 15 3 natrcl2 ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
17 14 12 16 funcf1 ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
18 17 1 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
19 13 18 ffvelcdmd ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐸 ) )
20 17 2 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) )
21 13 20 ffvelcdmd ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐸 ) )
22 15 3 natrcl3 ⊢ ( 𝜑 → 𝑀 ( 𝐶 Func 𝐷 ) 𝑁 )
23 14 12 22 funcf1 ⊢ ( 𝜑 → 𝑀 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
24 23 2 ffvelcdmd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) )
25 13 24 ffvelcdmd ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐸 ) )
26 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
27 12 26 7 10 18 20 funcf2 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) : ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ⟶ ( ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ) )
28 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
29 14 28 26 16 1 2 funcf2 ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) )
30 29 4 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ∈ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) )
31 27 30 ffvelcdmd ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ∈ ( ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ) )
32 12 26 7 10 20 24 funcf2 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) : ( ( 𝐹 ‘ 𝑌 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) ⟶ ( ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ( Hom ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) )
33 15 3 14 26 2 natcl ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑌 ) ∈ ( ( 𝐹 ‘ 𝑌 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) )
34 32 33 ffvelcdmd ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( 𝐴 ‘ 𝑌 ) ) ∈ ( ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ( Hom ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) )
35 9 5 natrcl3 ⊢ ( 𝜑 → 𝑅 ( 𝐷 Func 𝐸 ) 𝑆 )
36 12 6 35 funcf1 ⊢ ( 𝜑 → 𝑅 : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
37 36 24 ffvelcdmd ⊢ ( 𝜑 → ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐸 ) )
38 9 5 12 7 24 natcl ⊢ ( 𝜑 → ( 𝐵 ‘ ( 𝑀 ‘ 𝑌 ) ) ∈ ( ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ( Hom ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) )
39 6 7 8 11 19 21 25 31 34 37 38 catass ⊢ ( 𝜑 → ( ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( 𝐴 ‘ 𝑌 ) ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) = ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( ( 𝐹 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( 𝐴 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) ) )
40 1 2 3 4 10 fuco22natlem1 ⊢ ( 𝜑 → ( ( ( ( 𝐹 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( 𝐴 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) = ( ( ( ( 𝑀 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )
41 40 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( ( 𝐹 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( 𝐴 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) ) = ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( ( 𝑀 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) ) )
42 23 1 ffvelcdmd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
43 14 28 26 22 1 2 funcf2 ⊢ ( 𝜑 → ( 𝑋 𝑁 𝑌 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ⟶ ( ( 𝑀 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) )
44 43 4 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ∈ ( ( 𝑀 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) )
45 9 5 12 26 8 42 24 44 nati ⊢ ( 𝜑 → ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝑀 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ) = ( ( ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ) )
46 45 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝑀 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( ( ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) )
47 13 42 ffvelcdmd ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐸 ) )
48 12 26 7 10 18 42 funcf2 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) : ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑋 ) ) ⟶ ( ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ) )
49 15 3 14 26 1 natcl ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑋 ) ) )
50 48 49 ffvelcdmd ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ∈ ( ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ) )
51 12 26 7 10 42 24 funcf2 ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) : ( ( 𝑀 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) ⟶ ( ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) )
52 51 44 ffvelcdmd ⊢ ( 𝜑 → ( ( ( 𝑀 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ∈ ( ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) )
53 6 7 8 11 19 47 25 50 52 37 38 catass ⊢ ( 𝜑 → ( ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝑀 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( ( 𝑀 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) ) )
54 36 42 ffvelcdmd ⊢ ( 𝜑 → ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐸 ) )
55 9 5 12 7 42 natcl ⊢ ( 𝜑 → ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ∈ ( ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) )
56 12 26 7 35 42 24 funcf2 ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) : ( ( 𝑀 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑌 ) ) ⟶ ( ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) )
57 56 44 ffvelcdmd ⊢ ( 𝜑 → ( ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ∈ ( ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) )
58 6 7 8 11 19 47 54 50 55 37 57 catass ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) ) )
59 46 53 58 3eqtr3d ⊢ ( 𝜑 → ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( ( 𝑀 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) ) = ( ( ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) ) )
60 39 41 59 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑌 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑌 ) ) ‘ ( 𝐴 ‘ 𝑌 ) ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑌 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) = ( ( ( ( 𝑀 ‘ 𝑋 ) 𝑆 ( 𝑀 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐻 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑌 ) ) ) ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑋 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑋 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑋 ) ) ) ( ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝑀 ‘ 𝑋 ) ) ‘ ( 𝐴 ‘ 𝑋 ) ) ) ) )