Metamath Proof Explorer

Theorem fucoid

Description: Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also fucoid2 . (Contributed by Zhi Wang, 30-Sep-2025)

Ref Expression
Hypotheses fucoid.o ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
fucoid.t ⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐷 ) )
fucoid.1 ⊢ 1 = ( Id ‘ 𝑇 )
fucoid.q ⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
fucoid.i ⊢ 𝐼 = ( Id ‘ 𝑄 )
fucoid.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
fucoid.k ⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
fucoid.u ⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
Assertion fucoid ( 𝜑 → ( ( 𝑈 𝑃 𝑈 ) ‘ ( 1 ‘ 𝑈 ) ) = ( 𝐼 ‘ ( 𝑂 ‘ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 fucoid.o ⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2 fucoid.t ⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐷 ) )
3 fucoid.1 ⊢ 1 = ( Id ‘ 𝑇 )
4 fucoid.q ⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
5 fucoid.i ⊢ 𝐼 = ( Id ‘ 𝑄 )
6 fucoid.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
7 fucoid.k ⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
8 fucoid.u ⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
9 ovex ⊢ ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑥 ) ) ) ∈ V
10 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑥 ) ) ) )
11 9 10 fnmpti ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑥 ) ) ) ) Fn ( Base ‘ 𝐶 )
12 11 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑥 ) ) ) ) Fn ( Base ‘ 𝐶 ) )
13 7 funcrcl3 ⊢ ( 𝜑 → 𝐸 ∈ Cat )
14 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
15 eqid ⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
16 14 15 cidfn ⊢ ( 𝐸 ∈ Cat → ( Id ‘ 𝐸 ) Fn ( Base ‘ 𝐸 ) )
17 13 16 syl ⊢ ( 𝜑 → ( Id ‘ 𝐸 ) Fn ( Base ‘ 𝐸 ) )
18 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
19 18 14 7 funcf1 ⊢ ( 𝜑 → 𝐾 : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
20 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
21 20 18 6 funcf1 ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
22 19 21 fcod ⊢ ( 𝜑 → ( 𝐾 ∘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐸 ) )
23 fnfco ⊢ ( ( ( Id ‘ 𝐸 ) Fn ( Base ‘ 𝐸 ) ∧ ( 𝐾 ∘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐸 ) ) → ( ( Id ‘ 𝐸 ) ∘ ( 𝐾 ∘ 𝐹 ) ) Fn ( Base ‘ 𝐶 ) )
24 17 22 23 syl2anc ⊢ ( 𝜑 → ( ( Id ‘ 𝐸 ) ∘ ( 𝐾 ∘ 𝐹 ) ) Fn ( Base ‘ 𝐶 ) )
25 2fveq3 ⊢ ( 𝑥 = 𝑤 → ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) )
26 25 25 opeq12d ⊢ ( 𝑥 = 𝑤 → ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ = ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ⟩ )
27 26 25 oveq12d ⊢ ( 𝑥 = 𝑤 → ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) )
28 2fveq3 ⊢ ( 𝑥 = 𝑤 → ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑤 ) ) )
29 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
30 29 29 oveq12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑤 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) )
31 fveq2 ⊢ ( 𝑥 = 𝑤 → ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑤 ) )
32 30 31 fveq12d ⊢ ( 𝑥 = 𝑤 → ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑥 ) ) = ( ( ( 𝐹 ‘ 𝑤 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑤 ) ) )
33 27 28 32 oveq123d ⊢ ( 𝑥 = 𝑤 → ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑥 ) ) ) = ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑤 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) ( ( ( 𝐹 ‘ 𝑤 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑤 ) ) ) )
34 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
35 ovexd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑤 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) ( ( ( 𝐹 ‘ 𝑤 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑤 ) ) ) ∈ V )
36 10 33 34 35 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑥 ) ) ) ) ‘ 𝑤 ) = ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑤 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) ( ( ( 𝐹 ‘ 𝑤 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑤 ) ) ) )
37 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
38 13 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → 𝐸 ∈ Cat )
39 19 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → 𝐾 : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
40 21 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ( Base ‘ 𝐷 ) )
41 39 40 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ∈ ( Base ‘ 𝐸 ) )
42 eqid ⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
43 14 37 15 38 41 catidcl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐸 ) ‘ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) ∈ ( ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ( Hom ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) )
44 14 37 15 38 41 42 41 43 catlid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( Id ‘ 𝐸 ) ‘ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) ( ( Id ‘ 𝐸 ) ‘ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) )
45 39 40 fvco3d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑤 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) )
46 21 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
47 46 34 fvco3d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑤 ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑤 ) ) )
48 47 fveq2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑤 ) ) = ( ( ( 𝐹 ‘ 𝑤 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ‘ ( ( Id ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑤 ) ) ) )
49 eqid ⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
50 7 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
51 18 49 15 50 40 funcid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ‘ ( ( Id ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑤 ) ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) )
52 48 51 eqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑤 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) )
53 45 52 oveq12d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑤 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) ( ( ( 𝐹 ‘ 𝑤 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑤 ) ) ) = ( ( ( Id ‘ 𝐸 ) ‘ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) ( ( Id ‘ 𝐸 ) ‘ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) ) )
54 22 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐾 ∘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐸 ) )
55 54 34 fvco3d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( Id ‘ 𝐸 ) ∘ ( 𝐾 ∘ 𝐹 ) ) ‘ 𝑤 ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑤 ) ) )
56 46 34 fvco3d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑤 ) = ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) )
57 56 fveq2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐸 ) ‘ ( ( 𝐾 ∘ 𝐹 ) ‘ 𝑤 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) )
58 55 57 eqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( Id ‘ 𝐸 ) ∘ ( 𝐾 ∘ 𝐹 ) ) ‘ 𝑤 ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) )
59 44 53 58 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑤 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑤 ) ) ) ( ( ( 𝐹 ‘ 𝑤 ) 𝐿 ( 𝐹 ‘ 𝑤 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑤 ) ) ) = ( ( ( Id ‘ 𝐸 ) ∘ ( 𝐾 ∘ 𝐹 ) ) ‘ 𝑤 ) )
60 36 59 eqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑥 ) ) ) ) ‘ 𝑤 ) = ( ( ( Id ‘ 𝐸 ) ∘ ( 𝐾 ∘ 𝐹 ) ) ‘ 𝑤 ) )
61 12 24 60 eqfnfvd ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑥 ) ) ) ) = ( ( Id ‘ 𝐸 ) ∘ ( 𝐾 ∘ 𝐹 ) ) )
62 8 fveq2d ⊢ ( 𝜑 → ( 1 ‘ 𝑈 ) = ( 1 ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) )
63 eqid ⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
64 7 funcrcl2 ⊢ ( 𝜑 → 𝐷 ∈ Cat )
65 63 64 13 fuccat ⊢ ( 𝜑 → ( 𝐷 FuncCat 𝐸 ) ∈ Cat )
66 eqid ⊢ ( 𝐶 FuncCat 𝐷 ) = ( 𝐶 FuncCat 𝐷 )
67 6 funcrcl2 ⊢ ( 𝜑 → 𝐶 ∈ Cat )
68 66 67 64 fuccat ⊢ ( 𝜑 → ( 𝐶 FuncCat 𝐷 ) ∈ Cat )
69 63 fucbas ⊢ ( 𝐷 Func 𝐸 ) = ( Base ‘ ( 𝐷 FuncCat 𝐸 ) )
70 66 fucbas ⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ ( 𝐶 FuncCat 𝐷 ) )
71 eqid ⊢ ( Id ‘ ( 𝐷 FuncCat 𝐸 ) ) = ( Id ‘ ( 𝐷 FuncCat 𝐸 ) )
72 eqid ⊢ ( Id ‘ ( 𝐶 FuncCat 𝐷 ) ) = ( Id ‘ ( 𝐶 FuncCat 𝐷 ) )
73 df-br ⊢ ( 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
74 7 73 sylib ⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
75 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
76 6 75 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
77 2 65 68 69 70 71 72 3 74 76 xpcid ⊢ ( 𝜑 → ( 1 ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) = ⟨ ( ( Id ‘ ( 𝐷 FuncCat 𝐸 ) ) ‘ ⟨ 𝐾 , 𝐿 ⟩ ) , ( ( Id ‘ ( 𝐶 FuncCat 𝐷 ) ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ⟩ )
78 63 71 15 74 fucid ⊢ ( 𝜑 → ( ( Id ‘ ( 𝐷 FuncCat 𝐸 ) ) ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = ( ( Id ‘ 𝐸 ) ∘ ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ) )
79 relfunc ⊢ Rel ( 𝐷 Func 𝐸 )
80 79 brrelex1i ⊢ ( 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 → 𝐾 ∈ V )
81 7 80 syl ⊢ ( 𝜑 → 𝐾 ∈ V )
82 79 brrelex2i ⊢ ( 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 → 𝐿 ∈ V )
83 7 82 syl ⊢ ( 𝜑 → 𝐿 ∈ V )
84 op1stg ⊢ ( ( 𝐾 ∈ V ∧ 𝐿 ∈ V ) → ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
85 81 83 84 syl2anc ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
86 85 coeq2d ⊢ ( 𝜑 → ( ( Id ‘ 𝐸 ) ∘ ( 1st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ) = ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) )
87 78 86 eqtrd ⊢ ( 𝜑 → ( ( Id ‘ ( 𝐷 FuncCat 𝐸 ) ) ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) )
88 66 72 49 76 fucid ⊢ ( 𝜑 → ( ( Id ‘ ( 𝐶 FuncCat 𝐷 ) ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = ( ( Id ‘ 𝐷 ) ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) )
89 relfunc ⊢ Rel ( 𝐶 Func 𝐷 )
90 89 brrelex1i ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → 𝐹 ∈ V )
91 6 90 syl ⊢ ( 𝜑 → 𝐹 ∈ V )
92 89 brrelex2i ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → 𝐺 ∈ V )
93 6 92 syl ⊢ ( 𝜑 → 𝐺 ∈ V )
94 op1stg ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
95 91 93 94 syl2anc ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
96 95 coeq2d ⊢ ( 𝜑 → ( ( Id ‘ 𝐷 ) ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) )
97 88 96 eqtrd ⊢ ( 𝜑 → ( ( Id ‘ ( 𝐶 FuncCat 𝐷 ) ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) )
98 87 97 opeq12d ⊢ ( 𝜑 → ⟨ ( ( Id ‘ ( 𝐷 FuncCat 𝐸 ) ) ‘ ⟨ 𝐾 , 𝐿 ⟩ ) , ( ( Id ‘ ( 𝐶 FuncCat 𝐷 ) ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ⟩ = ⟨ ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) , ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ⟩ )
99 62 77 98 3eqtrd ⊢ ( 𝜑 → ( 1 ‘ 𝑈 ) = ⟨ ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) , ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ⟩ )
100 99 fveq2d ⊢ ( 𝜑 → ( ( 𝑈 𝑃 𝑈 ) ‘ ( 1 ‘ 𝑈 ) ) = ( ( 𝑈 𝑃 𝑈 ) ‘ ⟨ ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) , ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ⟩ ) )
101 df-ov ⊢ ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ( 𝑈 𝑃 𝑈 ) ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ) = ( ( 𝑈 𝑃 𝑈 ) ‘ ⟨ ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) , ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ⟩ )
102 100 101 eqtr4di ⊢ ( 𝜑 → ( ( 𝑈 𝑃 𝑈 ) ‘ ( 1 ‘ 𝑈 ) ) = ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ( 𝑈 𝑃 𝑈 ) ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ) )
103 eqid ⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
104 66 103 fuchom ⊢ ( 𝐶 Nat 𝐷 ) = ( Hom ‘ ( 𝐶 FuncCat 𝐷 ) )
105 70 104 72 68 76 catidcl ⊢ ( 𝜑 → ( ( Id ‘ ( 𝐶 FuncCat 𝐷 ) ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝐹 , 𝐺 ⟩ ) )
106 97 105 eqeltrrd ⊢ ( 𝜑 → ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝐹 , 𝐺 ⟩ ) )
107 eqid ⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
108 63 107 fuchom ⊢ ( 𝐷 Nat 𝐸 ) = ( Hom ‘ ( 𝐷 FuncCat 𝐸 ) )
109 69 108 71 65 74 catidcl ⊢ ( 𝜑 → ( ( Id ‘ ( 𝐷 FuncCat 𝐸 ) ) ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝐾 , 𝐿 ⟩ ) )
110 87 109 eqeltrrd ⊢ ( 𝜑 → ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝐾 , 𝐿 ⟩ ) )
111 1 8 8 106 110 fuco22 ⊢ ( 𝜑 → ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ( 𝑈 𝑃 𝑈 ) ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑥 ) ) ) ) )
112 102 111 eqtrd ⊢ ( 𝜑 → ( ( 𝑈 𝑃 𝑈 ) ‘ ( 1 ‘ 𝑈 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( Id ‘ 𝐸 ) ∘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ 𝐹 ) ‘ 𝑥 ) ) ) ) )
113 1 6 7 8 4 5 15 fuco11id ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑂 ‘ 𝑈 ) ) = ( ( Id ‘ 𝐸 ) ∘ ( 𝐾 ∘ 𝐹 ) ) )
114 61 112 113 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑈 𝑃 𝑈 ) ‘ ( 1 ‘ 𝑈 ) ) = ( 𝐼 ‘ ( 𝑂 ‘ 𝑈 ) ) )