Step | Hyp | Ref
| Expression |
1 | | xpccat.t |
. . . . 5
⊢ 𝑇 = (𝐶 ×c 𝐷) |
2 | | xpccat.x |
. . . . 5
⊢ 𝑋 = (Base‘𝐶) |
3 | | xpccat.y |
. . . . 5
⊢ 𝑌 = (Base‘𝐷) |
4 | 1, 2, 3 | xpcbas 17544 |
. . . 4
⊢ (𝑋 × 𝑌) = (Base‘𝑇) |
5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑋 × 𝑌) = (Base‘𝑇)) |
6 | | eqidd 2739 |
. . 3
⊢ (𝜑 → (Hom ‘𝑇) = (Hom ‘𝑇)) |
7 | | eqidd 2739 |
. . 3
⊢ (𝜑 → (comp‘𝑇) = (comp‘𝑇)) |
8 | 1 | ovexi 7204 |
. . . 4
⊢ 𝑇 ∈ V |
9 | 8 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑇 ∈ V) |
10 | | biid 264 |
. . 3
⊢ (((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣))) ↔ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) |
11 | | eqid 2738 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
12 | | xpccat.i |
. . . . . 6
⊢ 𝐼 = (Id‘𝐶) |
13 | | xpccat.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ Cat) |
14 | 13 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝐶 ∈ Cat) |
15 | | xp1st 7746 |
. . . . . . 7
⊢ (𝑡 ∈ (𝑋 × 𝑌) → (1st ‘𝑡) ∈ 𝑋) |
16 | 15 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (1st ‘𝑡) ∈ 𝑋) |
17 | 2, 11, 12, 14, 16 | catidcl 17056 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (𝐼‘(1st ‘𝑡)) ∈ ((1st
‘𝑡)(Hom ‘𝐶)(1st ‘𝑡))) |
18 | | eqid 2738 |
. . . . . 6
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
19 | | xpccat.j |
. . . . . 6
⊢ 𝐽 = (Id‘𝐷) |
20 | | xpccat.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ Cat) |
21 | 20 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝐷 ∈ Cat) |
22 | | xp2nd 7747 |
. . . . . . 7
⊢ (𝑡 ∈ (𝑋 × 𝑌) → (2nd ‘𝑡) ∈ 𝑌) |
23 | 22 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑡) ∈ 𝑌) |
24 | 3, 18, 19, 21, 23 | catidcl 17056 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (𝐽‘(2nd ‘𝑡)) ∈ ((2nd
‘𝑡)(Hom ‘𝐷)(2nd ‘𝑡))) |
25 | 17, 24 | opelxpd 5563 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉 ∈
(((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑡)) × ((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑡)))) |
26 | | eqid 2738 |
. . . . 5
⊢ (Hom
‘𝑇) = (Hom
‘𝑇) |
27 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝑡 ∈ (𝑋 × 𝑌)) |
28 | 1, 4, 11, 18, 26, 27, 27 | xpchom 17546 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (𝑡(Hom ‘𝑇)𝑡) = (((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑡)) × ((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑡)))) |
29 | 25, 28 | eleqtrrd 2836 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉 ∈ (𝑡(Hom ‘𝑇)𝑡)) |
30 | | fvex 6687 |
. . . . . . . 8
⊢ (𝐼‘(1st
‘𝑡)) ∈
V |
31 | | fvex 6687 |
. . . . . . . 8
⊢ (𝐽‘(2nd
‘𝑡)) ∈
V |
32 | 30, 31 | op1st 7722 |
. . . . . . 7
⊢
(1st ‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉) = (𝐼‘(1st ‘𝑡)) |
33 | 32 | oveq1i 7180 |
. . . . . 6
⊢
((1st ‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑡))(1st ‘𝑓)) = ((𝐼‘(1st ‘𝑡))(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑡))(1st ‘𝑓)) |
34 | 13 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝐶 ∈ Cat) |
35 | | simpr1l 1231 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑠 ∈ (𝑋 × 𝑌)) |
36 | | xp1st 7746 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝑋 × 𝑌) → (1st ‘𝑠) ∈ 𝑋) |
37 | 35, 36 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘𝑠) ∈ 𝑋) |
38 | | eqid 2738 |
. . . . . . 7
⊢
(comp‘𝐶) =
(comp‘𝐶) |
39 | | simpr1r 1232 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑡 ∈ (𝑋 × 𝑌)) |
40 | 39, 15 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘𝑡) ∈ 𝑋) |
41 | | simpr31 1264 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡)) |
42 | 1, 4, 11, 18, 26, 35, 39 | xpchom 17546 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑠(Hom ‘𝑇)𝑡) = (((1st ‘𝑠)(Hom ‘𝐶)(1st ‘𝑡)) × ((2nd ‘𝑠)(Hom ‘𝐷)(2nd ‘𝑡)))) |
43 | 41, 42 | eleqtrd 2835 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 ∈ (((1st ‘𝑠)(Hom ‘𝐶)(1st ‘𝑡)) × ((2nd ‘𝑠)(Hom ‘𝐷)(2nd ‘𝑡)))) |
44 | | xp1st 7746 |
. . . . . . . 8
⊢ (𝑓 ∈ (((1st
‘𝑠)(Hom ‘𝐶)(1st ‘𝑡)) × ((2nd
‘𝑠)(Hom ‘𝐷)(2nd ‘𝑡))) → (1st
‘𝑓) ∈
((1st ‘𝑠)(Hom ‘𝐶)(1st ‘𝑡))) |
45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘𝑓) ∈ ((1st
‘𝑠)(Hom ‘𝐶)(1st ‘𝑡))) |
46 | 2, 11, 12, 34, 37, 38, 40, 45 | catlid 17057 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((𝐼‘(1st ‘𝑡))(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑡))(1st ‘𝑓)) = (1st ‘𝑓)) |
47 | 33, 46 | syl5eq 2785 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑡))(1st ‘𝑓)) = (1st ‘𝑓)) |
48 | 30, 31 | op2nd 7723 |
. . . . . . 7
⊢
(2nd ‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉) = (𝐽‘(2nd ‘𝑡)) |
49 | 48 | oveq1i 7180 |
. . . . . 6
⊢
((2nd ‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑡))(2nd ‘𝑓)) = ((𝐽‘(2nd ‘𝑡))(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑡))(2nd ‘𝑓)) |
50 | 20 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝐷 ∈ Cat) |
51 | | xp2nd 7747 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝑋 × 𝑌) → (2nd ‘𝑠) ∈ 𝑌) |
52 | 35, 51 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘𝑠) ∈ 𝑌) |
53 | | eqid 2738 |
. . . . . . 7
⊢
(comp‘𝐷) =
(comp‘𝐷) |
54 | 39, 22 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘𝑡) ∈ 𝑌) |
55 | | xp2nd 7747 |
. . . . . . . 8
⊢ (𝑓 ∈ (((1st
‘𝑠)(Hom ‘𝐶)(1st ‘𝑡)) × ((2nd
‘𝑠)(Hom ‘𝐷)(2nd ‘𝑡))) → (2nd
‘𝑓) ∈
((2nd ‘𝑠)(Hom ‘𝐷)(2nd ‘𝑡))) |
56 | 43, 55 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘𝑓) ∈ ((2nd
‘𝑠)(Hom ‘𝐷)(2nd ‘𝑡))) |
57 | 3, 18, 19, 50, 52, 53, 54, 56 | catlid 17057 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((𝐽‘(2nd ‘𝑡))(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑡))(2nd ‘𝑓)) = (2nd ‘𝑓)) |
58 | 49, 57 | syl5eq 2785 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑡))(2nd ‘𝑓)) = (2nd ‘𝑓)) |
59 | 47, 58 | opeq12d 4769 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 〈((1st
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑡))(1st ‘𝑓)), ((2nd ‘〈(𝐼‘(1st
‘𝑡)), (𝐽‘(2nd
‘𝑡))〉)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑡))(2nd ‘𝑓))〉 = 〈(1st
‘𝑓), (2nd
‘𝑓)〉) |
60 | | eqid 2738 |
. . . . 5
⊢
(comp‘𝑇) =
(comp‘𝑇) |
61 | 39, 29 | syldan 594 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉 ∈ (𝑡(Hom ‘𝑇)𝑡)) |
62 | 1, 4, 26, 38, 53, 60, 35, 39, 39, 41, 61 | xpcco 17549 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉(〈𝑠, 𝑡〉(comp‘𝑇)𝑡)𝑓) = 〈((1st
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑡))(1st ‘𝑓)), ((2nd ‘〈(𝐼‘(1st
‘𝑡)), (𝐽‘(2nd
‘𝑡))〉)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑡))(2nd ‘𝑓))〉) |
63 | | 1st2nd2 7753 |
. . . . 5
⊢ (𝑓 ∈ (((1st
‘𝑠)(Hom ‘𝐶)(1st ‘𝑡)) × ((2nd
‘𝑠)(Hom ‘𝐷)(2nd ‘𝑡))) → 𝑓 = 〈(1st ‘𝑓), (2nd ‘𝑓)〉) |
64 | 43, 63 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 = 〈(1st ‘𝑓), (2nd ‘𝑓)〉) |
65 | 59, 62, 64 | 3eqtr4d 2783 |
. . 3
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉(〈𝑠, 𝑡〉(comp‘𝑇)𝑡)𝑓) = 𝑓) |
66 | 32 | oveq2i 7181 |
. . . . . 6
⊢
((1st ‘𝑔)(〈(1st ‘𝑡), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)) = ((1st
‘𝑔)(〈(1st ‘𝑡), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(𝐼‘(1st ‘𝑡))) |
67 | | simpr2l 1233 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑢 ∈ (𝑋 × 𝑌)) |
68 | | xp1st 7746 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝑋 × 𝑌) → (1st ‘𝑢) ∈ 𝑋) |
69 | 67, 68 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘𝑢) ∈ 𝑋) |
70 | | simpr32 1265 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢)) |
71 | 1, 4, 11, 18, 26, 39, 67 | xpchom 17546 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑡(Hom ‘𝑇)𝑢) = (((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑢)) × ((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑢)))) |
72 | 70, 71 | eleqtrd 2835 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 ∈ (((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑢)) × ((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑢)))) |
73 | | xp1st 7746 |
. . . . . . . 8
⊢ (𝑔 ∈ (((1st
‘𝑡)(Hom ‘𝐶)(1st ‘𝑢)) × ((2nd
‘𝑡)(Hom ‘𝐷)(2nd ‘𝑢))) → (1st
‘𝑔) ∈
((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑢))) |
74 | 72, 73 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘𝑔) ∈ ((1st
‘𝑡)(Hom ‘𝐶)(1st ‘𝑢))) |
75 | 2, 11, 12, 34, 40, 38, 69, 74 | catrid 17058 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘𝑔)(〈(1st
‘𝑡), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(𝐼‘(1st ‘𝑡))) = (1st
‘𝑔)) |
76 | 66, 75 | syl5eq 2785 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘𝑔)(〈(1st
‘𝑡), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘〈(𝐼‘(1st
‘𝑡)), (𝐽‘(2nd
‘𝑡))〉)) =
(1st ‘𝑔)) |
77 | 48 | oveq2i 7181 |
. . . . . 6
⊢
((2nd ‘𝑔)(〈(2nd ‘𝑡), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)) = ((2nd
‘𝑔)(〈(2nd ‘𝑡), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(𝐽‘(2nd ‘𝑡))) |
78 | | xp2nd 7747 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝑋 × 𝑌) → (2nd ‘𝑢) ∈ 𝑌) |
79 | 67, 78 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘𝑢) ∈ 𝑌) |
80 | | xp2nd 7747 |
. . . . . . . 8
⊢ (𝑔 ∈ (((1st
‘𝑡)(Hom ‘𝐶)(1st ‘𝑢)) × ((2nd
‘𝑡)(Hom ‘𝐷)(2nd ‘𝑢))) → (2nd
‘𝑔) ∈
((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑢))) |
81 | 72, 80 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘𝑔) ∈ ((2nd
‘𝑡)(Hom ‘𝐷)(2nd ‘𝑢))) |
82 | 3, 18, 19, 50, 54, 53, 79, 81 | catrid 17058 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘𝑔)(〈(2nd
‘𝑡), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(𝐽‘(2nd ‘𝑡))) = (2nd
‘𝑔)) |
83 | 77, 82 | syl5eq 2785 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘𝑔)(〈(2nd
‘𝑡), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘〈(𝐼‘(1st
‘𝑡)), (𝐽‘(2nd
‘𝑡))〉)) =
(2nd ‘𝑔)) |
84 | 76, 83 | opeq12d 4769 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 〈((1st
‘𝑔)(〈(1st ‘𝑡), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)), ((2nd
‘𝑔)(〈(2nd ‘𝑡), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉))〉 =
〈(1st ‘𝑔), (2nd ‘𝑔)〉) |
85 | 1, 4, 26, 38, 53, 60, 39, 39, 67, 61, 70 | xpcco 17549 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(〈𝑡, 𝑡〉(comp‘𝑇)𝑢)〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉) =
〈((1st ‘𝑔)(〈(1st ‘𝑡), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)), ((2nd
‘𝑔)(〈(2nd ‘𝑡), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd
‘〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉))〉) |
86 | | 1st2nd2 7753 |
. . . . 5
⊢ (𝑔 ∈ (((1st
‘𝑡)(Hom ‘𝐶)(1st ‘𝑢)) × ((2nd
‘𝑡)(Hom ‘𝐷)(2nd ‘𝑢))) → 𝑔 = 〈(1st ‘𝑔), (2nd ‘𝑔)〉) |
87 | 72, 86 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 = 〈(1st ‘𝑔), (2nd ‘𝑔)〉) |
88 | 84, 85, 87 | 3eqtr4d 2783 |
. . 3
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(〈𝑡, 𝑡〉(comp‘𝑇)𝑢)〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉) = 𝑔) |
89 | 2, 11, 38, 34, 37, 40, 69, 45, 74 | catcocl 17059 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘𝑔)(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)) ∈ ((1st ‘𝑠)(Hom ‘𝐶)(1st ‘𝑢))) |
90 | 3, 18, 53, 50, 52, 54, 79, 56, 81 | catcocl 17059 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘𝑔)(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓)) ∈ ((2nd ‘𝑠)(Hom ‘𝐷)(2nd ‘𝑢))) |
91 | 89, 90 | opelxpd 5563 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 〈((1st
‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)), ((2nd
‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓))〉 ∈
(((1st ‘𝑠)(Hom ‘𝐶)(1st ‘𝑢)) × ((2nd ‘𝑠)(Hom ‘𝐷)(2nd ‘𝑢)))) |
92 | 1, 4, 26, 38, 53, 60, 35, 39, 67, 41, 70 | xpcco 17549 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓) = 〈((1st ‘𝑔)(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓))〉) |
93 | 1, 4, 11, 18, 26, 35, 67 | xpchom 17546 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑠(Hom ‘𝑇)𝑢) = (((1st ‘𝑠)(Hom ‘𝐶)(1st ‘𝑢)) × ((2nd ‘𝑠)(Hom ‘𝐷)(2nd ‘𝑢)))) |
94 | 91, 92, 93 | 3eltr4d 2848 |
. . 3
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓) ∈ (𝑠(Hom ‘𝑇)𝑢)) |
95 | | simpr2r 1234 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑣 ∈ (𝑋 × 𝑌)) |
96 | | xp1st 7746 |
. . . . . . . 8
⊢ (𝑣 ∈ (𝑋 × 𝑌) → (1st ‘𝑣) ∈ 𝑋) |
97 | 95, 96 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘𝑣) ∈ 𝑋) |
98 | | simpr33 1266 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)) |
99 | 1, 4, 11, 18, 26, 67, 95 | xpchom 17546 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑢(Hom ‘𝑇)𝑣) = (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣)))) |
100 | 98, 99 | eleqtrd 2835 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ℎ ∈ (((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣)))) |
101 | | xp1st 7746 |
. . . . . . . 8
⊢ (ℎ ∈ (((1st
‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd
‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))) → (1st
‘ℎ) ∈
((1st ‘𝑢)(Hom ‘𝐶)(1st ‘𝑣))) |
102 | 100, 101 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘ℎ) ∈ ((1st
‘𝑢)(Hom ‘𝐶)(1st ‘𝑣))) |
103 | 2, 11, 38, 34, 37, 40, 69, 45, 74, 97, 102 | catass 17060 |
. . . . . 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 ‘𝑓)))) |
104 | 1, 4, 26, 38, 53, 60, 39, 67, 95, 70, 98 | xpcco 17549 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔) = 〈((1st ‘ℎ)(〈(1st
‘𝑡), (1st
‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)), ((2nd ‘ℎ)(〈(2nd
‘𝑡), (2nd
‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))〉) |
105 | 104 | fveq2d 6678 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔)) = (1st
‘〈((1st ‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)), ((2nd
‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))〉)) |
106 | | ovex 7203 |
. . . . . . . . 9
⊢
((1st ‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)) ∈ V |
107 | | ovex 7203 |
. . . . . . . . 9
⊢
((2nd ‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔)) ∈ V |
108 | 106, 107 | op1st 7722 |
. . . . . . . 8
⊢
(1st ‘〈((1st ‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)), ((2nd
‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))〉) = ((1st
‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)) |
109 | 105, 108 | eqtrdi 2789 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔)) = ((1st ‘ℎ)(〈(1st
‘𝑡), (1st
‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔))) |
110 | 109 | oveq1d 7185 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔))(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑓)) = (((1st
‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔))(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑓))) |
111 | 92 | fveq2d 6678 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)) = (1st
‘〈((1st ‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)), ((2nd
‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓))〉)) |
112 | | ovex 7203 |
. . . . . . . . 9
⊢
((1st ‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)) ∈ V |
113 | | ovex 7203 |
. . . . . . . . 9
⊢
((2nd ‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓)) ∈ V |
114 | 112, 113 | op1st 7722 |
. . . . . . . 8
⊢
(1st ‘〈((1st ‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)), ((2nd
‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓))〉) = ((1st
‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)) |
115 | 111, 114 | eqtrdi 2789 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1st ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)) = ((1st ‘𝑔)(〈(1st
‘𝑠), (1st
‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓))) |
116 | 115 | oveq2d 7186 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘ℎ)(〈(1st
‘𝑠), (1st
‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓))) = ((1st ‘ℎ)(〈(1st
‘𝑠), (1st
‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))((1st ‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)))) |
117 | 103, 110,
116 | 3eqtr4d 2783 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔))(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑓)) = ((1st
‘ℎ)(〈(1st ‘𝑠), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)))) |
118 | | xp2nd 7747 |
. . . . . . . 8
⊢ (𝑣 ∈ (𝑋 × 𝑌) → (2nd ‘𝑣) ∈ 𝑌) |
119 | 95, 118 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘𝑣) ∈ 𝑌) |
120 | | xp2nd 7747 |
. . . . . . . 8
⊢ (ℎ ∈ (((1st
‘𝑢)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd
‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))) → (2nd
‘ℎ) ∈
((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))) |
121 | 100, 120 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘ℎ) ∈ ((2nd
‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))) |
122 | 3, 18, 53, 50, 52, 54, 79, 56, 81, 119, 121 | catass 17060 |
. . . . . 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 ‘𝑓)))) |
123 | 104 | fveq2d 6678 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔)) = (2nd
‘〈((1st ‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)), ((2nd
‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))〉)) |
124 | 106, 107 | op2nd 7723 |
. . . . . . . 8
⊢
(2nd ‘〈((1st ‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)), ((2nd
‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))〉) = ((2nd
‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔)) |
125 | 123, 124 | eqtrdi 2789 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔)) = ((2nd ‘ℎ)(〈(2nd
‘𝑡), (2nd
‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))) |
126 | 125 | oveq1d 7185 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔))(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑓)) = (((2nd
‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑓))) |
127 | 92 | fveq2d 6678 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)) = (2nd
‘〈((1st ‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)), ((2nd
‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓))〉)) |
128 | 112, 113 | op2nd 7723 |
. . . . . . . 8
⊢
(2nd ‘〈((1st ‘𝑔)(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑢))(1st ‘𝑓)), ((2nd
‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓))〉) = ((2nd
‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓)) |
129 | 127, 128 | eqtrdi 2789 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2nd ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)) = ((2nd ‘𝑔)(〈(2nd
‘𝑠), (2nd
‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓))) |
130 | 129 | oveq2d 7186 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘ℎ)(〈(2nd
‘𝑠), (2nd
‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓))) = ((2nd ‘ℎ)(〈(2nd
‘𝑠), (2nd
‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))((2nd ‘𝑔)(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑢))(2nd ‘𝑓)))) |
131 | 122, 126,
130 | 3eqtr4d 2783 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔))(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑓)) = ((2nd
‘ℎ)(〈(2nd ‘𝑠), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)))) |
132 | 117, 131 | opeq12d 4769 |
. . . 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‘𝑇)𝑢)𝑓)))〉) |
133 | 2, 11, 38, 34, 40, 69, 97, 74, 102 | catcocl 17059 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1st ‘ℎ)(〈(1st
‘𝑡), (1st
‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)) ∈ ((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑣))) |
134 | 3, 18, 53, 50, 54, 79, 119, 81, 121 | catcocl 17059 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2nd ‘ℎ)(〈(2nd
‘𝑡), (2nd
‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔)) ∈ ((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑣))) |
135 | 133, 134 | opelxpd 5563 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 〈((1st
‘ℎ)(〈(1st ‘𝑡), (1st ‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑔)), ((2nd
‘ℎ)(〈(2nd ‘𝑡), (2nd ‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑔))〉 ∈
(((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑣)))) |
136 | 1, 4, 11, 18, 26, 39, 95 | xpchom 17546 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑡(Hom ‘𝑇)𝑣) = (((1st ‘𝑡)(Hom ‘𝐶)(1st ‘𝑣)) × ((2nd ‘𝑡)(Hom ‘𝐷)(2nd ‘𝑣)))) |
137 | 135, 104,
136 | 3eltr4d 2848 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔) ∈ (𝑡(Hom ‘𝑇)𝑣)) |
138 | 1, 4, 26, 38, 53, 60, 35, 39, 95, 41, 137 | xpcco 17549 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔)(〈𝑠, 𝑡〉(comp‘𝑇)𝑣)𝑓) = 〈((1st ‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔))(〈(1st ‘𝑠), (1st ‘𝑡)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘𝑓)), ((2nd
‘(ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔))(〈(2nd ‘𝑠), (2nd ‘𝑡)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘𝑓))〉) |
139 | 1, 4, 26, 38, 53, 60, 35, 67, 95, 94, 98 | xpcco 17549 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (ℎ(〈𝑠, 𝑢〉(comp‘𝑇)𝑣)(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)) = 〈((1st ‘ℎ)(〈(1st
‘𝑠), (1st
‘𝑢)〉(comp‘𝐶)(1st ‘𝑣))(1st ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓))), ((2nd ‘ℎ)(〈(2nd
‘𝑠), (2nd
‘𝑢)〉(comp‘𝐷)(2nd ‘𝑣))(2nd ‘(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓)))〉) |
140 | 132, 138,
139 | 3eqtr4d 2783 |
. . 3
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((ℎ(〈𝑡, 𝑢〉(comp‘𝑇)𝑣)𝑔)(〈𝑠, 𝑡〉(comp‘𝑇)𝑣)𝑓) = (ℎ(〈𝑠, 𝑢〉(comp‘𝑇)𝑣)(𝑔(〈𝑠, 𝑡〉(comp‘𝑇)𝑢)𝑓))) |
141 | 5, 6, 7, 9, 10, 29, 65, 88, 94, 140 | iscatd2 17055 |
. 2
⊢ (𝜑 → (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑡 ∈ (𝑋 × 𝑌) ↦ 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉))) |
142 | | vex 3402 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
143 | | vex 3402 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
144 | 142, 143 | op1std 7724 |
. . . . . . 7
⊢ (𝑡 = 〈𝑥, 𝑦〉 → (1st ‘𝑡) = 𝑥) |
145 | 144 | fveq2d 6678 |
. . . . . 6
⊢ (𝑡 = 〈𝑥, 𝑦〉 → (𝐼‘(1st ‘𝑡)) = (𝐼‘𝑥)) |
146 | 142, 143 | op2ndd 7725 |
. . . . . . 7
⊢ (𝑡 = 〈𝑥, 𝑦〉 → (2nd ‘𝑡) = 𝑦) |
147 | 146 | fveq2d 6678 |
. . . . . 6
⊢ (𝑡 = 〈𝑥, 𝑦〉 → (𝐽‘(2nd ‘𝑡)) = (𝐽‘𝑦)) |
148 | 145, 147 | opeq12d 4769 |
. . . . 5
⊢ (𝑡 = 〈𝑥, 𝑦〉 → 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉 = 〈(𝐼‘𝑥), (𝐽‘𝑦)〉) |
149 | 148 | mpompt 7280 |
. . . 4
⊢ (𝑡 ∈ (𝑋 × 𝑌) ↦ 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐼‘𝑥), (𝐽‘𝑦)〉) |
150 | 149 | eqeq2i 2751 |
. . 3
⊢
((Id‘𝑇) =
(𝑡 ∈ (𝑋 × 𝑌) ↦ 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉) ↔ (Id‘𝑇) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐼‘𝑥), (𝐽‘𝑦)〉)) |
151 | 150 | anbi2i 626 |
. 2
⊢ ((𝑇 ∈ Cat ∧
(Id‘𝑇) = (𝑡 ∈ (𝑋 × 𝑌) ↦ 〈(𝐼‘(1st ‘𝑡)), (𝐽‘(2nd ‘𝑡))〉)) ↔ (𝑇 ∈ Cat ∧
(Id‘𝑇) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐼‘𝑥), (𝐽‘𝑦)〉))) |
152 | 141, 151 | sylib 221 |
1
⊢ (𝜑 → (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐼‘𝑥), (𝐽‘𝑦)〉))) |