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

Theorem xpccatid 16749
 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 16739 . . . 4 (𝑋 × 𝑌) = (Base‘𝑇)
54a1i 11 . . 3 (𝜑 → (𝑋 × 𝑌) = (Base‘𝑇))
6 eqidd 2622 . . 3 (𝜑 → (Hom ‘𝑇) = (Hom ‘𝑇))
7 eqidd 2622 . . 3 (𝜑 → (comp‘𝑇) = (comp‘𝑇))
8 ovex 6632 . . . . 5 (𝐶 ×c 𝐷) ∈ V
91, 8eqeltri 2694 . . . 4 𝑇 ∈ V
109a1i 11 . . 3 (𝜑𝑇 ∈ V)
11 biid 251 . . 3 (((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣))) ↔ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣))))
12 eqid 2621 . . . . . 6 (Hom ‘𝐶) = (Hom ‘𝐶)
13 xpccat.i . . . . . 6 𝐼 = (Id‘𝐶)
14 xpccat.c . . . . . . 7 (𝜑𝐶 ∈ Cat)
1514adantr 481 . . . . . 6 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → 𝐶 ∈ Cat)
16 xp1st 7143 . . . . . . 7 (𝑡 ∈ (𝑋 × 𝑌) → (1st𝑡) ∈ 𝑋)
1716adantl 482 . . . . . 6 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → (1st𝑡) ∈ 𝑋)
182, 12, 13, 15, 17catidcl 16264 . . . . 5 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → (𝐼‘(1st𝑡)) ∈ ((1st𝑡)(Hom ‘𝐶)(1st𝑡)))
19 eqid 2621 . . . . . 6 (Hom ‘𝐷) = (Hom ‘𝐷)
20 xpccat.j . . . . . 6 𝐽 = (Id‘𝐷)
21 xpccat.d . . . . . . 7 (𝜑𝐷 ∈ Cat)
2221adantr 481 . . . . . 6 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → 𝐷 ∈ Cat)
23 xp2nd 7144 . . . . . . 7 (𝑡 ∈ (𝑋 × 𝑌) → (2nd𝑡) ∈ 𝑌)
2423adantl 482 . . . . . 6 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → (2nd𝑡) ∈ 𝑌)
253, 19, 20, 22, 24catidcl 16264 . . . . 5 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → (𝐽‘(2nd𝑡)) ∈ ((2nd𝑡)(Hom ‘𝐷)(2nd𝑡)))
26 opelxpi 5108 . . . . 5 (((𝐼‘(1st𝑡)) ∈ ((1st𝑡)(Hom ‘𝐶)(1st𝑡)) ∧ (𝐽‘(2nd𝑡)) ∈ ((2nd𝑡)(Hom ‘𝐷)(2nd𝑡))) → ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩ ∈ (((1st𝑡)(Hom ‘𝐶)(1st𝑡)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑡))))
2718, 25, 26syl2anc 692 . . . 4 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩ ∈ (((1st𝑡)(Hom ‘𝐶)(1st𝑡)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑡))))
28 eqid 2621 . . . . 5 (Hom ‘𝑇) = (Hom ‘𝑇)
29 simpr 477 . . . . 5 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → 𝑡 ∈ (𝑋 × 𝑌))
301, 4, 12, 19, 28, 29, 29xpchom 16741 . . . 4 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → (𝑡(Hom ‘𝑇)𝑡) = (((1st𝑡)(Hom ‘𝐶)(1st𝑡)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑡))))
3127, 30eleqtrrd 2701 . . 3 ((𝜑𝑡 ∈ (𝑋 × 𝑌)) → ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩ ∈ (𝑡(Hom ‘𝑇)𝑡))
32 fvex 6158 . . . . . . . 8 (𝐼‘(1st𝑡)) ∈ V
33 fvex 6158 . . . . . . . 8 (𝐽‘(2nd𝑡)) ∈ V
3432, 33op1st 7121 . . . . . . 7 (1st ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩) = (𝐼‘(1st𝑡))
3534oveq1i 6614 . . . . . 6 ((1st ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑡))(1st𝑓)) = ((𝐼‘(1st𝑡))(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑡))(1st𝑓))
3614adantr 481 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝐶 ∈ Cat)
37 simpr1l 1116 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑠 ∈ (𝑋 × 𝑌))
38 xp1st 7143 . . . . . . . 8 (𝑠 ∈ (𝑋 × 𝑌) → (1st𝑠) ∈ 𝑋)
3937, 38syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st𝑠) ∈ 𝑋)
40 eqid 2621 . . . . . . 7 (comp‘𝐶) = (comp‘𝐶)
41 simpr1r 1117 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑡 ∈ (𝑋 × 𝑌))
4241, 16syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st𝑡) ∈ 𝑋)
43 simpr31 1149 . . . . . . . . 9 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡))
441, 4, 12, 19, 28, 37, 41xpchom 16741 . . . . . . . . 9 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑠(Hom ‘𝑇)𝑡) = (((1st𝑠)(Hom ‘𝐶)(1st𝑡)) × ((2nd𝑠)(Hom ‘𝐷)(2nd𝑡))))
4543, 44eleqtrd 2700 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 ∈ (((1st𝑠)(Hom ‘𝐶)(1st𝑡)) × ((2nd𝑠)(Hom ‘𝐷)(2nd𝑡))))
46 xp1st 7143 . . . . . . . 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 16265 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((𝐼‘(1st𝑡))(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑡))(1st𝑓)) = (1st𝑓))
4935, 48syl5eq 2667 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑡))(1st𝑓)) = (1st𝑓))
5032, 33op2nd 7122 . . . . . . 7 (2nd ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩) = (𝐽‘(2nd𝑡))
5150oveq1i 6614 . . . . . 6 ((2nd ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑡))(2nd𝑓)) = ((𝐽‘(2nd𝑡))(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑡))(2nd𝑓))
5221adantr 481 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝐷 ∈ Cat)
53 xp2nd 7144 . . . . . . . 8 (𝑠 ∈ (𝑋 × 𝑌) → (2nd𝑠) ∈ 𝑌)
5437, 53syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd𝑠) ∈ 𝑌)
55 eqid 2621 . . . . . . 7 (comp‘𝐷) = (comp‘𝐷)
5641, 23syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd𝑡) ∈ 𝑌)
57 xp2nd 7144 . . . . . . . 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 16265 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((𝐽‘(2nd𝑡))(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑡))(2nd𝑓)) = (2nd𝑓))
6051, 59syl5eq 2667 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑡))(2nd𝑓)) = (2nd𝑓))
6149, 60opeq12d 4378 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ⟨((1st ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑡))(1st𝑓)), ((2nd ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑡))(2nd𝑓))⟩ = ⟨(1st𝑓), (2nd𝑓)⟩)
62 eqid 2621 . . . . 5 (comp‘𝑇) = (comp‘𝑇)
6341, 31syldan 487 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩ ∈ (𝑡(Hom ‘𝑇)𝑡))
641, 4, 28, 40, 55, 62, 37, 41, 41, 43, 63xpcco 16744 . . . 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 7150 . . . . 5 (𝑓 ∈ (((1st𝑠)(Hom ‘𝐶)(1st𝑡)) × ((2nd𝑠)(Hom ‘𝐷)(2nd𝑡))) → 𝑓 = ⟨(1st𝑓), (2nd𝑓)⟩)
6645, 65syl 17 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 = ⟨(1st𝑓), (2nd𝑓)⟩)
6761, 64, 663eqtr4d 2665 . . 3 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑡)𝑓) = 𝑓)
6834oveq2i 6615 . . . . . 6 ((1st𝑔)(⟨(1st𝑡), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)) = ((1st𝑔)(⟨(1st𝑡), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(𝐼‘(1st𝑡)))
69 simpr2l 1118 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑢 ∈ (𝑋 × 𝑌))
70 xp1st 7143 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (1st𝑢) ∈ 𝑋)
7169, 70syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st𝑢) ∈ 𝑋)
72 simpr32 1150 . . . . . . . . 9 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢))
731, 4, 12, 19, 28, 41, 69xpchom 16741 . . . . . . . . 9 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑡(Hom ‘𝑇)𝑢) = (((1st𝑡)(Hom ‘𝐶)(1st𝑢)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑢))))
7472, 73eleqtrd 2700 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 ∈ (((1st𝑡)(Hom ‘𝐶)(1st𝑢)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑢))))
75 xp1st 7143 . . . . . . . 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 16266 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st𝑔)(⟨(1st𝑡), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(𝐼‘(1st𝑡))) = (1st𝑔))
7868, 77syl5eq 2667 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st𝑔)(⟨(1st𝑡), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)) = (1st𝑔))
7950oveq2i 6615 . . . . . 6 ((2nd𝑔)(⟨(2nd𝑡), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)) = ((2nd𝑔)(⟨(2nd𝑡), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(𝐽‘(2nd𝑡)))
80 xp2nd 7144 . . . . . . . 8 (𝑢 ∈ (𝑋 × 𝑌) → (2nd𝑢) ∈ 𝑌)
8169, 80syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd𝑢) ∈ 𝑌)
82 xp2nd 7144 . . . . . . . 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 16266 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd𝑔)(⟨(2nd𝑡), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(𝐽‘(2nd𝑡))) = (2nd𝑔))
8579, 84syl5eq 2667 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd𝑔)(⟨(2nd𝑡), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd ‘⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)) = (2nd𝑔))
8678, 85opeq12d 4378 . . . 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 16744 . . . 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 7150 . . . . 5 (𝑔 ∈ (((1st𝑡)(Hom ‘𝐶)(1st𝑢)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑢))) → 𝑔 = ⟨(1st𝑔), (2nd𝑔)⟩)
8974, 88syl 17 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 = ⟨(1st𝑔), (2nd𝑔)⟩)
9086, 87, 893eqtr4d 2665 . . 3 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(⟨𝑡, 𝑡⟩(comp‘𝑇)𝑢)⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩) = 𝑔)
912, 12, 40, 36, 39, 42, 71, 47, 76catcocl 16267 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)) ∈ ((1st𝑠)(Hom ‘𝐶)(1st𝑢)))
923, 19, 55, 52, 54, 56, 81, 58, 83catcocl 16267 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓)) ∈ ((2nd𝑠)(Hom ‘𝐷)(2nd𝑢)))
93 opelxpi 5108 . . . . 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 692 . . . 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 16744 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓) = ⟨((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)), ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))⟩)
961, 4, 12, 19, 28, 37, 69xpchom 16741 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑠(Hom ‘𝑇)𝑢) = (((1st𝑠)(Hom ‘𝐶)(1st𝑢)) × ((2nd𝑠)(Hom ‘𝐷)(2nd𝑢))))
9794, 95, 963eltr4d 2713 . . 3 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓) ∈ (𝑠(Hom ‘𝑇)𝑢))
98 simpr2r 1119 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑣 ∈ (𝑋 × 𝑌))
99 xp1st 7143 . . . . . . . 8 (𝑣 ∈ (𝑋 × 𝑌) → (1st𝑣) ∈ 𝑋)
10098, 99syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st𝑣) ∈ 𝑋)
101 simpr33 1151 . . . . . . . . 9 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ∈ (𝑢(Hom ‘𝑇)𝑣))
1021, 4, 12, 19, 28, 69, 98xpchom 16741 . . . . . . . . 9 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑢(Hom ‘𝑇)𝑣) = (((1st𝑢)(Hom ‘𝐶)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝐷)(2nd𝑣))))
103101, 102eleqtrd 2700 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ∈ (((1st𝑢)(Hom ‘𝐶)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝐷)(2nd𝑣))))
104 xp1st 7143 . . . . . . . 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 16268 . . . . . 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 16744 . . . . . . . . 9 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔) = ⟨((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)), ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))⟩)
108107fveq2d 6152 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)) = (1st ‘⟨((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)), ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))⟩))
109 ovex 6632 . . . . . . . . 9 ((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)) ∈ V
110 ovex 6632 . . . . . . . . 9 ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔)) ∈ V
111109, 110op1st 7121 . . . . . . . 8 (1st ‘⟨((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)), ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))⟩) = ((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔))
112108, 111syl6eq 2671 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)) = ((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)))
113112oveq1d 6619 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔))(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑣))(1st𝑓)) = (((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔))(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑣))(1st𝑓)))
11495fveq2d 6152 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)) = (1st ‘⟨((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)), ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))⟩))
115 ovex 6632 . . . . . . . . 9 ((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)) ∈ V
116 ovex 6632 . . . . . . . . 9 ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓)) ∈ V
117115, 116op1st 7121 . . . . . . . 8 (1st ‘⟨((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)), ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))⟩) = ((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓))
118114, 117syl6eq 2671 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)) = ((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)))
119118oveq2d 6620 . . . . . 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 2665 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔))(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑣))(1st𝑓)) = ((1st)(⟨(1st𝑠), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓))))
121 xp2nd 7144 . . . . . . . 8 (𝑣 ∈ (𝑋 × 𝑌) → (2nd𝑣) ∈ 𝑌)
12298, 121syl 17 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd𝑣) ∈ 𝑌)
123 xp2nd 7144 . . . . . . . 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 16268 . . . . . 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 6152 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)) = (2nd ‘⟨((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)), ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))⟩))
127109, 110op2nd 7122 . . . . . . . 8 (2nd ‘⟨((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)), ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))⟩) = ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))
128126, 127syl6eq 2671 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)) = ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔)))
129128oveq1d 6619 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔))(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑓)) = (((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔))(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑓)))
13095fveq2d 6152 . . . . . . . 8 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)) = (2nd ‘⟨((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)), ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))⟩))
131115, 116op2nd 7122 . . . . . . . 8 (2nd ‘⟨((1st𝑔)(⟨(1st𝑠), (1st𝑡)⟩(comp‘𝐶)(1st𝑢))(1st𝑓)), ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))⟩) = ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓))
132130, 131syl6eq 2671 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)) = ((2nd𝑔)(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑢))(2nd𝑓)))
133132oveq2d 6620 . . . . . 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 2665 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔))(⟨(2nd𝑠), (2nd𝑡)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑓)) = ((2nd)(⟨(2nd𝑠), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓))))
135120, 134opeq12d 4378 . . . 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 16267 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st)(⟨(1st𝑡), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st𝑔)) ∈ ((1st𝑡)(Hom ‘𝐶)(1st𝑣)))
1373, 19, 55, 52, 56, 81, 122, 83, 124catcocl 16267 . . . . . . 7 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd)(⟨(2nd𝑡), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd𝑔)) ∈ ((2nd𝑡)(Hom ‘𝐷)(2nd𝑣)))
138 opelxpi 5108 . . . . . . 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 692 . . . . . 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 16741 . . . . . 6 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑡(Hom ‘𝑇)𝑣) = (((1st𝑡)(Hom ‘𝐶)(1st𝑣)) × ((2nd𝑡)(Hom ‘𝐷)(2nd𝑣))))
141139, 107, 1403eltr4d 2713 . . . . 5 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔) ∈ (𝑡(Hom ‘𝑇)𝑣))
1421, 4, 28, 40, 55, 62, 37, 41, 98, 43, 141xpcco 16744 . . . 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 16744 . . . 4 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((⟨𝑠, 𝑢⟩(comp‘𝑇)𝑣)(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)) = ⟨((1st)(⟨(1st𝑠), (1st𝑢)⟩(comp‘𝐶)(1st𝑣))(1st ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓))), ((2nd)(⟨(2nd𝑠), (2nd𝑢)⟩(comp‘𝐷)(2nd𝑣))(2nd ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)))⟩)
144135, 142, 1433eqtr4d 2665 . . 3 ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (((⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑣)𝑓) = ((⟨𝑠, 𝑢⟩(comp‘𝑇)𝑣)(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)))
1455, 6, 7, 10, 11, 31, 67, 90, 97, 144iscatd2 16263 . 2 (𝜑 → (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)))
146 vex 3189 . . . . . . . 8 𝑥 ∈ V
147 vex 3189 . . . . . . . 8 𝑦 ∈ V
148146, 147op1std 7123 . . . . . . 7 (𝑡 = ⟨𝑥, 𝑦⟩ → (1st𝑡) = 𝑥)
149148fveq2d 6152 . . . . . 6 (𝑡 = ⟨𝑥, 𝑦⟩ → (𝐼‘(1st𝑡)) = (𝐼𝑥))
150146, 147op2ndd 7124 . . . . . . 7 (𝑡 = ⟨𝑥, 𝑦⟩ → (2nd𝑡) = 𝑦)
151150fveq2d 6152 . . . . . 6 (𝑡 = ⟨𝑥, 𝑦⟩ → (𝐽‘(2nd𝑡)) = (𝐽𝑦))
152149, 151opeq12d 4378 . . . . 5 (𝑡 = ⟨𝑥, 𝑦⟩ → ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩ = ⟨(𝐼𝑥), (𝐽𝑦)⟩)
153152mpt2mpt 6705 . . . 4 (𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐼𝑥), (𝐽𝑦)⟩)
154153eqeq2i 2633 . . 3 ((Id‘𝑇) = (𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩) ↔ (Id‘𝑇) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐼𝑥), (𝐽𝑦)⟩))
155154anbi2i 729 . 2 ((𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1st𝑡)), (𝐽‘(2nd𝑡))⟩)) ↔ (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐼𝑥), (𝐽𝑦)⟩)))
156145, 155sylib 208 1 (𝜑 → (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐼𝑥), (𝐽𝑦)⟩)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987  Vcvv 3186  ⟨cop 4154   ↦ cmpt 4673   × cxp 5072  ‘cfv 5847  (class class class)co 6604   ↦ cmpt2 6606  1st c1st 7111  2nd c2nd 7112  Basecbs 15781  Hom chom 15873  compcco 15874  Catccat 16246  Idccid 16247   ×c cxpc 16729 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-z 11322  df-dec 11438  df-uz 11632  df-fz 12269  df-struct 15783  df-ndx 15784  df-slot 15785  df-base 15786  df-hom 15887  df-cco 15888  df-cat 16250  df-cid 16251  df-xpc 16733 This theorem is referenced by:  xpcid  16750  xpccat  16751
 Copyright terms: Public domain W3C validator