Metamath Proof Explorer

Theorem hofcllem

Description: Lemma for hofcl . (Contributed by Mario Carneiro, 15-Jan-2017)

Ref Expression
Hypotheses hofcl.m ⊢ 𝑀 = ( HomF ‘ 𝐶 )
hofcl.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
hofcl.d ⊢ 𝐷 = ( SetCat ‘ 𝑈 )
hofcl.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
hofcl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
hofcl.h ⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
hofcllem.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
hofcllem.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
hofcllem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
hofcllem.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
hofcllem.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
hofcllem.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
hofcllem.s ⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
hofcllem.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )
hofcllem.m ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑍 𝐻 𝑋 ) )
hofcllem.n ⊢ ( 𝜑 → 𝐿 ∈ ( 𝑌 𝐻 𝑊 ) )
hofcllem.p ⊢ ( 𝜑 → 𝑃 ∈ ( 𝑆 𝐻 𝑍 ) )
hofcllem.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑊 𝐻 𝑇 ) )
Assertion hofcllem ( 𝜑 → ( ( 𝐾 ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑃 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑆 , 𝑇 ⟩ ) ( 𝑄 ( ⟨ 𝑌 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐿 ) ) = ( ( 𝑃 ( ⟨ 𝑍 , 𝑊 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑆 , 𝑇 ⟩ ) 𝑄 ) ( ⟨ ( 𝑋 𝐻 𝑌 ) , ( 𝑍 𝐻 𝑊 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑆 𝐻 𝑇 ) ) ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝐿 ) ) )

Proof

Step Hyp Ref Expression
1 hofcl.m ⊢ 𝑀 = ( HomF ‘ 𝐶 )
2 hofcl.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
3 hofcl.d ⊢ 𝐷 = ( SetCat ‘ 𝑈 )
4 hofcl.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 hofcl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
6 hofcl.h ⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
7 hofcllem.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
8 hofcllem.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
9 hofcllem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
10 hofcllem.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
11 hofcllem.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
12 hofcllem.w ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
13 hofcllem.s ⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
14 hofcllem.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )
15 hofcllem.m ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑍 𝐻 𝑋 ) )
16 hofcllem.n ⊢ ( 𝜑 → 𝐿 ∈ ( 𝑌 𝐻 𝑊 ) )
17 hofcllem.p ⊢ ( 𝜑 → 𝑃 ∈ ( 𝑆 𝐻 𝑍 ) )
18 hofcllem.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑊 𝐻 𝑇 ) )
19 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
20 4 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝐶 ∈ Cat )
21 13 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑆 ∈ 𝐵 )
22 11 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑍 ∈ 𝐵 )
23 9 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑋 ∈ 𝐵 )
24 17 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑃 ∈ ( 𝑆 𝐻 𝑍 ) )
25 15 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝐾 ∈ ( 𝑍 𝐻 𝑋 ) )
26 14 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑇 ∈ 𝐵 )
27 10 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑌 ∈ 𝐵 )
28 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
29 7 8 19 4 10 12 14 16 18 catcocl ⊢ ( 𝜑 → ( 𝑄 ( ⟨ 𝑌 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐿 ) ∈ ( 𝑌 𝐻 𝑇 ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( 𝑄 ( ⟨ 𝑌 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐿 ) ∈ ( 𝑌 𝐻 𝑇 ) )
31 7 8 19 20 23 27 26 28 30 catcocl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( ( 𝑄 ( ⟨ 𝑌 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐿 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑓 ) ∈ ( 𝑋 𝐻 𝑇 ) )
32 7 8 19 20 21 22 23 24 25 26 31 catass ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( ( ( ( 𝑄 ( ⟨ 𝑌 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐿 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐾 ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) = ( ( ( 𝑄 ( ⟨ 𝑌 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐿 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑓 ) ( ⟨ 𝑆 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( 𝐾 ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑃 ) ) )
33 12 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑊 ∈ 𝐵 )
34 16 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝐿 ∈ ( 𝑌 𝐻 𝑊 ) )
35 18 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑄 ∈ ( 𝑊 𝐻 𝑇 ) )
36 7 8 19 20 23 27 33 28 34 26 35 catass ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( ( 𝑄 ( ⟨ 𝑌 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐿 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑓 ) = ( 𝑄 ( ⟨ 𝑋 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ) )
37 36 oveq1d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( ( ( 𝑄 ( ⟨ 𝑌 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐿 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐾 ) = ( ( 𝑄 ( ⟨ 𝑋 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐾 ) )
38 7 8 19 20 23 27 33 28 34 catcocl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ∈ ( 𝑋 𝐻 𝑊 ) )
39 7 8 19 20 22 23 33 25 38 26 35 catass ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( ( 𝑄 ( ⟨ 𝑋 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐾 ) = ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) )
40 37 39 eqtrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( ( ( 𝑄 ( ⟨ 𝑌 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐿 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐾 ) = ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) )
41 40 oveq1d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( ( ( ( 𝑄 ( ⟨ 𝑌 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐿 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐾 ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) = ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) )
42 32 41 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( ( ( 𝑄 ( ⟨ 𝑌 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐿 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑓 ) ( ⟨ 𝑆 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( 𝐾 ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑃 ) ) = ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) )
43 42 mpteq2dva ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( ( 𝑄 ( ⟨ 𝑌 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐿 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑓 ) ( ⟨ 𝑆 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( 𝐾 ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑃 ) ) ) = ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) ) )
44 7 8 19 4 13 11 9 17 15 catcocl ⊢ ( 𝜑 → ( 𝐾 ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑃 ) ∈ ( 𝑆 𝐻 𝑋 ) )
45 1 4 7 8 9 10 13 14 19 44 29 hof2val ⊢ ( 𝜑 → ( ( 𝐾 ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑃 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑆 , 𝑇 ⟩ ) ( 𝑄 ( ⟨ 𝑌 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐿 ) ) = ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( ( 𝑄 ( ⟨ 𝑌 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐿 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑓 ) ( ⟨ 𝑆 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( 𝐾 ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑃 ) ) ) )
46 1 4 7 8 11 12 13 14 19 17 18 hof2val ⊢ ( 𝜑 → ( 𝑃 ( ⟨ 𝑍 , 𝑊 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑆 , 𝑇 ⟩ ) 𝑄 ) = ( 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ↦ ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑔 ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) ) )
47 1 4 7 8 9 10 11 12 19 15 16 hof2val ⊢ ( 𝜑 → ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝐿 ) = ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) )
48 46 47 oveq12d ⊢ ( 𝜑 → ( ( 𝑃 ( ⟨ 𝑍 , 𝑊 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑆 , 𝑇 ⟩ ) 𝑄 ) ( ⟨ ( 𝑋 𝐻 𝑌 ) , ( 𝑍 𝐻 𝑊 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑆 𝐻 𝑇 ) ) ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝐿 ) ) = ( ( 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ↦ ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑔 ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) ) ( ⟨ ( 𝑋 𝐻 𝑌 ) , ( 𝑍 𝐻 𝑊 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑆 𝐻 𝑇 ) ) ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) ) )
49 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
50 eqid ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
51 50 7 8 9 10 homfval ⊢ ( 𝜑 → ( 𝑋 ( Homf ‘ 𝐶 ) 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )
52 50 7 homffn ⊢ ( Homf ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 )
53 52 a1i ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 ) )
54 df-f ⊢ ( ( Homf ‘ 𝐶 ) : ( 𝐵 × 𝐵 ) ⟶ 𝑈 ↔ ( ( Homf ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 ) ∧ ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 ) )
55 53 6 54 sylanbrc ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) : ( 𝐵 × 𝐵 ) ⟶ 𝑈 )
56 55 9 10 fovcdmd ⊢ ( 𝜑 → ( 𝑋 ( Homf ‘ 𝐶 ) 𝑌 ) ∈ 𝑈 )
57 51 56 eqeltrrd ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) ∈ 𝑈 )
58 50 7 8 11 12 homfval ⊢ ( 𝜑 → ( 𝑍 ( Homf ‘ 𝐶 ) 𝑊 ) = ( 𝑍 𝐻 𝑊 ) )
59 55 11 12 fovcdmd ⊢ ( 𝜑 → ( 𝑍 ( Homf ‘ 𝐶 ) 𝑊 ) ∈ 𝑈 )
60 58 59 eqeltrrd ⊢ ( 𝜑 → ( 𝑍 𝐻 𝑊 ) ∈ 𝑈 )
61 50 7 8 13 14 homfval ⊢ ( 𝜑 → ( 𝑆 ( Homf ‘ 𝐶 ) 𝑇 ) = ( 𝑆 𝐻 𝑇 ) )
62 55 13 14 fovcdmd ⊢ ( 𝜑 → ( 𝑆 ( Homf ‘ 𝐶 ) 𝑇 ) ∈ 𝑈 )
63 61 62 eqeltrrd ⊢ ( 𝜑 → ( 𝑆 𝐻 𝑇 ) ∈ 𝑈 )
64 7 8 19 20 22 23 33 25 38 catcocl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ∈ ( 𝑍 𝐻 𝑊 ) )
65 64 fmpttd ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( 𝑍 𝐻 𝑊 ) )
66 4 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝐶 ∈ Cat )
67 13 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝑆 ∈ 𝐵 )
68 11 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝑍 ∈ 𝐵 )
69 14 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝑇 ∈ 𝐵 )
70 17 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝑃 ∈ ( 𝑆 𝐻 𝑍 ) )
71 12 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝑊 ∈ 𝐵 )
72 simpr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) )
73 18 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ) → 𝑄 ∈ ( 𝑊 𝐻 𝑇 ) )
74 7 8 19 66 68 71 69 72 73 catcocl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑔 ) ∈ ( 𝑍 𝐻 𝑇 ) )
75 7 8 19 66 67 68 69 70 74 catcocl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ) → ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑔 ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) ∈ ( 𝑆 𝐻 𝑇 ) )
76 75 fmpttd ⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ↦ ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑔 ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) ) : ( 𝑍 𝐻 𝑊 ) ⟶ ( 𝑆 𝐻 𝑇 ) )
77 3 5 49 57 60 63 65 76 setcco ⊢ ( 𝜑 → ( ( 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ↦ ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑔 ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) ) ( ⟨ ( 𝑋 𝐻 𝑌 ) , ( 𝑍 𝐻 𝑊 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑆 𝐻 𝑇 ) ) ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) ) = ( ( 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ↦ ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑔 ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) ) ∘ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) ) )
78 eqidd ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) = ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) )
79 eqidd ⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ↦ ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑔 ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) ) = ( 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ↦ ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑔 ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) ) )
80 oveq2 ⊢ ( 𝑔 = ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) → ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑔 ) = ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) )
81 80 oveq1d ⊢ ( 𝑔 = ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) → ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑔 ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) = ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) )
82 64 78 79 81 fmptco ⊢ ( 𝜑 → ( ( 𝑔 ∈ ( 𝑍 𝐻 𝑊 ) ↦ ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑔 ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) ) ∘ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) ) = ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) ) )
83 48 77 82 3eqtrd ⊢ ( 𝜑 → ( ( 𝑃 ( ⟨ 𝑍 , 𝑊 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑆 , 𝑇 ⟩ ) 𝑄 ) ( ⟨ ( 𝑋 𝐻 𝑌 ) , ( 𝑍 𝐻 𝑊 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑆 𝐻 𝑇 ) ) ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝐿 ) ) = ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝑄 ( ⟨ 𝑍 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) ( ( 𝐿 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝑓 ) ( ⟨ 𝑍 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑊 ) 𝐾 ) ) ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝑃 ) ) )
84 43 45 83 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐾 ( ⟨ 𝑆 , 𝑍 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑃 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑆 , 𝑇 ⟩ ) ( 𝑄 ( ⟨ 𝑌 , 𝑊 ⟩ ( comp ‘ 𝐶 ) 𝑇 ) 𝐿 ) ) = ( ( 𝑃 ( ⟨ 𝑍 , 𝑊 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑆 , 𝑇 ⟩ ) 𝑄 ) ( ⟨ ( 𝑋 𝐻 𝑌 ) , ( 𝑍 𝐻 𝑊 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑆 𝐻 𝑇 ) ) ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝐿 ) ) )