Step | Hyp | Ref
| Expression |
1 | | xpccat.t |
. . . . 5
⊢ 𝑇 = (𝐶 ×c 𝐷) |
2 | | xpccat.x |
. . . . 5
⊢ 𝑋 = (Base‘𝐶) |
3 | | xpccat.y |
. . . . 5
⊢ 𝑌 = (Base‘𝐷) |
4 | 1, 2, 3 | xpcbas 17172 |
. . . 4
⊢ (𝑋 × 𝑌) = (Base‘𝑇) |
5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑋 × 𝑌) = (Base‘𝑇)) |
6 | | eqidd 2827 |
. . 3
⊢ (𝜑 → (Hom ‘𝑇) = (Hom ‘𝑇)) |
7 | | eqidd 2827 |
. . 3
⊢ (𝜑 → (comp‘𝑇) = (comp‘𝑇)) |
8 | | ovex 6938 |
. . . . 5
⊢ (𝐶 ×c
𝐷) ∈
V |
9 | 1, 8 | eqeltri 2903 |
. . . 4
⊢ 𝑇 ∈ V |
10 | 9 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑇 ∈ V) |
11 | | biid 253 |
. . 3
⊢ (((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣))) ↔ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) |
12 | | eqid 2826 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
13 | | xpccat.i |
. . . . . 6
⊢ 𝐼 = (Id‘𝐶) |
14 | | xpccat.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ Cat) |
15 | 14 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝐶 ∈ Cat) |
16 | | xp1st 7461 |
. . . . . . 7
⊢ (𝑡 ∈ (𝑋 × 𝑌) → (1st ‘𝑡) ∈ 𝑋) |
17 | 16 | adantl 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (1st ‘𝑡) ∈ 𝑋) |
18 | 2, 12, 13, 15, 17 | catidcl 16696 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (𝐼‘(1st ‘𝑡)) ∈ ((1st
‘𝑡)(Hom ‘𝐶)(1st ‘𝑡))) |
19 | | eqid 2826 |
. . . . . 6
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
20 | | xpccat.j |
. . . . . 6
⊢ 𝐽 = (Id‘𝐷) |
21 | | xpccat.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ Cat) |
22 | 21 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝐷 ∈ Cat) |
23 | | xp2nd 7462 |
. . . . . . 7
⊢ (𝑡 ∈ (𝑋 × 𝑌) → (2nd ‘𝑡) ∈ 𝑌) |
24 | 23 | adantl 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑡) ∈ 𝑌) |
25 | 3, 19, 20, 22, 24 | catidcl 16696 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (𝐽‘(2nd ‘𝑡)) ∈ ((2nd
‘𝑡)(Hom ‘𝐷)(2nd ‘𝑡))) |
26 | | opelxpi 5380 |
. . . . 5
⊢ (((𝐼‘(1st
‘𝑡)) ∈
((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑡)) ∧ (𝐽‘(2nd ‘𝑡)) ∈ ((2nd
‘𝑡)(Hom ‘𝐷)(2nd ‘𝑡))) → 〈(𝐼‘(1st
‘𝑡)), (𝐽‘(2nd
‘𝑡))〉 ∈
(((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑡)) × ((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑡)))) |
27 | 18, 25, 26 | syl2anc 581 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉 ∈
(((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑡)) × ((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑡)))) |
28 | | eqid 2826 |
. . . . 5
⊢ (Hom
‘𝑇) = (Hom
‘𝑇) |
29 | | simpr 479 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝑡 ∈ (𝑋 × 𝑌)) |
30 | 1, 4, 12, 19, 28, 29, 29 | xpchom 17174 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (𝑡(Hom ‘𝑇)𝑡) = (((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑡)) × ((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑡)))) |
31 | 27, 30 | eleqtrrd 2910 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉 ∈ (𝑡(Hom ‘𝑇)𝑡)) |
32 | | fvex 6447 |
. . . . . . . 8
⊢ (𝐼‘(1st
‘𝑡)) ∈
V |
33 | | fvex 6447 |
. . . . . . . 8
⊢ (𝐽‘(2nd
‘𝑡)) ∈
V |
34 | 32, 33 | op1st 7437 |
. . . . . . 7
⊢
(1st ‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉) = (𝐼‘(1st ‘𝑡)) |
35 | 34 | oveq1i 6916 |
. . . . . 6
⊢
((1st ‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑡))(1st ‘𝑓)) = ((𝐼‘(1st ‘𝑡))(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑡))(1st ‘𝑓)) |
36 | 14 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝐶 ∈ Cat) |
37 | | simpr1l 1311 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑠 ∈ (𝑋 × 𝑌)) |
38 | | xp1st 7461 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝑋 × 𝑌) → (1st ‘𝑠) ∈ 𝑋) |
39 | 37, 38 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘𝑠) ∈ 𝑋) |
40 | | eqid 2826 |
. . . . . . 7
⊢
(comp‘𝐶) =
(comp‘𝐶) |
41 | | simpr1r 1313 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑡 ∈ (𝑋 × 𝑌)) |
42 | 41, 16 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘𝑡) ∈ 𝑋) |
43 | | simpr31 1365 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡)) |
44 | 1, 4, 12, 19, 28, 37, 41 | xpchom 17174 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑠(Hom ‘𝑇)𝑡) = (((1st ‘𝑠)(Hom ‘𝐶)(1st ‘𝑡)) × ((2nd ‘𝑠)(Hom ‘𝐷)(2nd ‘𝑡)))) |
45 | 43, 44 | eleqtrd 2909 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 ∈ (((1st ‘𝑠)(Hom ‘𝐶)(1st ‘𝑡)) × ((2nd ‘𝑠)(Hom ‘𝐷)(2nd ‘𝑡)))) |
46 | | xp1st 7461 |
. . . . . . . 8
⊢ (𝑓 ∈ (((1st
‘𝑠)(Hom ‘𝐶)(1st ‘𝑡)) × ((2nd
‘𝑠)(Hom ‘𝐷)(2nd ‘𝑡))) → (1st
‘𝑓) ∈
((1st ‘𝑠)(Hom ‘𝐶)(1st ‘𝑡))) |
47 | 45, 46 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘𝑓) ∈ ((1st
‘𝑠)(Hom ‘𝐶)(1st ‘𝑡))) |
48 | 2, 12, 13, 36, 39, 40, 42, 47 | catlid 16697 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((𝐼‘(1st ‘𝑡))(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑡))(1st ‘𝑓)) = (1st ‘𝑓)) |
49 | 35, 48 | syl5eq 2874 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑡))(1st ‘𝑓)) = (1st ‘𝑓)) |
50 | 32, 33 | op2nd 7438 |
. . . . . . 7
⊢
(2nd ‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉) = (𝐽‘(2nd ‘𝑡)) |
51 | 50 | oveq1i 6916 |
. . . . . 6
⊢
((2nd ‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑡))(2nd ‘𝑓)) = ((𝐽‘(2nd ‘𝑡))(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑡))(2nd ‘𝑓)) |
52 | 21 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝐷 ∈ Cat) |
53 | | xp2nd 7462 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝑋 × 𝑌) → (2nd ‘𝑠) ∈ 𝑌) |
54 | 37, 53 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘𝑠) ∈ 𝑌) |
55 | | eqid 2826 |
. . . . . . 7
⊢
(comp‘𝐷) =
(comp‘𝐷) |
56 | 41, 23 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘𝑡) ∈ 𝑌) |
57 | | xp2nd 7462 |
. . . . . . . 8
⊢ (𝑓 ∈ (((1st
‘𝑠)(Hom ‘𝐶)(1st ‘𝑡)) × ((2nd
‘𝑠)(Hom ‘𝐷)(2nd ‘𝑡))) → (2nd
‘𝑓) ∈
((2nd ‘𝑠)(Hom ‘𝐷)(2nd ‘𝑡))) |
58 | 45, 57 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘𝑓) ∈ ((2nd
‘𝑠)(Hom ‘𝐷)(2nd ‘𝑡))) |
59 | 3, 19, 20, 52, 54, 55, 56, 58 | catlid 16697 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((𝐽‘(2nd ‘𝑡))(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑡))(2nd ‘𝑓)) = (2nd ‘𝑓)) |
60 | 51, 59 | syl5eq 2874 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑡))(2nd ‘𝑓)) = (2nd ‘𝑓)) |
61 | 49, 60 | opeq12d 4632 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 〈((1st
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑡))(1st ‘𝑓)), ((2nd ‘〈(𝐼‘(1st
‘𝑡)), (𝐽‘(2nd
‘𝑡))〉)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑡))(2nd ‘𝑓))〉 = 〈(1st
‘𝑓), (2nd
‘𝑓)〉) |
62 | | eqid 2826 |
. . . . 5
⊢
(comp‘𝑇) =
(comp‘𝑇) |
63 | 41, 31 | syldan 587 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉 ∈ (𝑡(Hom ‘𝑇)𝑡)) |
64 | 1, 4, 28, 40, 55, 62, 37, 41, 41, 43, 63 | xpcco 17177 |
. . . 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 7468 |
. . . . 5
⊢ (𝑓 ∈ (((1st
‘𝑠)(Hom ‘𝐶)(1st ‘𝑡)) × ((2nd
‘𝑠)(Hom ‘𝐷)(2nd ‘𝑡))) → 𝑓 = 〈(1st ‘𝑓), (2nd ‘𝑓)〉) |
66 | 45, 65 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 = 〈(1st ‘𝑓), (2nd ‘𝑓)〉) |
67 | 61, 64, 66 | 3eqtr4d 2872 |
. . 3
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉(〈𝑠, 𝑡〉(comp‘𝑇)𝑡)𝑓) = 𝑓) |
68 | 34 | oveq2i 6917 |
. . . . . 6
⊢
((1st ‘𝑔)(〈(1st ‘𝑡), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)) = ((1st
‘𝑔)(〈(1st ‘𝑡), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(𝐼‘(1st ‘𝑡))) |
69 | | simpr2l 1315 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑢 ∈ (𝑋 × 𝑌)) |
70 | | xp1st 7461 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝑋 × 𝑌) → (1st ‘𝑢) ∈ 𝑋) |
71 | 69, 70 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘𝑢) ∈ 𝑋) |
72 | | simpr32 1367 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢)) |
73 | 1, 4, 12, 19, 28, 41, 69 | xpchom 17174 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑡(Hom ‘𝑇)𝑢) = (((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑢)) × ((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑢)))) |
74 | 72, 73 | eleqtrd 2909 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 ∈ (((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑢)) × ((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑢)))) |
75 | | xp1st 7461 |
. . . . . . . 8
⊢ (𝑔 ∈ (((1st
‘𝑡)(Hom ‘𝐶)(1st ‘𝑢)) × ((2nd
‘𝑡)(Hom ‘𝐷)(2nd ‘𝑢))) → (1st
‘𝑔) ∈
((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑢))) |
76 | 74, 75 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘𝑔) ∈ ((1st
‘𝑡)(Hom ‘𝐶)(1st ‘𝑢))) |
77 | 2, 12, 13, 36, 42, 40, 71, 76 | catrid 16698 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘𝑔)(〈(1st
‘𝑡), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(𝐼‘(1st ‘𝑡))) = (1st
‘𝑔)) |
78 | 68, 77 | syl5eq 2874 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘𝑔)(〈(1st
‘𝑡), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘〈(𝐼‘(1st
‘𝑡)), (𝐽‘(2nd
‘𝑡))〉)) =
(1st ‘𝑔)) |
79 | 50 | oveq2i 6917 |
. . . . . 6
⊢
((2nd ‘𝑔)(〈(2nd ‘𝑡), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)) = ((2nd
‘𝑔)(〈(2nd ‘𝑡), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(𝐽‘(2nd ‘𝑡))) |
80 | | xp2nd 7462 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝑋 × 𝑌) → (2nd ‘𝑢) ∈ 𝑌) |
81 | 69, 80 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘𝑢) ∈ 𝑌) |
82 | | xp2nd 7462 |
. . . . . . . 8
⊢ (𝑔 ∈ (((1st
‘𝑡)(Hom ‘𝐶)(1st ‘𝑢)) × ((2nd
‘𝑡)(Hom ‘𝐷)(2nd ‘𝑢))) → (2nd
‘𝑔) ∈
((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑢))) |
83 | 74, 82 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘𝑔) ∈ ((2nd
‘𝑡)(Hom ‘𝐷)(2nd ‘𝑢))) |
84 | 3, 19, 20, 52, 56, 55, 81, 83 | catrid 16698 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘𝑔)(〈(2nd
‘𝑡), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(𝐽‘(2nd ‘𝑡))) = (2nd
‘𝑔)) |
85 | 79, 84 | syl5eq 2874 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘𝑔)(〈(2nd
‘𝑡), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘〈(𝐼‘(1st
‘𝑡)), (𝐽‘(2nd
‘𝑡))〉)) =
(2nd ‘𝑔)) |
86 | 78, 85 | opeq12d 4632 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 〈((1st
‘𝑔)(〈(1st ‘𝑡), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)), ((2nd
‘𝑔)(〈(2nd ‘𝑡), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉))〉 =
〈(1st ‘𝑔), (2nd ‘𝑔)〉) |
87 | 1, 4, 28, 40, 55, 62, 41, 41, 69, 63, 72 | xpcco 17177 |
. . . 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 7468 |
. . . . 5
⊢ (𝑔 ∈ (((1st
‘𝑡)(Hom ‘𝐶)(1st ‘𝑢)) × ((2nd
‘𝑡)(Hom ‘𝐷)(2nd ‘𝑢))) → 𝑔 = 〈(1st ‘𝑔), (2nd ‘𝑔)〉) |
89 | 74, 88 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 = 〈(1st ‘𝑔), (2nd ‘𝑔)〉) |
90 | 86, 87, 89 | 3eqtr4d 2872 |
. . 3
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(〈𝑡, 𝑡〉(comp‘𝑇)𝑢)〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉) = 𝑔) |
91 | 2, 12, 40, 36, 39, 42, 71, 47, 76 | catcocl 16699 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘𝑔)(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)) ∈ ((1st ‘𝑠)(Hom ‘𝐶)(1st ‘𝑢))) |
92 | 3, 19, 55, 52, 54, 56, 81, 58, 83 | catcocl 16699 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘𝑔)(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓)) ∈ ((2nd ‘𝑠)(Hom ‘𝐷)(2nd ‘𝑢))) |
93 | | opelxpi 5380 |
. . . . 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 ‘𝑢)))) |
94 | 91, 92, 93 | syl2anc 581 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 〈((1st
‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)), ((2nd
‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓))〉 ∈
(((1st ‘𝑠)(Hom ‘𝐶)(1st ‘𝑢)) × ((2nd ‘𝑠)(Hom ‘𝐷)(2nd ‘𝑢)))) |
95 | 1, 4, 28, 40, 55, 62, 37, 41, 69, 43, 72 | xpcco 17177 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓) = 〈((1st ‘𝑔)(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓))〉) |
96 | 1, 4, 12, 19, 28, 37, 69 | xpchom 17174 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑠(Hom ‘𝑇)𝑢) = (((1st ‘𝑠)(Hom ‘𝐶)(1st ‘𝑢)) × ((2nd ‘𝑠)(Hom ‘𝐷)(2nd ‘𝑢)))) |
97 | 94, 95, 96 | 3eltr4d 2922 |
. . 3
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓) ∈ (𝑠(Hom ‘𝑇)𝑢)) |
98 | | simpr2r 1317 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑣 ∈ (𝑋 × 𝑌)) |
99 | | xp1st 7461 |
. . . . . . . 8
⊢ (𝑣 ∈ (𝑋 × 𝑌) → (1st ‘𝑣) ∈ 𝑋) |
100 | 98, 99 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘𝑣) ∈ 𝑋) |
101 | | simpr33 1369 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)) |
102 | 1, 4, 12, 19, 28, 69, 98 | xpchom 17174 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑢(Hom ‘𝑇)𝑣) = (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣)))) |
103 | 101, 102 | eleqtrd 2909 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ℎ ∈ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣)))) |
104 | | xp1st 7461 |
. . . . . . . 8
⊢ (ℎ ∈ (((1st
‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd
‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))) → (1st
‘ℎ) ∈
((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣))) |
105 | 103, 104 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘ℎ) ∈ ((1st
‘𝑢)(Hom ‘𝐶)(1st ‘𝑣))) |
106 | 2, 12, 40, 36, 39, 42, 71, 47, 76, 100, 105 | catass 16700 |
. . . . . 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 ‘𝑓)))) |
107 | 1, 4, 28, 40, 55, 62, 41, 69, 98, 72, 101 | xpcco 17177 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔) = 〈((1st ‘ℎ)(〈(1st
‘𝑡), (1st
‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)), ((2nd ‘ℎ)(〈(2nd
‘𝑡), (2nd
‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))〉) |
108 | 107 | fveq2d 6438 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔)) = (1st
‘〈((1st ‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)), ((2nd
‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))〉)) |
109 | | ovex 6938 |
. . . . . . . . 9
⊢
((1st ‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)) ∈ V |
110 | | ovex 6938 |
. . . . . . . . 9
⊢
((2nd ‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔)) ∈ V |
111 | 109, 110 | op1st 7437 |
. . . . . . . 8
⊢
(1st ‘〈((1st ‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)), ((2nd
‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))〉) = ((1st
‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)) |
112 | 108, 111 | syl6eq 2878 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔)) = ((1st ‘ℎ)(〈(1st
‘𝑡), (1st
‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔))) |
113 | 112 | oveq1d 6921 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔))(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑓)) = (((1st
‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔))(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑓))) |
114 | 95 | fveq2d 6438 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)) = (1st
‘〈((1st ‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)), ((2nd
‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓))〉)) |
115 | | ovex 6938 |
. . . . . . . . 9
⊢
((1st ‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)) ∈ V |
116 | | ovex 6938 |
. . . . . . . . 9
⊢
((2nd ‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓)) ∈ V |
117 | 115, 116 | op1st 7437 |
. . . . . . . 8
⊢
(1st ‘〈((1st ‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)), ((2nd
‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓))〉) = ((1st
‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)) |
118 | 114, 117 | syl6eq 2878 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)) = ((1st ‘𝑔)(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓))) |
119 | 118 | oveq2d 6922 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘ℎ)(〈(1st
‘𝑠), (1st
‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓))) = ((1st ‘ℎ)(〈(1st
‘𝑠), (1st
‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))((1st ‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)))) |
120 | 106, 113,
119 | 3eqtr4d 2872 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔))(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑓)) = ((1st
‘ℎ)(〈(1st ‘𝑠), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)))) |
121 | | xp2nd 7462 |
. . . . . . . 8
⊢ (𝑣 ∈ (𝑋 × 𝑌) → (2nd ‘𝑣) ∈ 𝑌) |
122 | 98, 121 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘𝑣) ∈ 𝑌) |
123 | | xp2nd 7462 |
. . . . . . . 8
⊢ (ℎ ∈ (((1st
‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd
‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))) → (2nd
‘ℎ) ∈
((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))) |
124 | 103, 123 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘ℎ) ∈ ((2nd
‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))) |
125 | 3, 19, 55, 52, 54, 56, 81, 58, 83, 122, 124 | catass 16700 |
. . . . . 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 ‘𝑓)))) |
126 | 107 | fveq2d 6438 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔)) = (2nd
‘〈((1st ‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)), ((2nd
‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))〉)) |
127 | 109, 110 | op2nd 7438 |
. . . . . . . 8
⊢
(2nd ‘〈((1st ‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)), ((2nd
‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))〉) = ((2nd
‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔)) |
128 | 126, 127 | syl6eq 2878 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔)) = ((2nd ‘ℎ)(〈(2nd
‘𝑡), (2nd
‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))) |
129 | 128 | oveq1d 6921 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔))(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑓)) = (((2nd
‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑓))) |
130 | 95 | fveq2d 6438 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)) = (2nd
‘〈((1st ‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)), ((2nd
‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓))〉)) |
131 | 115, 116 | op2nd 7438 |
. . . . . . . 8
⊢
(2nd ‘〈((1st ‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)), ((2nd
‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓))〉) = ((2nd
‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓)) |
132 | 130, 131 | syl6eq 2878 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)) = ((2nd ‘𝑔)(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓))) |
133 | 132 | oveq2d 6922 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘ℎ)(〈(2nd
‘𝑠), (2nd
‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓))) = ((2nd ‘ℎ)(〈(2nd
‘𝑠), (2nd
‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))((2nd ‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓)))) |
134 | 125, 129,
133 | 3eqtr4d 2872 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔))(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑓)) = ((2nd
‘ℎ)(〈(2nd ‘𝑠), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)))) |
135 | 120, 134 | opeq12d 4632 |
. . . 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‘𝑇)𝑢)𝑓)))〉) |
136 | 2, 12, 40, 36, 42, 71, 100, 76, 105 | catcocl 16699 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘ℎ)(〈(1st
‘𝑡), (1st
‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)) ∈ ((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑣))) |
137 | 3, 19, 55, 52, 56, 81, 122, 83, 124 | catcocl 16699 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘ℎ)(〈(2nd
‘𝑡), (2nd
‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔)) ∈ ((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑣))) |
138 | | opelxpi 5380 |
. . . . . . 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 ‘𝑣)))) |
139 | 136, 137,
138 | syl2anc 581 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 〈((1st
‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)), ((2nd
‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))〉 ∈
(((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑣)))) |
140 | 1, 4, 12, 19, 28, 41, 98 | xpchom 17174 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑡(Hom ‘𝑇)𝑣) = (((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑣)))) |
141 | 139, 107,
140 | 3eltr4d 2922 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔) ∈ (𝑡(Hom ‘𝑇)𝑣)) |
142 | 1, 4, 28, 40, 55, 62, 37, 41, 98, 43, 141 | xpcco 17177 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔)(〈𝑠, 𝑡〉(comp‘𝑇)𝑣)𝑓) = 〈((1st ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔))(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑓)), ((2nd
‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔))(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑓))〉) |
143 | 1, 4, 28, 40, 55, 62, 37, 69, 98, 97, 101 | xpcco 17177 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (ℎ(〈𝑠, 𝑢〉(comp‘𝑇)𝑣)(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)) = 〈((1st ‘ℎ)(〈(1st
‘𝑠), (1st
‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓))), ((2nd ‘ℎ)(〈(2nd
‘𝑠), (2nd
‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)))〉) |
144 | 135, 142,
143 | 3eqtr4d 2872 |
. . 3
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔)(〈𝑠, 𝑡〉(comp‘𝑇)𝑣)𝑓) = (ℎ(〈𝑠, 𝑢〉(comp‘𝑇)𝑣)(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓))) |
145 | 5, 6, 7, 10, 11, 31, 67, 90, 97, 144 | iscatd2 16695 |
. 2
⊢ (𝜑 → (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑡 ∈ (𝑋 × 𝑌) ↦ 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉))) |
146 | | vex 3418 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
147 | | vex 3418 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
148 | 146, 147 | op1std 7439 |
. . . . . . 7
⊢ (𝑡 = 〈𝑥, 𝑦〉 → (1st ‘𝑡) = 𝑥) |
149 | 148 | fveq2d 6438 |
. . . . . 6
⊢ (𝑡 = 〈𝑥, 𝑦〉 → (𝐼‘(1st ‘𝑡)) = (𝐼‘𝑥)) |
150 | 146, 147 | op2ndd 7440 |
. . . . . . 7
⊢ (𝑡 = 〈𝑥, 𝑦〉 → (2nd ‘𝑡) = 𝑦) |
151 | 150 | fveq2d 6438 |
. . . . . 6
⊢ (𝑡 = 〈𝑥, 𝑦〉 → (𝐽‘(2nd ‘𝑡)) = (𝐽‘𝑦)) |
152 | 149, 151 | opeq12d 4632 |
. . . . 5
⊢ (𝑡 = 〈𝑥, 𝑦〉 → 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉 = 〈(𝐼‘𝑥), (𝐽‘𝑦)〉) |
153 | 152 | mpt2mpt 7013 |
. . . 4
⊢ (𝑡 ∈ (𝑋 × 𝑌) ↦ 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐼‘𝑥), (𝐽‘𝑦)〉) |
154 | 153 | eqeq2i 2838 |
. . 3
⊢
((Id‘𝑇) =
(𝑡 ∈ (𝑋 × 𝑌) ↦ 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉) ↔ (Id‘𝑇) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐼‘𝑥), (𝐽‘𝑦)〉)) |
155 | 154 | anbi2i 618 |
. 2
⊢ ((𝑇 ∈ Cat ∧
(Id‘𝑇) = (𝑡 ∈ (𝑋 × 𝑌) ↦ 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)) ↔ (𝑇 ∈ Cat ∧
(Id‘𝑇) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐼‘𝑥), (𝐽‘𝑦)〉))) |
156 | 145, 155 | sylib 210 |
1
⊢ (𝜑 → (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐼‘𝑥), (𝐽‘𝑦)〉))) |