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