xpccatid - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > xpccatid		Structured version Visualization version GIF version

Theorem xpccatid 16828

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

**Hypotheses**
Ref	Expression
xpccat.t	⊢ 𝑇 = (𝐶 ×_c 𝐷)
xpccat.c	⊢ (𝜑 → 𝐶 ∈ Cat)
xpccat.d	⊢ (𝜑 → 𝐷 ∈ Cat)
xpccat.x	⊢ 𝑋 = (Base‘𝐶)
xpccat.y	⊢ 𝑌 = (Base‘𝐷)
xpccat.i	⊢ 𝐼 = (Id‘𝐶)
xpccat.j	⊢ 𝐽 = (Id‘𝐷)

**Assertion**
Ref	Expression
xpccatid	⊢ (𝜑 → (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐼‘𝑥), (𝐽‘𝑦)⟩)))

Distinct variable groups: 𝑥,𝑦,𝐼 𝑥,𝐽,𝑦 𝑥,𝐶,𝑦 𝜑,𝑥,𝑦 𝑥,𝑋,𝑦 𝑥,𝐷,𝑦 𝑥,𝑌,𝑦 Allowed substitution hints: 𝑇(𝑥,𝑦)

Proof of Theorem xpccatid Dummy variables 𝑓 𝑔 ℎ 𝑠 𝑡 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xpccat.t	. . . . 5 ⊢ 𝑇 = (𝐶 ×_c 𝐷)
2		xpccat.x	. . . . 5 ⊢ 𝑋 = (Base‘𝐶)
3		xpccat.y	. . . . 5 ⊢ 𝑌 = (Base‘𝐷)
4	1, 2, 3	xpcbas 16818	. . . 4 ⊢ (𝑋 × 𝑌) = (Base‘𝑇)
5	4	a1i 11	. . 3 ⊢ (𝜑 → (𝑋 × 𝑌) = (Base‘𝑇))
6		eqidd 2623	. . 3 ⊢ (𝜑 → (Hom ‘𝑇) = (Hom ‘𝑇))
7		eqidd 2623	. . 3 ⊢ (𝜑 → (comp‘𝑇) = (comp‘𝑇))
8		ovex 6678	. . . . 5 ⊢ (𝐶 ×_c 𝐷) ∈ V
9	1, 8	eqeltri 2697	. . . 4 ⊢ 𝑇 ∈ V
10	9	a1i 11	. . 3 ⊢ (𝜑 → 𝑇 ∈ V)
11		biid 251	. . 3 ⊢ (((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣))) ↔ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣))))
12		eqid 2622	. . . . . 6 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
13		xpccat.i	. . . . . 6 ⊢ 𝐼 = (Id‘𝐶)
14		xpccat.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ Cat)
15	14	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝐶 ∈ Cat)
16		xp1st 7198	. . . . . . 7 ⊢ (𝑡 ∈ (𝑋 × 𝑌) → (1^st ‘𝑡) ∈ 𝑋)
17	16	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (1^st ‘𝑡) ∈ 𝑋)
18	2, 12, 13, 15, 17	catidcl 16343	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (𝐼‘(1^st ‘𝑡)) ∈ ((1^st ‘𝑡)(Hom ‘𝐶)(1^st ‘𝑡)))
19		eqid 2622	. . . . . 6 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
20		xpccat.j	. . . . . 6 ⊢ 𝐽 = (Id‘𝐷)
21		xpccat.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ Cat)
22	21	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝐷 ∈ Cat)
23		xp2nd 7199	. . . . . . 7 ⊢ (𝑡 ∈ (𝑋 × 𝑌) → (2^nd ‘𝑡) ∈ 𝑌)
24	23	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (2^nd ‘𝑡) ∈ 𝑌)
25	3, 19, 20, 22, 24	catidcl 16343	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (𝐽‘(2^nd ‘𝑡)) ∈ ((2^nd ‘𝑡)(Hom ‘𝐷)(2^nd ‘𝑡)))
26		opelxpi 5148	. . . . 5 ⊢ (((𝐼‘(1^st ‘𝑡)) ∈ ((1^st ‘𝑡)(Hom ‘𝐶)(1^st ‘𝑡)) ∧ (𝐽‘(2^nd ‘𝑡)) ∈ ((2^nd ‘𝑡)(Hom ‘𝐷)(2^nd ‘𝑡))) → ⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩ ∈ (((1^st ‘𝑡)(Hom ‘𝐶)(1^st ‘𝑡)) × ((2^nd ‘𝑡)(Hom ‘𝐷)(2^nd ‘𝑡))))
27	18, 25, 26	syl2anc 693	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → ⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩ ∈ (((1^st ‘𝑡)(Hom ‘𝐶)(1^st ‘𝑡)) × ((2^nd ‘𝑡)(Hom ‘𝐷)(2^nd ‘𝑡))))
28		eqid 2622	. . . . 5 ⊢ (Hom ‘𝑇) = (Hom ‘𝑇)
29		simpr 477	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝑡 ∈ (𝑋 × 𝑌))
30	1, 4, 12, 19, 28, 29, 29	xpchom 16820	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (𝑡(Hom ‘𝑇)𝑡) = (((1^st ‘𝑡)(Hom ‘𝐶)(1^st ‘𝑡)) × ((2^nd ‘𝑡)(Hom ‘𝐷)(2^nd ‘𝑡))))
31	27, 30	eleqtrrd 2704	. . 3 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → ⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩ ∈ (𝑡(Hom ‘𝑇)𝑡))
32		fvex 6201	. . . . . . . 8 ⊢ (𝐼‘(1^st ‘𝑡)) ∈ V
33		fvex 6201	. . . . . . . 8 ⊢ (𝐽‘(2^nd ‘𝑡)) ∈ V
34	32, 33	op1st 7176	. . . . . . 7 ⊢ (1^st ‘⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩) = (𝐼‘(1^st ‘𝑡))
35	34	oveq1i 6660	. . . . . 6 ⊢ ((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 ‘𝑓))
36	14	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝐶 ∈ Cat)
37		simpr1l 1118	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑠 ∈ (𝑋 × 𝑌))
38		xp1st 7198	. . . . . . . 8 ⊢ (𝑠 ∈ (𝑋 × 𝑌) → (1^st ‘𝑠) ∈ 𝑋)
39	37, 38	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^st ‘𝑠) ∈ 𝑋)
40		eqid 2622	. . . . . . 7 ⊢ (comp‘𝐶) = (comp‘𝐶)
41		simpr1r 1119	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑡 ∈ (𝑋 × 𝑌))
42	41, 16	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^st ‘𝑡) ∈ 𝑋)
43		simpr31 1151	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡))
44	1, 4, 12, 19, 28, 37, 41	xpchom 16820	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑠(Hom ‘𝑇)𝑡) = (((1^st ‘𝑠)(Hom ‘𝐶)(1^st ‘𝑡)) × ((2^nd ‘𝑠)(Hom ‘𝐷)(2^nd ‘𝑡))))
45	43, 44	eleqtrd 2703	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 ∈ (((1^st ‘𝑠)(Hom ‘𝐶)(1^st ‘𝑡)) × ((2^nd ‘𝑠)(Hom ‘𝐷)(2^nd ‘𝑡))))
46		xp1st 7198	. . . . . . . 8 ⊢ (𝑓 ∈ (((1^st ‘𝑠)(Hom ‘𝐶)(1^st ‘𝑡)) × ((2^nd ‘𝑠)(Hom ‘𝐷)(2^nd ‘𝑡))) → (1^st ‘𝑓) ∈ ((1^st ‘𝑠)(Hom ‘𝐶)(1^st ‘𝑡)))
47	45, 46	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^st ‘𝑓) ∈ ((1^st ‘𝑠)(Hom ‘𝐶)(1^st ‘𝑡)))
48	2, 12, 13, 36, 39, 40, 42, 47	catlid 16344	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((𝐼‘(1^st ‘𝑡))(⟨(1^st ‘𝑠), (1^st ‘𝑡)⟩(comp‘𝐶)(1^st ‘𝑡))(1^st ‘𝑓)) = (1^st ‘𝑓))
49	35, 48	syl5eq 2668	. . . . 5 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1^st ‘⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩)(⟨(1^st ‘𝑠), (1^st ‘𝑡)⟩(comp‘𝐶)(1^st ‘𝑡))(1^st ‘𝑓)) = (1^st ‘𝑓))
50	32, 33	op2nd 7177	. . . . . . 7 ⊢ (2^nd ‘⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩) = (𝐽‘(2^nd ‘𝑡))
51	50	oveq1i 6660	. . . . . 6 ⊢ ((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 ‘𝑓))
52	21	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝐷 ∈ Cat)
53		xp2nd 7199	. . . . . . . 8 ⊢ (𝑠 ∈ (𝑋 × 𝑌) → (2^nd ‘𝑠) ∈ 𝑌)
54	37, 53	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^nd ‘𝑠) ∈ 𝑌)
55		eqid 2622	. . . . . . 7 ⊢ (comp‘𝐷) = (comp‘𝐷)
56	41, 23	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^nd ‘𝑡) ∈ 𝑌)
57		xp2nd 7199	. . . . . . . 8 ⊢ (𝑓 ∈ (((1^st ‘𝑠)(Hom ‘𝐶)(1^st ‘𝑡)) × ((2^nd ‘𝑠)(Hom ‘𝐷)(2^nd ‘𝑡))) → (2^nd ‘𝑓) ∈ ((2^nd ‘𝑠)(Hom ‘𝐷)(2^nd ‘𝑡)))
58	45, 57	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^nd ‘𝑓) ∈ ((2^nd ‘𝑠)(Hom ‘𝐷)(2^nd ‘𝑡)))
59	3, 19, 20, 52, 54, 55, 56, 58	catlid 16344	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((𝐽‘(2^nd ‘𝑡))(⟨(2^nd ‘𝑠), (2^nd ‘𝑡)⟩(comp‘𝐷)(2^nd ‘𝑡))(2^nd ‘𝑓)) = (2^nd ‘𝑓))
60	51, 59	syl5eq 2668	. . . . 5 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2^nd ‘⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩)(⟨(2^nd ‘𝑠), (2^nd ‘𝑡)⟩(comp‘𝐷)(2^nd ‘𝑡))(2^nd ‘𝑓)) = (2^nd ‘𝑓))
61	49, 60	opeq12d 4410	. . . 4 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑓)⟩)
62		eqid 2622	. . . . 5 ⊢ (comp‘𝑇) = (comp‘𝑇)
63	41, 31	syldan 487	. . . . 5 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩ ∈ (𝑡(Hom ‘𝑇)𝑡))
64	1, 4, 28, 40, 55, 62, 37, 41, 41, 43, 63	xpcco 16823	. . . 4 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑓))⟩)
65		1st2nd2 7205	. . . . 5 ⊢ (𝑓 ∈ (((1^st ‘𝑠)(Hom ‘𝐶)(1^st ‘𝑡)) × ((2^nd ‘𝑠)(Hom ‘𝐷)(2^nd ‘𝑡))) → 𝑓 = ⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩)
66	45, 65	syl 17	. . . 4 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 = ⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩)
67	61, 64, 66	3eqtr4d 2666	. . 3 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑡)𝑓) = 𝑓)
68	34	oveq2i 6661	. . . . . 6 ⊢ ((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 ‘𝑡)))
69		simpr2l 1120	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑢 ∈ (𝑋 × 𝑌))
70		xp1st 7198	. . . . . . . 8 ⊢ (𝑢 ∈ (𝑋 × 𝑌) → (1^st ‘𝑢) ∈ 𝑋)
71	69, 70	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^st ‘𝑢) ∈ 𝑋)
72		simpr32 1152	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢))
73	1, 4, 12, 19, 28, 41, 69	xpchom 16820	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑡(Hom ‘𝑇)𝑢) = (((1^st ‘𝑡)(Hom ‘𝐶)(1^st ‘𝑢)) × ((2^nd ‘𝑡)(Hom ‘𝐷)(2^nd ‘𝑢))))
74	72, 73	eleqtrd 2703	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 ∈ (((1^st ‘𝑡)(Hom ‘𝐶)(1^st ‘𝑢)) × ((2^nd ‘𝑡)(Hom ‘𝐷)(2^nd ‘𝑢))))
75		xp1st 7198	. . . . . . . 8 ⊢ (𝑔 ∈ (((1^st ‘𝑡)(Hom ‘𝐶)(1^st ‘𝑢)) × ((2^nd ‘𝑡)(Hom ‘𝐷)(2^nd ‘𝑢))) → (1^st ‘𝑔) ∈ ((1^st ‘𝑡)(Hom ‘𝐶)(1^st ‘𝑢)))
76	74, 75	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^st ‘𝑔) ∈ ((1^st ‘𝑡)(Hom ‘𝐶)(1^st ‘𝑢)))
77	2, 12, 13, 36, 42, 40, 71, 76	catrid 16345	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1^st ‘𝑔)(⟨(1^st ‘𝑡), (1^st ‘𝑡)⟩(comp‘𝐶)(1^st ‘𝑢))(𝐼‘(1^st ‘𝑡))) = (1^st ‘𝑔))
78	68, 77	syl5eq 2668	. . . . 5 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1^st ‘𝑔)(⟨(1^st ‘𝑡), (1^st ‘𝑡)⟩(comp‘𝐶)(1^st ‘𝑢))(1^st ‘⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩)) = (1^st ‘𝑔))
79	50	oveq2i 6661	. . . . . 6 ⊢ ((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 ‘𝑡)))
80		xp2nd 7199	. . . . . . . 8 ⊢ (𝑢 ∈ (𝑋 × 𝑌) → (2^nd ‘𝑢) ∈ 𝑌)
81	69, 80	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^nd ‘𝑢) ∈ 𝑌)
82		xp2nd 7199	. . . . . . . 8 ⊢ (𝑔 ∈ (((1^st ‘𝑡)(Hom ‘𝐶)(1^st ‘𝑢)) × ((2^nd ‘𝑡)(Hom ‘𝐷)(2^nd ‘𝑢))) → (2^nd ‘𝑔) ∈ ((2^nd ‘𝑡)(Hom ‘𝐷)(2^nd ‘𝑢)))
83	74, 82	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^nd ‘𝑔) ∈ ((2^nd ‘𝑡)(Hom ‘𝐷)(2^nd ‘𝑢)))
84	3, 19, 20, 52, 56, 55, 81, 83	catrid 16345	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2^nd ‘𝑔)(⟨(2^nd ‘𝑡), (2^nd ‘𝑡)⟩(comp‘𝐷)(2^nd ‘𝑢))(𝐽‘(2^nd ‘𝑡))) = (2^nd ‘𝑔))
85	79, 84	syl5eq 2668	. . . . 5 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2^nd ‘𝑔)(⟨(2^nd ‘𝑡), (2^nd ‘𝑡)⟩(comp‘𝐷)(2^nd ‘𝑢))(2^nd ‘⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩)) = (2^nd ‘𝑔))
86	78, 85	opeq12d 4410	. . . 4 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑔)⟩)
87	1, 4, 28, 40, 55, 62, 41, 41, 69, 63, 72	xpcco 16823	. . . 4 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑡))⟩))⟩)
88		1st2nd2 7205	. . . . 5 ⊢ (𝑔 ∈ (((1^st ‘𝑡)(Hom ‘𝐶)(1^st ‘𝑢)) × ((2^nd ‘𝑡)(Hom ‘𝐷)(2^nd ‘𝑢))) → 𝑔 = ⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩)
89	74, 88	syl 17	. . . 4 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 = ⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩)
90	86, 87, 89	3eqtr4d 2666	. . 3 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(⟨𝑡, 𝑡⟩(comp‘𝑇)𝑢)⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩) = 𝑔)
91	2, 12, 40, 36, 39, 42, 71, 47, 76	catcocl 16346	. . . . 5 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1^st ‘𝑔)(⟨(1^st ‘𝑠), (1^st ‘𝑡)⟩(comp‘𝐶)(1^st ‘𝑢))(1^st ‘𝑓)) ∈ ((1^st ‘𝑠)(Hom ‘𝐶)(1^st ‘𝑢)))
92	3, 19, 55, 52, 54, 56, 81, 58, 83	catcocl 16346	. . . . 5 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2^nd ‘𝑔)(⟨(2^nd ‘𝑠), (2^nd ‘𝑡)⟩(comp‘𝐷)(2^nd ‘𝑢))(2^nd ‘𝑓)) ∈ ((2^nd ‘𝑠)(Hom ‘𝐷)(2^nd ‘𝑢)))
93		opelxpi 5148	. . . . 5 ⊢ ((((1^st ‘𝑔)(⟨(1^st ‘𝑠), (1^st ‘𝑡)⟩(comp‘𝐶)(1^st ‘𝑢))(1^st ‘𝑓)) ∈ ((1^st ‘𝑠)(Hom ‘𝐶)(1^st ‘𝑢)) ∧ ((2^nd ‘𝑔)(⟨(2^nd ‘𝑠), (2^nd ‘𝑡)⟩(comp‘𝐷)(2^nd ‘𝑢))(2^nd ‘𝑓)) ∈ ((2^nd ‘𝑠)(Hom ‘𝐷)(2^nd ‘𝑢))) → ⟨((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 ‘𝑢))))
94	91, 92, 93	syl2anc 693	. . . 4 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑢))))
95	1, 4, 28, 40, 55, 62, 37, 41, 69, 43, 72	xpcco 16823	. . . 4 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑓))⟩)
96	1, 4, 12, 19, 28, 37, 69	xpchom 16820	. . . 4 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑠(Hom ‘𝑇)𝑢) = (((1^st ‘𝑠)(Hom ‘𝐶)(1^st ‘𝑢)) × ((2^nd ‘𝑠)(Hom ‘𝐷)(2^nd ‘𝑢))))
97	94, 95, 96	3eltr4d 2716	. . 3 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓) ∈ (𝑠(Hom ‘𝑇)𝑢))
98		simpr2r 1121	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑣 ∈ (𝑋 × 𝑌))
99		xp1st 7198	. . . . . . . 8 ⊢ (𝑣 ∈ (𝑋 × 𝑌) → (1^st ‘𝑣) ∈ 𝑋)
100	98, 99	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^st ‘𝑣) ∈ 𝑋)
101		simpr33 1153	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ℎ ∈ (𝑢(Hom ‘𝑇)𝑣))
102	1, 4, 12, 19, 28, 69, 98	xpchom 16820	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑢(Hom ‘𝑇)𝑣) = (((1^st ‘𝑢)(Hom ‘𝐶)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝐷)(2^nd ‘𝑣))))
103	101, 102	eleqtrd 2703	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ℎ ∈ (((1^st ‘𝑢)(Hom ‘𝐶)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝐷)(2^nd ‘𝑣))))
104		xp1st 7198	. . . . . . . 8 ⊢ (ℎ ∈ (((1^st ‘𝑢)(Hom ‘𝐶)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝐷)(2^nd ‘𝑣))) → (1^st ‘ℎ) ∈ ((1^st ‘𝑢)(Hom ‘𝐶)(1^st ‘𝑣)))
105	103, 104	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^st ‘ℎ) ∈ ((1^st ‘𝑢)(Hom ‘𝐶)(1^st ‘𝑣)))
106	2, 12, 40, 36, 39, 42, 71, 47, 76, 100, 105	catass 16347	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑓))))
107	1, 4, 28, 40, 55, 62, 41, 69, 98, 72, 101	xpcco 16823	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑔))⟩)
108	107	fveq2d 6195	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑔))⟩))
109		ovex 6678	. . . . . . . . 9 ⊢ ((1^st ‘ℎ)(⟨(1^st ‘𝑡), (1^st ‘𝑢)⟩(comp‘𝐶)(1^st ‘𝑣))(1^st ‘𝑔)) ∈ V
110		ovex 6678	. . . . . . . . 9 ⊢ ((2^nd ‘ℎ)(⟨(2^nd ‘𝑡), (2^nd ‘𝑢)⟩(comp‘𝐷)(2^nd ‘𝑣))(2^nd ‘𝑔)) ∈ V
111	109, 110	op1st 7176	. . . . . . . 8 ⊢ (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 ‘𝑔))
112	108, 111	syl6eq 2672	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^st ‘(ℎ(⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)) = ((1^st ‘ℎ)(⟨(1^st ‘𝑡), (1^st ‘𝑢)⟩(comp‘𝐶)(1^st ‘𝑣))(1^st ‘𝑔)))
113	112	oveq1d 6665	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑓)))
114	95	fveq2d 6195	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑓))⟩))
115		ovex 6678	. . . . . . . . 9 ⊢ ((1^st ‘𝑔)(⟨(1^st ‘𝑠), (1^st ‘𝑡)⟩(comp‘𝐶)(1^st ‘𝑢))(1^st ‘𝑓)) ∈ V
116		ovex 6678	. . . . . . . . 9 ⊢ ((2^nd ‘𝑔)(⟨(2^nd ‘𝑠), (2^nd ‘𝑡)⟩(comp‘𝐷)(2^nd ‘𝑢))(2^nd ‘𝑓)) ∈ V
117	115, 116	op1st 7176	. . . . . . . 8 ⊢ (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 ‘𝑓))
118	114, 117	syl6eq 2672	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^st ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)) = ((1^st ‘𝑔)(⟨(1^st ‘𝑠), (1^st ‘𝑡)⟩(comp‘𝐶)(1^st ‘𝑢))(1^st ‘𝑓)))
119	118	oveq2d 6666	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑓))))
120	106, 113, 119	3eqtr4d 2666	. . . . 5 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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‘𝑇)𝑢)𝑓))))
121		xp2nd 7199	. . . . . . . 8 ⊢ (𝑣 ∈ (𝑋 × 𝑌) → (2^nd ‘𝑣) ∈ 𝑌)
122	98, 121	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^nd ‘𝑣) ∈ 𝑌)
123		xp2nd 7199	. . . . . . . 8 ⊢ (ℎ ∈ (((1^st ‘𝑢)(Hom ‘𝐶)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝐷)(2^nd ‘𝑣))) → (2^nd ‘ℎ) ∈ ((2^nd ‘𝑢)(Hom ‘𝐷)(2^nd ‘𝑣)))
124	103, 123	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^nd ‘ℎ) ∈ ((2^nd ‘𝑢)(Hom ‘𝐷)(2^nd ‘𝑣)))
125	3, 19, 55, 52, 54, 56, 81, 58, 83, 122, 124	catass 16347	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑓))))
126	107	fveq2d 6195	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑔))⟩))
127	109, 110	op2nd 7177	. . . . . . . 8 ⊢ (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 ‘𝑔))
128	126, 127	syl6eq 2672	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^nd ‘(ℎ(⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)) = ((2^nd ‘ℎ)(⟨(2^nd ‘𝑡), (2^nd ‘𝑢)⟩(comp‘𝐷)(2^nd ‘𝑣))(2^nd ‘𝑔)))
129	128	oveq1d 6665	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑓)))
130	95	fveq2d 6195	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑓))⟩))
131	115, 116	op2nd 7177	. . . . . . . 8 ⊢ (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 ‘𝑓))
132	130, 131	syl6eq 2672	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^nd ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)) = ((2^nd ‘𝑔)(⟨(2^nd ‘𝑠), (2^nd ‘𝑡)⟩(comp‘𝐷)(2^nd ‘𝑢))(2^nd ‘𝑓)))
133	132	oveq2d 6666	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑓))))
134	125, 129, 133	3eqtr4d 2666	. . . . 5 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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‘𝑇)𝑢)𝑓))))
135	120, 134	opeq12d 4410	. . . 4 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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‘𝑇)𝑢)𝑓)))⟩)
136	2, 12, 40, 36, 42, 71, 100, 76, 105	catcocl 16346	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1^st ‘ℎ)(⟨(1^st ‘𝑡), (1^st ‘𝑢)⟩(comp‘𝐶)(1^st ‘𝑣))(1^st ‘𝑔)) ∈ ((1^st ‘𝑡)(Hom ‘𝐶)(1^st ‘𝑣)))
137	3, 19, 55, 52, 56, 81, 122, 83, 124	catcocl 16346	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2^nd ‘ℎ)(⟨(2^nd ‘𝑡), (2^nd ‘𝑢)⟩(comp‘𝐷)(2^nd ‘𝑣))(2^nd ‘𝑔)) ∈ ((2^nd ‘𝑡)(Hom ‘𝐷)(2^nd ‘𝑣)))
138		opelxpi 5148	. . . . . . 7 ⊢ ((((1^st ‘ℎ)(⟨(1^st ‘𝑡), (1^st ‘𝑢)⟩(comp‘𝐶)(1^st ‘𝑣))(1^st ‘𝑔)) ∈ ((1^st ‘𝑡)(Hom ‘𝐶)(1^st ‘𝑣)) ∧ ((2^nd ‘ℎ)(⟨(2^nd ‘𝑡), (2^nd ‘𝑢)⟩(comp‘𝐷)(2^nd ‘𝑣))(2^nd ‘𝑔)) ∈ ((2^nd ‘𝑡)(Hom ‘𝐷)(2^nd ‘𝑣))) → ⟨((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 ‘𝑣))))
139	136, 137, 138	syl2anc 693	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑣))))
140	1, 4, 12, 19, 28, 41, 98	xpchom 16820	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑡(Hom ‘𝑇)𝑣) = (((1^st ‘𝑡)(Hom ‘𝐶)(1^st ‘𝑣)) × ((2^nd ‘𝑡)(Hom ‘𝐷)(2^nd ‘𝑣))))
141	139, 107, 140	3eltr4d 2716	. . . . 5 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (ℎ(⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔) ∈ (𝑡(Hom ‘𝑇)𝑣))
142	1, 4, 28, 40, 55, 62, 37, 41, 98, 43, 141	xpcco 16823	. . . 4 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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 ‘𝑓))⟩)
143	1, 4, 28, 40, 55, 62, 37, 69, 98, 97, 101	xpcco 16823	. . . 4 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(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‘𝑇)𝑢)𝑓)))⟩)
144	135, 142, 143	3eqtr4d 2666	. . 3 ⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((ℎ(⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑣)𝑓) = (ℎ(⟨𝑠, 𝑢⟩(comp‘𝑇)𝑣)(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)))
145	5, 6, 7, 10, 11, 31, 67, 90, 97, 144	iscatd2 16342	. 2 ⊢ (𝜑 → (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩)))
146		vex 3203	. . . . . . . 8 ⊢ 𝑥 ∈ V
147		vex 3203	. . . . . . . 8 ⊢ 𝑦 ∈ V
148	146, 147	op1std 7178	. . . . . . 7 ⊢ (𝑡 = ⟨𝑥, 𝑦⟩ → (1^st ‘𝑡) = 𝑥)
149	148	fveq2d 6195	. . . . . 6 ⊢ (𝑡 = ⟨𝑥, 𝑦⟩ → (𝐼‘(1^st ‘𝑡)) = (𝐼‘𝑥))
150	146, 147	op2ndd 7179	. . . . . . 7 ⊢ (𝑡 = ⟨𝑥, 𝑦⟩ → (2^nd ‘𝑡) = 𝑦)
151	150	fveq2d 6195	. . . . . 6 ⊢ (𝑡 = ⟨𝑥, 𝑦⟩ → (𝐽‘(2^nd ‘𝑡)) = (𝐽‘𝑦))
152	149, 151	opeq12d 4410	. . . . 5 ⊢ (𝑡 = ⟨𝑥, 𝑦⟩ → ⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩ = ⟨(𝐼‘𝑥), (𝐽‘𝑦)⟩)
153	152	mpt2mpt 6752	. . . 4 ⊢ (𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐼‘𝑥), (𝐽‘𝑦)⟩)
154	153	eqeq2i 2634	. . 3 ⊢ ((Id‘𝑇) = (𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩) ↔ (Id‘𝑇) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐼‘𝑥), (𝐽‘𝑦)⟩))
155	154	anbi2i 730	. 2 ⊢ ((𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1^st ‘𝑡)), (𝐽‘(2^nd ‘𝑡))⟩)) ↔ (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐼‘𝑥), (𝐽‘𝑦)⟩)))
156	145, 155	sylib 208	1 ⊢ (𝜑 → (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐼‘𝑥), (𝐽‘𝑦)⟩)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 Vcvv 3200 ⟨cop 4183 ↦ cmpt 4729 × cxp 5112 ‘cfv 5888 (class class class)co 6650 ↦ cmpt2 6652 1^st c1st 7166 2^nd c2nd 7167 Basecbs 15857 Hom chom 15952 compcco 15953 Catccat 16325 Idccid 16326 ×_c cxpc 16808

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-fz 12327 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-hom 15966 df-cco 15967 df-cat 16329 df-cid 16330 df-xpc 16812

This theorem is referenced by: xpcid 16829 xpccat 16830

W3C validator