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

Theorem xpccatid 16875
 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.
StepHypRef Expression
1 xpccat.t . . . . 5 𝑇 = (𝐶 ×c 𝐷)
2 xpccat.x . . . . 5 𝑋 = (Base‘𝐶)
3 xpccat.y . . . . 5 𝑌 = (Base‘𝐷)
41, 2, 3xpcbas 16865 . . . 4 (𝑋 × 𝑌) = (Base‘𝑇)
54a1i 11 . . 3 (𝜑 → (𝑋 × 𝑌) = (Base‘𝑇))
6 eqidd 2652 . . 3 (𝜑 → (Hom ‘𝑇) = (Hom ‘𝑇))
7 eqidd 2652 . . 3 (𝜑 → (comp‘𝑇) = (comp‘𝑇))
8 ovex 6718 . . . . 5 (𝐶 ×c 𝐷) ∈ V
91, 8eqeltri 2726 . . . 4 𝑇 ∈ V
109a1i 11 . . 3 (𝜑𝑇 ∈ V)
11 biid 251 . . 3 (((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣))) ↔ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣))))
12 eqid 2651 . . . . . 6 (Hom ‘𝐶) = (Hom ‘𝐶)
13 xpccat.i . . . . . 6 𝐼 = (Id‘𝐶)
14 xpccat.c . . . . . . 7 (𝜑𝐶 ∈ Cat)
1514adantr 480 . . . . . 6 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → 𝐶 ∈ Cat)
16 xp1st 7242 . . . . . . 7 (𝑡 ∈ (𝑋 × 𝑌) → (1st𝑡) ∈ 𝑋)
1716adantl 481 . . . . . 6 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → (1st𝑡) ∈ 𝑋)
182, 12, 13, 15, 17catidcl 16390 . . . . 5 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → (𝐼‘(1st𝑡)) ∈ ((1st𝑡)(Hom ‘𝐶)(1st𝑡)))
19 eqid 2651 . . . . . 6 (Hom ‘𝐷) = (Hom ‘𝐷)
20 xpccat.j . . . . . 6 𝐽 = (Id‘𝐷)
21 xpccat.d . . . . . . 7 (𝜑𝐷 ∈ Cat)
2221adantr 480 . . . . . 6 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → 𝐷 ∈ Cat)
23 xp2nd 7243 . . . . . . 7 (𝑡 ∈ (𝑋 × 𝑌) → (2nd𝑡) ∈ 𝑌)
2423adantl 481 . . . . . 6 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → (2nd𝑡) ∈ 𝑌)
253, 19, 20, 22, 24catidcl 16390 . . . . 5 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → (𝐽‘(2nd𝑡)) ∈ ((2nd𝑡)(Hom ‘𝐷)(2nd𝑡)))
26 opelxpi 5182 . . . . 5 (((𝐼‘(1st𝑡)) ∈ ((1st𝑡)(Hom ‘𝐶)(1st𝑡)) ∧ (𝐽‘(2nd𝑡)) ∈ ((2nd𝑡)(Hom ‘𝐷)(2nd𝑡))) → ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩ ∈ (((1st𝑡)(Hom ‘𝐶)(1st𝑡)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑡))))
2718, 25, 26syl2anc 694 . . . 4 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩ ∈ (((1st𝑡)(Hom ‘𝐶)(1st𝑡)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑡))))
28 eqid 2651 . . . . 5 (Hom ‘𝑇) = (Hom ‘𝑇)
29 simpr 476 . . . . 5 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → 𝑡 ∈ (𝑋 × 𝑌))
301, 4, 12, 19, 28, 29, 29xpchom 16867 . . . 4 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → (𝑡(Hom ‘𝑇)𝑡) = (((1st𝑡)(Hom ‘𝐶)(1st𝑡)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑡))))
3127, 30eleqtrrd 2733 . . 3 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩ ∈ (𝑡(Hom ‘𝑇)𝑡))
32 fvex 6239 . . . . . . . 8 (𝐼‘(1st𝑡)) ∈ V
33 fvex 6239 . . . . . . . 8 (𝐽‘(2nd𝑡)) ∈ V
3432, 33op1st 7218 . . . . . . 7 (1st ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩) = (𝐼‘(1st𝑡))
3534oveq1i 6700 . . . . . 6 ((1st ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑡))(1st𝑓)) = ((𝐼‘(1st𝑡))(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑡))(1st𝑓))
3614adantr 480 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝐶 ∈ Cat)
37 simpr1l 1138 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑠 ∈ (𝑋 × 𝑌))
38 xp1st 7242 . . . . . . . 8 (𝑠 ∈ (𝑋 × 𝑌) → (1st𝑠) ∈ 𝑋)
3937, 38syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st𝑠) ∈ 𝑋)
40 eqid 2651 . . . . . . 7 (comp‘𝐶) = (comp‘𝐶)
41 simpr1r 1139 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑡 ∈ (𝑋 × 𝑌))
4241, 16syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st𝑡) ∈ 𝑋)
43 simpr31 1171 . . . . . . . . 9 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡))
441, 4, 12, 19, 28, 37, 41xpchom 16867 . . . . . . . . 9 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑠(Hom ‘𝑇)𝑡) = (((1st𝑠)(Hom ‘𝐶)(1st𝑡)) × ((2nd𝑠)(Hom ‘𝐷)(2nd𝑡))))
4543, 44eleqtrd 2732 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 ∈ (((1st𝑠)(Hom ‘𝐶)(1st𝑡)) × ((2nd𝑠)(Hom ‘𝐷)(2nd𝑡))))
46 xp1st 7242 . . . . . . . 8 (𝑓 ∈ (((1st𝑠)(Hom ‘𝐶)(1st𝑡)) × ((2nd𝑠)(Hom ‘𝐷)(2nd𝑡))) → (1st𝑓) ∈ ((1st𝑠)(Hom ‘𝐶)(1st𝑡)))
4745, 46syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st𝑓) ∈ ((1st𝑠)(Hom ‘𝐶)(1st𝑡)))
482, 12, 13, 36, 39, 40, 42, 47catlid 16391 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((𝐼‘(1st𝑡))(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑡))(1st𝑓)) = (1st𝑓))
4935, 48syl5eq 2697 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑡))(1st𝑓)) = (1st𝑓))
5032, 33op2nd 7219 . . . . . . 7 (2nd ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩) = (𝐽‘(2nd𝑡))
5150oveq1i 6700 . . . . . 6 ((2nd ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑡))(2nd𝑓)) = ((𝐽‘(2nd𝑡))(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑡))(2nd𝑓))
5221adantr 480 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝐷 ∈ Cat)
53 xp2nd 7243 . . . . . . . 8 (𝑠 ∈ (𝑋 × 𝑌) → (2nd𝑠) ∈ 𝑌)
5437, 53syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd𝑠) ∈ 𝑌)
55 eqid 2651 . . . . . . 7 (comp‘𝐷) = (comp‘𝐷)
5641, 23syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd𝑡) ∈ 𝑌)
57 xp2nd 7243 . . . . . . . 8 (𝑓 ∈ (((1st𝑠)(Hom ‘𝐶)(1st𝑡)) × ((2nd𝑠)(Hom ‘𝐷)(2nd𝑡))) → (2nd𝑓) ∈ ((2nd𝑠)(Hom ‘𝐷)(2nd𝑡)))
5845, 57syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd𝑓) ∈ ((2nd𝑠)(Hom ‘𝐷)(2nd𝑡)))
593, 19, 20, 52, 54, 55, 56, 58catlid 16391 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((𝐽‘(2nd𝑡))(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑡))(2nd𝑓)) = (2nd𝑓))
6051, 59syl5eq 2697 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑡))(2nd𝑓)) = (2nd𝑓))
6149, 60opeq12d 4441 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ⟨((1st ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑡))(1st𝑓)), ((2nd ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑡))(2nd𝑓))⟩ = ⟨(1st𝑓), (2nd𝑓)⟩)
62 eqid 2651 . . . . 5 (comp‘𝑇) = (comp‘𝑇)
6341, 31syldan 486 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩ ∈ (𝑡(Hom ‘𝑇)𝑡))
641, 4, 28, 40, 55, 62, 37, 41, 41, 43, 63xpcco 16870 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑡)𝑓) = ⟨((1st ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑡))(1st𝑓)), ((2nd ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑡))(2nd𝑓))⟩)
65 1st2nd2 7249 . . . . 5 (𝑓 ∈ (((1st𝑠)(Hom ‘𝐶)(1st𝑡)) × ((2nd𝑠)(Hom ‘𝐷)(2nd𝑡))) → 𝑓 = ⟨(1st𝑓), (2nd𝑓)⟩)
6645, 65syl 17 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 = ⟨(1st𝑓), (2nd𝑓)⟩)
6761, 64, 663eqtr4d 2695 . . 3 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑡)𝑓) = 𝑓)
6834oveq2i 6701 . . . . . 6 ((1st𝑔)(⟨(1st𝑡), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)) = ((1st𝑔)(⟨(1st𝑡), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(𝐼‘(1st𝑡)))
69 simpr2l 1140 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑢 ∈ (𝑋 × 𝑌))
70 xp1st 7242 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (1st𝑢) ∈ 𝑋)
7169, 70syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st𝑢) ∈ 𝑋)
72 simpr32 1172 . . . . . . . . 9 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢))
731, 4, 12, 19, 28, 41, 69xpchom 16867 . . . . . . . . 9 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑡(Hom ‘𝑇)𝑢) = (((1st𝑡)(Hom ‘𝐶)(1st𝑢)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑢))))
7472, 73eleqtrd 2732 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 ∈ (((1st𝑡)(Hom ‘𝐶)(1st𝑢)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑢))))
75 xp1st 7242 . . . . . . . 8 (𝑔 ∈ (((1st𝑡)(Hom ‘𝐶)(1st𝑢)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑢))) → (1st𝑔) ∈ ((1st𝑡)(Hom ‘𝐶)(1st𝑢)))
7674, 75syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st𝑔) ∈ ((1st𝑡)(Hom ‘𝐶)(1st𝑢)))
772, 12, 13, 36, 42, 40, 71, 76catrid 16392 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st𝑔)(⟨(1st𝑡), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(𝐼‘(1st𝑡))) = (1st𝑔))
7868, 77syl5eq 2697 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st𝑔)(⟨(1st𝑡), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)) = (1st𝑔))
7950oveq2i 6701 . . . . . 6 ((2nd𝑔)(⟨(2nd𝑡), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)) = ((2nd𝑔)(⟨(2nd𝑡), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(𝐽‘(2nd𝑡)))
80 xp2nd 7243 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (2nd𝑢) ∈ 𝑌)
8169, 80syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd𝑢) ∈ 𝑌)
82 xp2nd 7243 . . . . . . . 8 (𝑔 ∈ (((1st𝑡)(Hom ‘𝐶)(1st𝑢)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑢))) → (2nd𝑔) ∈ ((2nd𝑡)(Hom ‘𝐷)(2nd𝑢)))
8374, 82syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd𝑔) ∈ ((2nd𝑡)(Hom ‘𝐷)(2nd𝑢)))
843, 19, 20, 52, 56, 55, 81, 83catrid 16392 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd𝑔)(⟨(2nd𝑡), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(𝐽‘(2nd𝑡))) = (2nd𝑔))
8579, 84syl5eq 2697 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd𝑔)(⟨(2nd𝑡), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)) = (2nd𝑔))
8678, 85opeq12d 4441 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ⟨((1st𝑔)(⟨(1st𝑡), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)), ((2nd𝑔)(⟨(2nd𝑡), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩))⟩ = ⟨(1st𝑔), (2nd𝑔)⟩)
871, 4, 28, 40, 55, 62, 41, 41, 69, 63, 72xpcco 16870 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(⟨𝑡, 𝑡⟩(comp‘𝑇)𝑢)⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩) = ⟨((1st𝑔)(⟨(1st𝑡), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)), ((2nd𝑔)(⟨(2nd𝑡), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩))⟩)
88 1st2nd2 7249 . . . . 5 (𝑔 ∈ (((1st𝑡)(Hom ‘𝐶)(1st𝑢)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑢))) → 𝑔 = ⟨(1st𝑔), (2nd𝑔)⟩)
8974, 88syl 17 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 = ⟨(1st𝑔), (2nd𝑔)⟩)
9086, 87, 893eqtr4d 2695 . . 3 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(⟨𝑡, 𝑡⟩(comp‘𝑇)𝑢)⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩) = 𝑔)
912, 12, 40, 36, 39, 42, 71, 47, 76catcocl 16393 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)) ∈ ((1st𝑠)(Hom ‘𝐶)(1st𝑢)))
923, 19, 55, 52, 54, 56, 81, 58, 83catcocl 16393 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓)) ∈ ((2nd𝑠)(Hom ‘𝐷)(2nd𝑢)))
93 opelxpi 5182 . . . . 5 ((((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)) ∈ ((1st𝑠)(Hom ‘𝐶)(1st𝑢)) ∧ ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓)) ∈ ((2nd𝑠)(Hom ‘𝐷)(2nd𝑢))) → ⟨((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)), ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))⟩ ∈ (((1st𝑠)(Hom ‘𝐶)(1st𝑢)) × ((2nd𝑠)(Hom ‘𝐷)(2nd𝑢))))
9491, 92, 93syl2anc 694 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ⟨((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)), ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))⟩ ∈ (((1st𝑠)(Hom ‘𝐶)(1st𝑢)) × ((2nd𝑠)(Hom ‘𝐷)(2nd𝑢))))
951, 4, 28, 40, 55, 62, 37, 41, 69, 43, 72xpcco 16870 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓) = ⟨((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)), ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))⟩)
961, 4, 12, 19, 28, 37, 69xpchom 16867 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑠(Hom ‘𝑇)𝑢) = (((1st𝑠)(Hom ‘𝐶)(1st𝑢)) × ((2nd𝑠)(Hom ‘𝐷)(2nd𝑢))))
9794, 95, 963eltr4d 2745 . . 3 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓) ∈ (𝑠(Hom ‘𝑇)𝑢))
98 simpr2r 1141 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑣 ∈ (𝑋 × 𝑌))
99 xp1st 7242 . . . . . . . 8 (𝑣 ∈ (𝑋 × 𝑌) → (1st𝑣) ∈ 𝑋)
10098, 99syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st𝑣) ∈ 𝑋)
101 simpr33 1173 . . . . . . . . 9 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ∈ (𝑢(Hom ‘𝑇)𝑣))
1021, 4, 12, 19, 28, 69, 98xpchom 16867 . . . . . . . . 9 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑢(Hom ‘𝑇)𝑣) = (((1st𝑢)(Hom ‘𝐶)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝐷)(2nd𝑣))))
103101, 102eleqtrd 2732 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ∈ (((1st𝑢)(Hom ‘𝐶)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝐷)(2nd𝑣))))
104 xp1st 7242 . . . . . . . 8 ( ∈ (((1st𝑢)(Hom ‘𝐶)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝐷)(2nd𝑣))) → (1st) ∈ ((1st𝑢)(Hom ‘𝐶)(1st𝑣)))
105103, 104syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st) ∈ ((1st𝑢)(Hom ‘𝐶)(1st𝑣)))
1062, 12, 40, 36, 39, 42, 71, 47, 76, 100, 105catass 16394 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔))(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑣))(1st𝑓)) = ((1st)(⟨(1st𝑠), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓))))
1071, 4, 28, 40, 55, 62, 41, 69, 98, 72, 101xpcco 16870 . . . . . . . . 9 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔) = ⟨((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)), ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))⟩)
108107fveq2d 6233 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)) = (1st ‘⟨((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)), ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))⟩))
109 ovex 6718 . . . . . . . . 9 ((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)) ∈ V
110 ovex 6718 . . . . . . . . 9 ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔)) ∈ V
111109, 110op1st 7218 . . . . . . . 8 (1st ‘⟨((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)), ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))⟩) = ((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔))
112108, 111syl6eq 2701 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)) = ((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)))
113112oveq1d 6705 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔))(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑣))(1st𝑓)) = (((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔))(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑣))(1st𝑓)))
11495fveq2d 6233 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)) = (1st ‘⟨((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)), ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))⟩))
115 ovex 6718 . . . . . . . . 9 ((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)) ∈ V
116 ovex 6718 . . . . . . . . 9 ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓)) ∈ V
117115, 116op1st 7218 . . . . . . . 8 (1st ‘⟨((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)), ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))⟩) = ((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓))
118114, 117syl6eq 2701 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)) = ((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)))
119118oveq2d 6706 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st)(⟨(1st𝑠), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓))) = ((1st)(⟨(1st𝑠), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓))))
120106, 113, 1193eqtr4d 2695 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔))(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑣))(1st𝑓)) = ((1st)(⟨(1st𝑠), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓))))
121 xp2nd 7243 . . . . . . . 8 (𝑣 ∈ (𝑋 × 𝑌) → (2nd𝑣) ∈ 𝑌)
12298, 121syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd𝑣) ∈ 𝑌)
123 xp2nd 7243 . . . . . . . 8 ( ∈ (((1st𝑢)(Hom ‘𝐶)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝐷)(2nd𝑣))) → (2nd) ∈ ((2nd𝑢)(Hom ‘𝐷)(2nd𝑣)))
124103, 123syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd) ∈ ((2nd𝑢)(Hom ‘𝐷)(2nd𝑣)))
1253, 19, 55, 52, 54, 56, 81, 58, 83, 122, 124catass 16394 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑓)) = ((2nd)(⟨(2nd𝑠), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))))
126107fveq2d 6233 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)) = (2nd ‘⟨((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)), ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))⟩))
127109, 110op2nd 7219 . . . . . . . 8 (2nd ‘⟨((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)), ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))⟩) = ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))
128126, 127syl6eq 2701 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)) = ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔)))
129128oveq1d 6705 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔))(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑓)) = (((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑓)))
13095fveq2d 6233 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)) = (2nd ‘⟨((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)), ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))⟩))
131115, 116op2nd 7219 . . . . . . . 8 (2nd ‘⟨((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)), ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))⟩) = ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))
132130, 131syl6eq 2701 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)) = ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓)))
133132oveq2d 6706 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd)(⟨(2nd𝑠), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓))) = ((2nd)(⟨(2nd𝑠), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))))
134125, 129, 1333eqtr4d 2695 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔))(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑓)) = ((2nd)(⟨(2nd𝑠), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓))))
135120, 134opeq12d 4441 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ⟨((1st ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔))(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑣))(1st𝑓)), ((2nd ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔))(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑓))⟩ = ⟨((1st)(⟨(1st𝑠), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓))), ((2nd)(⟨(2nd𝑠), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)))⟩)
1362, 12, 40, 36, 42, 71, 100, 76, 105catcocl 16393 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)) ∈ ((1st𝑡)(Hom ‘𝐶)(1st𝑣)))
1373, 19, 55, 52, 56, 81, 122, 83, 124catcocl 16393 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔)) ∈ ((2nd𝑡)(Hom ‘𝐷)(2nd𝑣)))
138 opelxpi 5182 . . . . . . 7 ((((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)) ∈ ((1st𝑡)(Hom ‘𝐶)(1st𝑣)) ∧ ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔)) ∈ ((2nd𝑡)(Hom ‘𝐷)(2nd𝑣))) → ⟨((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)), ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))⟩ ∈ (((1st𝑡)(Hom ‘𝐶)(1st𝑣)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑣))))
139136, 137, 138syl2anc 694 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ⟨((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)), ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))⟩ ∈ (((1st𝑡)(Hom ‘𝐶)(1st𝑣)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑣))))
1401, 4, 12, 19, 28, 41, 98xpchom 16867 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑡(Hom ‘𝑇)𝑣) = (((1st𝑡)(Hom ‘𝐶)(1st𝑣)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑣))))
141139, 107, 1403eltr4d 2745 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔) ∈ (𝑡(Hom ‘𝑇)𝑣))
1421, 4, 28, 40, 55, 62, 37, 41, 98, 43, 141xpcco 16870 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑣)𝑓) = ⟨((1st ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔))(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑣))(1st𝑓)), ((2nd ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔))(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑓))⟩)
1431, 4, 28, 40, 55, 62, 37, 69, 98, 97, 101xpcco 16870 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((⟨𝑠, 𝑢⟩(comp‘𝑇)𝑣)(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)) = ⟨((1st)(⟨(1st𝑠), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓))), ((2nd)(⟨(2nd𝑠), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)))⟩)
144135, 142, 1433eqtr4d 2695 . . 3 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑣)𝑓) = ((⟨𝑠, 𝑢⟩(comp‘𝑇)𝑣)(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)))
1455, 6, 7, 10, 11, 31, 67, 90, 97, 144iscatd2 16389 . 2 (𝜑 → (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)))
146 vex 3234 . . . . . . . 8 𝑥 ∈ V
147 vex 3234 . . . . . . . 8 𝑦 ∈ V
148146, 147op1std 7220 . . . . . . 7 (𝑡 = ⟨𝑥, 𝑦⟩ → (1st𝑡) = 𝑥)
149148fveq2d 6233 . . . . . 6 (𝑡 = ⟨𝑥, 𝑦⟩ → (𝐼‘(1st𝑡)) = (𝐼𝑥))
150146, 147op2ndd 7221 . . . . . . 7 (𝑡 = ⟨𝑥, 𝑦⟩ → (2nd𝑡) = 𝑦)
151150fveq2d 6233 . . . . . 6 (𝑡 = ⟨𝑥, 𝑦⟩ → (𝐽‘(2nd𝑡)) = (𝐽𝑦))
152149, 151opeq12d 4441 . . . . 5 (𝑡 = ⟨𝑥, 𝑦⟩ → ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩ = ⟨(𝐼𝑥), (𝐽𝑦)⟩)
153152mpt2mpt 6794 . . . 4 (𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐼𝑥), (𝐽𝑦)⟩)
154153eqeq2i 2663 . . 3 ((Id‘𝑇) = (𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩) ↔ (Id‘𝑇) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐼𝑥), (𝐽𝑦)⟩))
155154anbi2i 730 . 2 ((𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)) ↔ (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐼𝑥), (𝐽𝑦)⟩)))
156145, 155sylib 208 1 (𝜑 → (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐼𝑥), (𝐽𝑦)⟩)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  Vcvv 3231  ⟨cop 4216   ↦ cmpt 4762   × cxp 5141  ‘cfv 5926  (class class class)co 6690   ↦ cmpt2 6692  1st c1st 7208  2nd c2nd 7209  Basecbs 15904  Hom chom 15999  compcco 16000  Catccat 16372  Idccid 16373   ×c cxpc 16855 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-fz 12365  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-hom 16013  df-cco 16014  df-cat 16376  df-cid 16377  df-xpc 16859 This theorem is referenced by:  xpcid  16876  xpccat  16877
 Copyright terms: Public domain W3C validator