fucoco2

Description: Composition in the source category is mapped to composition in the target. See also fucoco . (Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fucoco2.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
	fucoco2.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
	fucoco2.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	fucoco2.1	⊢ · = ( comp ‘ 𝑇 )
	fucoco2.2	⊢ ∙ = ( comp ‘ 𝑄 )
	fucoco2.w	⊢ ( 𝜑 → 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
	fucoco2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
	fucoco2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑊 )
	fucoco2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
	fucoco2.j	⊢ 𝐽 = ( Hom ‘ 𝑇 )
	fucoco2.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝐽 𝑌 ) )
	fucoco2.b	⊢ ( 𝜑 → 𝐵 ∈ ( 𝑌 𝐽 𝑍 ) )
Assertion	fucoco2	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐴 ) ) = ( ( ( 𝑌 𝑃 𝑍 ) ‘ 𝐵 ) ( ⟨ ( 𝑂 ‘ 𝑋 ) , ( 𝑂 ‘ 𝑌 ) ⟩ ∙ ( 𝑂 ‘ 𝑍 ) ) ( ( 𝑋 𝑃 𝑌 ) ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucoco2.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
2		fucoco2.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
3		fucoco2.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
4		fucoco2.1	⊢ · = ( comp ‘ 𝑇 )
5		fucoco2.2	⊢ ∙ = ( comp ‘ 𝑄 )
6		fucoco2.w	⊢ ( 𝜑 → 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
7		fucoco2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
8		fucoco2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑊 )
9		fucoco2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
10		fucoco2.j	⊢ 𝐽 = ( Hom ‘ 𝑇 )
11		fucoco2.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝐽 𝑌 ) )
12		fucoco2.b	⊢ ( 𝜑 → 𝐵 ∈ ( 𝑌 𝐽 𝑍 ) )
13	1	xpcfucbas	⊢ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( Base ‘ 𝑇 )
14	7 6	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
15	8 6	eleqtrd	⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
16	1 13 10 14 15	xpcfuchom	⊢ ( 𝜑 → ( 𝑋 𝐽 𝑌 ) = ( ( ( 1^st ‘ 𝑋 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑌 ) ) ) )
17	11 16	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( ( ( 1^st ‘ 𝑋 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑌 ) ) ) )
18		xp1st	⊢ ( 𝐴 ∈ ( ( ( 1^st ‘ 𝑋 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑌 ) ) ) → ( 1^st ‘ 𝐴 ) ∈ ( ( 1^st ‘ 𝑋 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑌 ) ) )
19	17 18	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝐴 ) ∈ ( ( 1^st ‘ 𝑋 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑌 ) ) )
20		xp2nd	⊢ ( 𝐴 ∈ ( ( ( 1^st ‘ 𝑋 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑌 ) ) ) → ( 2^nd ‘ 𝐴 ) ∈ ( ( 2^nd ‘ 𝑋 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑌 ) ) )
21	17 20	syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝐴 ) ∈ ( ( 2^nd ‘ 𝑋 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑌 ) ) )
22	9 6	eleqtrd	⊢ ( 𝜑 → 𝑍 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
23	1 13 10 15 22	xpcfuchom	⊢ ( 𝜑 → ( 𝑌 𝐽 𝑍 ) = ( ( ( 1^st ‘ 𝑌 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑍 ) ) × ( ( 2^nd ‘ 𝑌 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ) )
24	12 23	eleqtrd	⊢ ( 𝜑 → 𝐵 ∈ ( ( ( 1^st ‘ 𝑌 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑍 ) ) × ( ( 2^nd ‘ 𝑌 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ) )
25		xp1st	⊢ ( 𝐵 ∈ ( ( ( 1^st ‘ 𝑌 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑍 ) ) × ( ( 2^nd ‘ 𝑌 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ) → ( 1^st ‘ 𝐵 ) ∈ ( ( 1^st ‘ 𝑌 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑍 ) ) )
26	24 25	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝐵 ) ∈ ( ( 1^st ‘ 𝑌 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑍 ) ) )
27		xp2nd	⊢ ( 𝐵 ∈ ( ( ( 1^st ‘ 𝑌 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑍 ) ) × ( ( 2^nd ‘ 𝑌 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ) → ( 2^nd ‘ 𝐵 ) ∈ ( ( 2^nd ‘ 𝑌 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑍 ) ) )
28	24 27	syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝐵 ) ∈ ( ( 2^nd ‘ 𝑌 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑍 ) ) )
29		1st2nd2	⊢ ( 𝑋 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) → 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
30	14 29	syl	⊢ ( 𝜑 → 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
31		1st2nd2	⊢ ( 𝑌 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) → 𝑌 = ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ )
32	15 31	syl	⊢ ( 𝜑 → 𝑌 = ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ )
33		1st2nd2	⊢ ( 𝑍 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) → 𝑍 = ⟨ ( 1^st ‘ 𝑍 ) , ( 2^nd ‘ 𝑍 ) ⟩ )
34	22 33	syl	⊢ ( 𝜑 → 𝑍 = ⟨ ( 1^st ‘ 𝑍 ) , ( 2^nd ‘ 𝑍 ) ⟩ )
35		1st2nd2	⊢ ( 𝐴 ∈ ( ( ( 1^st ‘ 𝑋 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑌 ) ) ) → 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ )
36	17 35	syl	⊢ ( 𝜑 → 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ )
37		1st2nd2	⊢ ( 𝐵 ∈ ( ( ( 1^st ‘ 𝑌 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑍 ) ) × ( ( 2^nd ‘ 𝑌 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑍 ) ) ) → 𝐵 = ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ )
38	24 37	syl	⊢ ( 𝜑 → 𝐵 = ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ )
39	19 21 26 28 3 30 32 34 36 38 2 5 1 4	fucoco	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑍 ) ‘ ( 𝐵 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐴 ) ) = ( ( ( 𝑌 𝑃 𝑍 ) ‘ 𝐵 ) ( ⟨ ( 𝑂 ‘ 𝑋 ) , ( 𝑂 ‘ 𝑌 ) ⟩ ∙ ( 𝑂 ‘ 𝑍 ) ) ( ( 𝑋 𝑃 𝑌 ) ‘ 𝐴 ) ) )

Metamath Proof Explorer

Theorem fucoco2

Proof