Metamath Proof Explorer

Theorem fuco22natlem

Description: The composed natural transformation is a natural transformation. Use fuco22nat instead. (New usage is discouraged.) (Contributed by Zhi Wang, 30-Sep-2025)

Ref Expression
Hypotheses fuco22natlem.o ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
fuco22natlem.a ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
fuco22natlem.b ⊢ ( 𝜑 → 𝐵 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
fuco22natlem.u ⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
fuco22natlem.v ⊢ ( 𝜑 → 𝑉 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
Assertion fuco22natlem ( 𝜑 → ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ∈ ( ( 𝑂 ‘ 𝑈 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 fuco22natlem.o ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2 fuco22natlem.a ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
3 fuco22natlem.b ⊢ ( 𝜑 → 𝐵 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
4 fuco22natlem.u ⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
5 fuco22natlem.v ⊢ ( 𝜑 → 𝑉 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
6 eqid ⊢ ( 𝐶 Nat 𝐸 ) = ( 𝐶 Nat 𝐸 )
7 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
8 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
10 eqid ⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
11 eqid ⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
12 11 2 natrcl2 ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
13 eqid ⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
14 13 3 natrcl2 ⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
15 1 12 14 4 7 fuco11a ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑈 ) = ⟨ ( 𝐾 ∘ 𝐹 ) , ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑧 𝐺 𝑤 ) ) ) ⟩ )
16 1 12 14 4 fuco11cl ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑈 ) ∈ ( 𝐶 Func 𝐸 ) )
17 15 16 eqeltrrd ⊢ ( 𝜑 → ⟨ ( 𝐾 ∘ 𝐹 ) , ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑧 𝐺 𝑤 ) ) ) ⟩ ∈ ( 𝐶 Func 𝐸 ) )
18 df-br ⊢ ( ( 𝐾 ∘ 𝐹 ) ( 𝐶 Func 𝐸 ) ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑧 𝐺 𝑤 ) ) ) ↔ ⟨ ( 𝐾 ∘ 𝐹 ) , ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑧 𝐺 𝑤 ) ) ) ⟩ ∈ ( 𝐶 Func 𝐸 ) )
19 17 18 sylibr ⊢ ( 𝜑 → ( 𝐾 ∘ 𝐹 ) ( 𝐶 Func 𝐸 ) ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑧 𝐺 𝑤 ) ) ) )
20 11 2 natrcl3 ⊢ ( 𝜑 → 𝑀 ( 𝐶 Func 𝐷 ) 𝑁 )
21 13 3 natrcl3 ⊢ ( 𝜑 → 𝑅 ( 𝐷 Func 𝐸 ) 𝑆 )
22 1 20 21 5 7 fuco11a ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑉 ) = ⟨ ( 𝑅 ∘ 𝑀 ) , ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑧 𝑁 𝑤 ) ) ) ⟩ )
23 1 20 21 5 fuco11cl ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑉 ) ∈ ( 𝐶 Func 𝐸 ) )
24 22 23 eqeltrrd ⊢ ( 𝜑 → ⟨ ( 𝑅 ∘ 𝑀 ) , ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑧 𝑁 𝑤 ) ) ) ⟩ ∈ ( 𝐶 Func 𝐸 ) )
25 df-br ⊢ ( ( 𝑅 ∘ 𝑀 ) ( 𝐶 Func 𝐸 ) ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑧 𝑁 𝑤 ) ) ) ↔ ⟨ ( 𝑅 ∘ 𝑀 ) , ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑧 𝑁 𝑤 ) ) ) ⟩ ∈ ( 𝐶 Func 𝐸 ) )
26 24 25 sylibr ⊢ ( 𝜑 → ( 𝑅 ∘ 𝑀 ) ( 𝐶 Func 𝐸 ) ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑧 𝑁 𝑤 ) ) ) )
27 1 4 5 2 3 fucofn22 ⊢ ( 𝜑 → ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) Fn ( Base ‘ 𝐶 ) )
28 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
29 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
30 29 funcrcl3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐸 ∈ Cat )
31 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
32 31 28 29 funcf1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐾 : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
33 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
34 7 31 33 funcf1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
35 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
36 34 35 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
37 32 36 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐸 ) )
38 20 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑀 ( 𝐶 Func 𝐷 ) 𝑁 )
39 7 31 38 funcf1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑀 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
40 39 35 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑀 ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
41 32 40 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐸 ) )
42 21 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑅 ( 𝐷 Func 𝐸 ) 𝑆 )
43 31 28 42 funcf1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑅 : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
44 43 40 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐸 ) )
45 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
46 31 45 9 29 36 40 funcf2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) : ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑥 ) ) ⟶ ( ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ) )
47 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
48 11 47 7 45 35 natcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐴 ‘ 𝑥 ) ∈ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑀 ‘ 𝑥 ) ) )
49 46 48 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ∈ ( ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ) )
50 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐵 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
51 7 31 20 funcf1 ⊢ ( 𝜑 → 𝑀 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
52 51 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑀 ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
53 13 50 31 9 52 natcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐵 ‘ ( 𝑀 ‘ 𝑥 ) ) ∈ ( ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) )
54 28 9 10 30 37 41 44 49 53 catcocl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) ∈ ( ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) )
55 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
56 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
57 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑉 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
58 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) = ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) )
59 55 56 57 47 50 35 58 fuco23 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑥 ) = ( ( 𝐵 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) )
60 34 35 fvco3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) )
61 39 35 fvco3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑥 ) = ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) )
62 60 61 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑥 ) ) = ( ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) )
63 54 59 62 3eltr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑥 ) ∈ ( ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑥 ) ) )
64 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
65 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
66 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
67 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
68 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐵 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
69 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
70 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
71 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑉 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
72 64 65 66 67 68 69 70 71 fuco22natlem3 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑦 ) ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑦 ) ) ( ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ‘ ℎ ) ) = ( ( ( ( ( 𝑀 ‘ 𝑥 ) 𝑆 ( 𝑀 ‘ 𝑦 ) ) ∘ ( 𝑥 𝑁 𝑦 ) ) ‘ ℎ ) ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑦 ) ) ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑥 ) ) )
73 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
74 73 oveq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) )
75 oveq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝐺 𝑤 ) = ( 𝑥 𝐺 𝑤 ) )
76 74 75 coeq12d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑧 𝐺 𝑤 ) ) = ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑥 𝐺 𝑤 ) ) )
77 fveq2 ⊢ ( 𝑤 = 𝑦 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) )
78 77 oveq2d ⊢ ( 𝑤 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) )
79 oveq2 ⊢ ( 𝑤 = 𝑦 → ( 𝑥 𝐺 𝑤 ) = ( 𝑥 𝐺 𝑦 ) )
80 78 79 coeq12d ⊢ ( 𝑤 = 𝑦 → ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑥 𝐺 𝑤 ) ) = ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) )
81 eqid ⊢ ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑧 𝐺 𝑤 ) ) ) = ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑧 𝐺 𝑤 ) ) )
82 ovex ⊢ ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∈ V
83 ovex ⊢ ( 𝑥 𝐺 𝑦 ) ∈ V
84 82 83 coex ⊢ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ∈ V
85 76 80 81 84 ovmpo ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑧 𝐺 𝑤 ) ) ) 𝑦 ) = ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) )
86 85 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝑥 ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑧 𝐺 𝑤 ) ) ) 𝑦 ) = ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) )
87 86 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑧 𝐺 𝑤 ) ) ) 𝑦 ) ‘ ℎ ) = ( ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ‘ ℎ ) )
88 87 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑦 ) ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑧 𝐺 𝑤 ) ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑦 ) ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑦 ) ) ( ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ‘ ℎ ) ) )
89 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑀 ‘ 𝑧 ) = ( 𝑀 ‘ 𝑥 ) )
90 89 oveq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) = ( ( 𝑀 ‘ 𝑥 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) )
91 oveq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝑁 𝑤 ) = ( 𝑥 𝑁 𝑤 ) )
92 90 91 coeq12d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑧 𝑁 𝑤 ) ) = ( ( ( 𝑀 ‘ 𝑥 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑥 𝑁 𝑤 ) ) )
93 fveq2 ⊢ ( 𝑤 = 𝑦 → ( 𝑀 ‘ 𝑤 ) = ( 𝑀 ‘ 𝑦 ) )
94 93 oveq2d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑀 ‘ 𝑥 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) = ( ( 𝑀 ‘ 𝑥 ) 𝑆 ( 𝑀 ‘ 𝑦 ) ) )
95 oveq2 ⊢ ( 𝑤 = 𝑦 → ( 𝑥 𝑁 𝑤 ) = ( 𝑥 𝑁 𝑦 ) )
96 94 95 coeq12d ⊢ ( 𝑤 = 𝑦 → ( ( ( 𝑀 ‘ 𝑥 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑥 𝑁 𝑤 ) ) = ( ( ( 𝑀 ‘ 𝑥 ) 𝑆 ( 𝑀 ‘ 𝑦 ) ) ∘ ( 𝑥 𝑁 𝑦 ) ) )
97 eqid ⊢ ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑧 𝑁 𝑤 ) ) ) = ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑧 𝑁 𝑤 ) ) )
98 ovex ⊢ ( ( 𝑀 ‘ 𝑥 ) 𝑆 ( 𝑀 ‘ 𝑦 ) ) ∈ V
99 ovex ⊢ ( 𝑥 𝑁 𝑦 ) ∈ V
100 98 99 coex ⊢ ( ( ( 𝑀 ‘ 𝑥 ) 𝑆 ( 𝑀 ‘ 𝑦 ) ) ∘ ( 𝑥 𝑁 𝑦 ) ) ∈ V
101 92 96 97 100 ovmpo ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑧 𝑁 𝑤 ) ) ) 𝑦 ) = ( ( ( 𝑀 ‘ 𝑥 ) 𝑆 ( 𝑀 ‘ 𝑦 ) ) ∘ ( 𝑥 𝑁 𝑦 ) ) )
102 101 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝑥 ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑧 𝑁 𝑤 ) ) ) 𝑦 ) = ( ( ( 𝑀 ‘ 𝑥 ) 𝑆 ( 𝑀 ‘ 𝑦 ) ) ∘ ( 𝑥 𝑁 𝑦 ) ) )
103 102 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑧 𝑁 𝑤 ) ) ) 𝑦 ) ‘ ℎ ) = ( ( ( ( 𝑀 ‘ 𝑥 ) 𝑆 ( 𝑀 ‘ 𝑦 ) ) ∘ ( 𝑥 𝑁 𝑦 ) ) ‘ ℎ ) )
104 103 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( 𝑥 ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑧 𝑁 𝑤 ) ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑦 ) ) ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑥 ) ) = ( ( ( ( ( 𝑀 ‘ 𝑥 ) 𝑆 ( 𝑀 ‘ 𝑦 ) ) ∘ ( 𝑥 𝑁 𝑦 ) ) ‘ ℎ ) ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑦 ) ) ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑥 ) ) )
105 72 88 104 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑦 ) ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑧 𝐺 𝑤 ) ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑧 𝑁 𝑤 ) ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐸 ) ( ( 𝑅 ∘ 𝑀 ) ‘ 𝑦 ) ) ( ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ‘ 𝑥 ) ) )
106 6 7 8 9 10 19 26 27 63 105 isnatd ⊢ ( 𝜑 → ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ∈ ( ⟨ ( 𝐾 ∘ 𝐹 ) , ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑧 𝐺 𝑤 ) ) ) ⟩ ( 𝐶 Nat 𝐸 ) ⟨ ( 𝑅 ∘ 𝑀 ) , ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑧 𝑁 𝑤 ) ) ) ⟩ ) )
107 15 22 oveq12d ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑈 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑉 ) ) = ( ⟨ ( 𝐾 ∘ 𝐹 ) , ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ∘ ( 𝑧 𝐺 𝑤 ) ) ) ⟩ ( 𝐶 Nat 𝐸 ) ⟨ ( 𝑅 ∘ 𝑀 ) , ( 𝑧 ∈ ( Base ‘ 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( 𝑀 ‘ 𝑧 ) 𝑆 ( 𝑀 ‘ 𝑤 ) ) ∘ ( 𝑧 𝑁 𝑤 ) ) ) ⟩ ) )
108 106 107 eleqtrrd ⊢ ( 𝜑 → ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ∈ ( ( 𝑂 ‘ 𝑈 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑉 ) ) )