xpccatid

Description: The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	xpccat.t	⊢ 𝑇 = ( 𝐶 ×_c 𝐷 )
	xpccat.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	xpccat.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	xpccat.x	⊢ 𝑋 = ( Base ‘ 𝐶 )
	xpccat.y	⊢ 𝑌 = ( Base ‘ 𝐷 )
	xpccat.i	⊢ 𝐼 = ( Id ‘ 𝐶 )
	xpccat.j	⊢ 𝐽 = ( Id ‘ 𝐷 )
Assertion	xpccatid	⊢ ( 𝜑 → ( 𝑇 ∈ Cat ∧ ( Id ‘ 𝑇 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝐼 ‘ 𝑥 ) , ( 𝐽 ‘ 𝑦 ) ⟩ ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpccat.t	⊢ 𝑇 = ( 𝐶 ×_c 𝐷 )
2		xpccat.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		xpccat.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
4		xpccat.x	⊢ 𝑋 = ( Base ‘ 𝐶 )
5		xpccat.y	⊢ 𝑌 = ( Base ‘ 𝐷 )
6		xpccat.i	⊢ 𝐼 = ( Id ‘ 𝐶 )
7		xpccat.j	⊢ 𝐽 = ( Id ‘ 𝐷 )
8	1 4 5	xpcbas	⊢ ( 𝑋 × 𝑌 ) = ( Base ‘ 𝑇 )
9	8	a1i	⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( Base ‘ 𝑇 ) )
10		eqidd	⊢ ( 𝜑 → ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 ) )
11		eqidd	⊢ ( 𝜑 → ( comp ‘ 𝑇 ) = ( comp ‘ 𝑇 ) )
12	1	ovexi	⊢ 𝑇 ∈ V
13	12	a1i	⊢ ( 𝜑 → 𝑇 ∈ V )
14		biid	⊢ ( ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ↔ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) )
15		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
16	2	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) → 𝐶 ∈ Cat )
17		xp1st	⊢ ( 𝑡 ∈ ( 𝑋 × 𝑌 ) → ( 1^st ‘ 𝑡 ) ∈ 𝑋 )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) → ( 1^st ‘ 𝑡 ) ∈ 𝑋 )
19	4 15 6 16 18	catidcl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) → ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) ∈ ( ( 1^st ‘ 𝑡 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) )
20		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
21	3	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) → 𝐷 ∈ Cat )
22		xp2nd	⊢ ( 𝑡 ∈ ( 𝑋 × 𝑌 ) → ( 2^nd ‘ 𝑡 ) ∈ 𝑌 )
23	22	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) → ( 2^nd ‘ 𝑡 ) ∈ 𝑌 )
24	5 20 7 21 23	catidcl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) → ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ∈ ( ( 2^nd ‘ 𝑡 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) )
25	19 24	opelxpd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) → ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ∈ ( ( ( 1^st ‘ 𝑡 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) × ( ( 2^nd ‘ 𝑡 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) ) )
26		eqid	⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
27		simpr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) → 𝑡 ∈ ( 𝑋 × 𝑌 ) )
28	1 8 15 20 26 27 27	xpchom	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) → ( 𝑡 ( Hom ‘ 𝑇 ) 𝑡 ) = ( ( ( 1^st ‘ 𝑡 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) × ( ( 2^nd ‘ 𝑡 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) ) )
29	25 28	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) → ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑡 ) )
30		fvex	⊢ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) ∈ V
31		fvex	⊢ ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ∈ V
32	30 31	op1st	⊢ ( 1^st ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) = ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) )
33	32	oveq1i	⊢ ( ( 1^st ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) ( 1^st ‘ 𝑓 ) ) = ( ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) ( 1^st ‘ 𝑓 ) )
34	2	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → 𝐶 ∈ Cat )
35		simpr1l	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → 𝑠 ∈ ( 𝑋 × 𝑌 ) )
36		xp1st	⊢ ( 𝑠 ∈ ( 𝑋 × 𝑌 ) → ( 1^st ‘ 𝑠 ) ∈ 𝑋 )
37	35 36	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 1^st ‘ 𝑠 ) ∈ 𝑋 )
38		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
39		simpr1r	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → 𝑡 ∈ ( 𝑋 × 𝑌 ) )
40	39 17	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 1^st ‘ 𝑡 ) ∈ 𝑋 )
41		simpr31	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) )
42	1 8 15 20 26 35 39	xpchom	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) = ( ( ( 1^st ‘ 𝑠 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) × ( ( 2^nd ‘ 𝑠 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) ) )
43	41 42	eleqtrd	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → 𝑓 ∈ ( ( ( 1^st ‘ 𝑠 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) × ( ( 2^nd ‘ 𝑠 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) ) )
44		xp1st	⊢ ( 𝑓 ∈ ( ( ( 1^st ‘ 𝑠 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) × ( ( 2^nd ‘ 𝑠 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) ) → ( 1^st ‘ 𝑓 ) ∈ ( ( 1^st ‘ 𝑠 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) )
45	43 44	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 1^st ‘ 𝑓 ) ∈ ( ( 1^st ‘ 𝑠 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) )
46	4 15 6 34 37 38 40 45	catlid	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) ( 1^st ‘ 𝑓 ) ) = ( 1^st ‘ 𝑓 ) )
47	33 46	eqtrid	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 1^st ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) ( 1^st ‘ 𝑓 ) ) = ( 1^st ‘ 𝑓 ) )
48	30 31	op2nd	⊢ ( 2^nd ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) = ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) )
49	48	oveq1i	⊢ ( ( 2^nd ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) ( 2^nd ‘ 𝑓 ) ) = ( ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) ( 2^nd ‘ 𝑓 ) )
50	3	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → 𝐷 ∈ Cat )
51		xp2nd	⊢ ( 𝑠 ∈ ( 𝑋 × 𝑌 ) → ( 2^nd ‘ 𝑠 ) ∈ 𝑌 )
52	35 51	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 2^nd ‘ 𝑠 ) ∈ 𝑌 )
53		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
54	39 22	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 2^nd ‘ 𝑡 ) ∈ 𝑌 )
55		xp2nd	⊢ ( 𝑓 ∈ ( ( ( 1^st ‘ 𝑠 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) × ( ( 2^nd ‘ 𝑠 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) ) → ( 2^nd ‘ 𝑓 ) ∈ ( ( 2^nd ‘ 𝑠 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) )
56	43 55	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 2^nd ‘ 𝑓 ) ∈ ( ( 2^nd ‘ 𝑠 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) )
57	5 20 7 50 52 53 54 56	catlid	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) ( 2^nd ‘ 𝑓 ) ) = ( 2^nd ‘ 𝑓 ) )
58	49 57	eqtrid	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 2^nd ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) ( 2^nd ‘ 𝑓 ) ) = ( 2^nd ‘ 𝑓 ) )
59	47 58	opeq12d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ⟨ ( ( 1^st ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ = ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ )
60		eqid	⊢ ( comp ‘ 𝑇 ) = ( comp ‘ 𝑇 )
61	39 29	syldan	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑡 ) )
62	1 8 26 38 53 60 35 39 39 41 61	xpcco	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑡 ) 𝑓 ) = ⟨ ( ( 1^st ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ )
63		1st2nd2	⊢ ( 𝑓 ∈ ( ( ( 1^st ‘ 𝑠 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑡 ) ) × ( ( 2^nd ‘ 𝑠 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑡 ) ) ) → 𝑓 = ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ )
64	43 63	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → 𝑓 = ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ )
65	59 62 64	3eqtr4d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑡 ) 𝑓 ) = 𝑓 )
66	32	oveq2i	⊢ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ) = ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) )
67		simpr2l	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → 𝑢 ∈ ( 𝑋 × 𝑌 ) )
68		xp1st	⊢ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) → ( 1^st ‘ 𝑢 ) ∈ 𝑋 )
69	67 68	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 1^st ‘ 𝑢 ) ∈ 𝑋 )
70		simpr32	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) )
71	1 8 15 20 26 39 67	xpchom	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) = ( ( ( 1^st ‘ 𝑡 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) × ( ( 2^nd ‘ 𝑡 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ) )
72	70 71	eleqtrd	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → 𝑔 ∈ ( ( ( 1^st ‘ 𝑡 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) × ( ( 2^nd ‘ 𝑡 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ) )
73		xp1st	⊢ ( 𝑔 ∈ ( ( ( 1^st ‘ 𝑡 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) × ( ( 2^nd ‘ 𝑡 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ) → ( 1^st ‘ 𝑔 ) ∈ ( ( 1^st ‘ 𝑡 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) )
74	72 73	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 1^st ‘ 𝑔 ) ∈ ( ( 1^st ‘ 𝑡 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) )
75	4 15 6 34 40 38 69 74	catrid	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) ) = ( 1^st ‘ 𝑔 ) )
76	66 75	eqtrid	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ) = ( 1^st ‘ 𝑔 ) )
77	48	oveq2i	⊢ ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ) = ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) )
78		xp2nd	⊢ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) → ( 2^nd ‘ 𝑢 ) ∈ 𝑌 )
79	67 78	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 2^nd ‘ 𝑢 ) ∈ 𝑌 )
80		xp2nd	⊢ ( 𝑔 ∈ ( ( ( 1^st ‘ 𝑡 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) × ( ( 2^nd ‘ 𝑡 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ) → ( 2^nd ‘ 𝑔 ) ∈ ( ( 2^nd ‘ 𝑡 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) )
81	72 80	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 2^nd ‘ 𝑔 ) ∈ ( ( 2^nd ‘ 𝑡 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) )
82	5 20 7 50 54 53 79 81	catrid	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ) = ( 2^nd ‘ 𝑔 ) )
83	77 82	eqtrid	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ) = ( 2^nd ‘ 𝑔 ) )
84	76 83	opeq12d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ) ⟩ = ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ )
85	1 8 26 38 53 60 39 39 67 61 70	xpcco	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 𝑔 ( ⟨ 𝑡 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) = ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ) ⟩ )
86		1st2nd2	⊢ ( 𝑔 ∈ ( ( ( 1^st ‘ 𝑡 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) × ( ( 2^nd ‘ 𝑡 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ) → 𝑔 = ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ )
87	72 86	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → 𝑔 = ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ )
88	84 85 87	3eqtr4d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 𝑔 ( ⟨ 𝑡 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) = 𝑔 )
89	4 15 38 34 37 40 69 45 74	catcocl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ 𝑓 ) ) ∈ ( ( 1^st ‘ 𝑠 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) )
90	5 20 53 50 52 54 79 56 81	catcocl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ 𝑓 ) ) ∈ ( ( 2^nd ‘ 𝑠 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) )
91	89 90	opelxpd	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ∈ ( ( ( 1^st ‘ 𝑠 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) × ( ( 2^nd ‘ 𝑠 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ) )
92	1 8 26 38 53 60 35 39 67 41 70	xpcco	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) = ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ )
93	1 8 15 20 26 35 67	xpchom	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 𝑠 ( Hom ‘ 𝑇 ) 𝑢 ) = ( ( ( 1^st ‘ 𝑠 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) × ( ( 2^nd ‘ 𝑠 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ) )
94	91 92 93	3eltr4d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑢 ) )
95		simpr2r	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → 𝑣 ∈ ( 𝑋 × 𝑌 ) )
96		xp1st	⊢ ( 𝑣 ∈ ( 𝑋 × 𝑌 ) → ( 1^st ‘ 𝑣 ) ∈ 𝑋 )
97	95 96	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 1^st ‘ 𝑣 ) ∈ 𝑋 )
98		simpr33	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) )
99	1 8 15 20 26 67 95	xpchom	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) = ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) )
100	98 99	eleqtrd	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ℎ ∈ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) )
101		xp1st	⊢ ( ℎ ∈ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) → ( 1^st ‘ ℎ ) ∈ ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) )
102	100 101	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 1^st ‘ ℎ ) ∈ ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) )
103	4 15 38 34 37 40 69 45 74 97 102	catass	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑔 ) ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑓 ) ) = ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ 𝑓 ) ) ) )
104	1 8 26 38 53 60 39 67 95 70 98	xpcco	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) = ⟨ ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑔 ) ) , ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑔 ) ) ⟩ )
105	104	fveq2d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 1^st ‘ ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) ) = ( 1^st ‘ ⟨ ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑔 ) ) , ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑔 ) ) ⟩ ) )
106		ovex	⊢ ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑔 ) ) ∈ V
107		ovex	⊢ ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑔 ) ) ∈ V
108	106 107	op1st	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑔 ) ) , ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑔 ) ) ⟩ ) = ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑔 ) )
109	105 108	eqtrdi	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 1^st ‘ ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) ) = ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑔 ) ) )
110	109	oveq1d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 1^st ‘ ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑓 ) ) = ( ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑔 ) ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑓 ) ) )
111	92	fveq2d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 1^st ‘ ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) ) = ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
112		ovex	⊢ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ 𝑓 ) ) ∈ V
113		ovex	⊢ ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ 𝑓 ) ) ∈ V
114	112 113	op1st	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ 𝑓 ) )
115	111 114	eqtrdi	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 1^st ‘ ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) ) = ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ 𝑓 ) ) )
116	115	oveq2d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) ) ) = ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ 𝑓 ) ) ) )
117	103 110 116	3eqtr4d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 1^st ‘ ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑓 ) ) = ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) ) ) )
118		xp2nd	⊢ ( 𝑣 ∈ ( 𝑋 × 𝑌 ) → ( 2^nd ‘ 𝑣 ) ∈ 𝑌 )
119	95 118	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 2^nd ‘ 𝑣 ) ∈ 𝑌 )
120		xp2nd	⊢ ( ℎ ∈ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) → ( 2^nd ‘ ℎ ) ∈ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) )
121	100 120	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 2^nd ‘ ℎ ) ∈ ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) )
122	5 20 53 50 52 54 79 56 81 119 121	catass	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑔 ) ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑓 ) ) = ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ 𝑓 ) ) ) )
123	104	fveq2d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 2^nd ‘ ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) ) = ( 2^nd ‘ ⟨ ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑔 ) ) , ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑔 ) ) ⟩ ) )
124	106 107	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑔 ) ) , ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑔 ) ) ⟩ ) = ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑔 ) )
125	123 124	eqtrdi	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 2^nd ‘ ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) ) = ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑔 ) ) )
126	125	oveq1d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 2^nd ‘ ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑓 ) ) = ( ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑔 ) ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑓 ) ) )
127	92	fveq2d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 2^nd ‘ ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) ) = ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) )
128	112 113	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑢 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) = ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ 𝑓 ) )
129	127 128	eqtrdi	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 2^nd ‘ ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) ) = ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ 𝑓 ) ) )
130	129	oveq2d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) ) ) = ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑢 ) ) ( 2^nd ‘ 𝑓 ) ) ) )
131	122 126 130	3eqtr4d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 2^nd ‘ ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑓 ) ) = ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) ) ) )
132	117 131	opeq12d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ⟨ ( ( 1^st ‘ ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ = ⟨ ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) ) ) , ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) ) ) ⟩ )
133	4 15 38 34 40 69 97 74 102	catcocl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑔 ) ) ∈ ( ( 1^st ‘ 𝑡 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) )
134	5 20 53 50 54 79 119 81 121	catcocl	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑔 ) ) ∈ ( ( 2^nd ‘ 𝑡 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) )
135	133 134	opelxpd	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ⟨ ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑡 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑔 ) ) , ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑡 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑔 ) ) ⟩ ∈ ( ( ( 1^st ‘ 𝑡 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑡 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) )
136	1 8 15 20 26 39 95	xpchom	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( 𝑡 ( Hom ‘ 𝑇 ) 𝑣 ) = ( ( ( 1^st ‘ 𝑡 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑡 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) )
137	135 104 136	3eltr4d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑣 ) )
138	1 8 26 38 53 60 35 39 95 41 137	xpcco	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑓 ) = ⟨ ( ( 1^st ‘ ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑡 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑡 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ )
139	1 8 26 38 53 60 35 67 95 94 98	xpcco	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ℎ ( ⟨ 𝑠 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) ) = ⟨ ( ( 1^st ‘ ℎ ) ( ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑢 ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) ( 1^st ‘ ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) ) ) , ( ( 2^nd ‘ ℎ ) ( ⟨ ( 2^nd ‘ 𝑠 ) , ( 2^nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ( 2^nd ‘ ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) ) ) ⟩ )
140	132 138 139	3eqtr4d	⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) ∧ ( 𝑓 ∈ ( 𝑠 ( Hom ‘ 𝑇 ) 𝑡 ) ∧ 𝑔 ∈ ( 𝑡 ( Hom ‘ 𝑇 ) 𝑢 ) ∧ ℎ ∈ ( 𝑢 ( Hom ‘ 𝑇 ) 𝑣 ) ) ) ) → ( ( ℎ ( ⟨ 𝑡 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑔 ) ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) 𝑓 ) = ( ℎ ( ⟨ 𝑠 , 𝑢 ⟩ ( comp ‘ 𝑇 ) 𝑣 ) ( 𝑔 ( ⟨ 𝑠 , 𝑡 ⟩ ( comp ‘ 𝑇 ) 𝑢 ) 𝑓 ) ) )
141	9 10 11 13 14 29 65 88 94 140	iscatd2	⊢ ( 𝜑 → ( 𝑇 ∈ Cat ∧ ( Id ‘ 𝑇 ) = ( 𝑡 ∈ ( 𝑋 × 𝑌 ) ↦ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ) )
142		vex	⊢ 𝑥 ∈ V
143		vex	⊢ 𝑦 ∈ V
144	142 143	op1std	⊢ ( 𝑡 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ 𝑡 ) = 𝑥 )
145	144	fveq2d	⊢ ( 𝑡 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) = ( 𝐼 ‘ 𝑥 ) )
146	142 143	op2ndd	⊢ ( 𝑡 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2^nd ‘ 𝑡 ) = 𝑦 )
147	146	fveq2d	⊢ ( 𝑡 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) = ( 𝐽 ‘ 𝑦 ) )
148	145 147	opeq12d	⊢ ( 𝑡 = ⟨ 𝑥 , 𝑦 ⟩ → ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ = ⟨ ( 𝐼 ‘ 𝑥 ) , ( 𝐽 ‘ 𝑦 ) ⟩ )
149	148	mpompt	⊢ ( 𝑡 ∈ ( 𝑋 × 𝑌 ) ↦ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝐼 ‘ 𝑥 ) , ( 𝐽 ‘ 𝑦 ) ⟩ )
150	149	eqeq2i	⊢ ( ( Id ‘ 𝑇 ) = ( 𝑡 ∈ ( 𝑋 × 𝑌 ) ↦ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ↔ ( Id ‘ 𝑇 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝐼 ‘ 𝑥 ) , ( 𝐽 ‘ 𝑦 ) ⟩ ) )
151	150	anbi2i	⊢ ( ( 𝑇 ∈ Cat ∧ ( Id ‘ 𝑇 ) = ( 𝑡 ∈ ( 𝑋 × 𝑌 ) ↦ ⟨ ( 𝐼 ‘ ( 1^st ‘ 𝑡 ) ) , ( 𝐽 ‘ ( 2^nd ‘ 𝑡 ) ) ⟩ ) ) ↔ ( 𝑇 ∈ Cat ∧ ( Id ‘ 𝑇 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝐼 ‘ 𝑥 ) , ( 𝐽 ‘ 𝑦 ) ⟩ ) ) )
152	141 151	sylib	⊢ ( 𝜑 → ( 𝑇 ∈ Cat ∧ ( Id ‘ 𝑇 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝐼 ‘ 𝑥 ) , ( 𝐽 ‘ 𝑦 ) ⟩ ) ) )

Metamath Proof Explorer

Theorem xpccatid

Proof