Step | Hyp | Ref
| Expression |
1 | | xpccat.t |
. . . . 5
⊢ 𝑇 = (𝐶 ×_{c} 𝐷) |
2 | | xpccat.x |
. . . . 5
⊢ 𝑋 = (Base‘𝐶) |
3 | | xpccat.y |
. . . . 5
⊢ 𝑌 = (Base‘𝐷) |
4 | 1, 2, 3 | xpcbas 17406 |
. . . 4
⊢ (𝑋 × 𝑌) = (Base‘𝑇) |
5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑋 × 𝑌) = (Base‘𝑇)) |
6 | | eqidd 2822 |
. . 3
⊢ (𝜑 → (Hom ‘𝑇) = (Hom ‘𝑇)) |
7 | | eqidd 2822 |
. . 3
⊢ (𝜑 → (comp‘𝑇) = (comp‘𝑇)) |
8 | 1 | ovexi 7164 |
. . . 4
⊢ 𝑇 ∈ V |
9 | 8 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑇 ∈ V) |
10 | | biid 264 |
. . 3
⊢ (((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣))) ↔ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) |
11 | | eqid 2821 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
12 | | xpccat.i |
. . . . . 6
⊢ 𝐼 = (Id‘𝐶) |
13 | | xpccat.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ Cat) |
14 | 13 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝐶 ∈ Cat) |
15 | | xp1st 7696 |
. . . . . . 7
⊢ (𝑡 ∈ (𝑋 × 𝑌) → (1^{st} ‘𝑡) ∈ 𝑋) |
16 | 15 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (1^{st} ‘𝑡) ∈ 𝑋) |
17 | 2, 11, 12, 14, 16 | catidcl 16931 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (𝐼‘(1^{st} ‘𝑡)) ∈ ((1^{st}
‘𝑡)(Hom ‘𝐶)(1^{st} ‘𝑡))) |
18 | | eqid 2821 |
. . . . . 6
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
19 | | xpccat.j |
. . . . . 6
⊢ 𝐽 = (Id‘𝐷) |
20 | | xpccat.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ Cat) |
21 | 20 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝐷 ∈ Cat) |
22 | | xp2nd 7697 |
. . . . . . 7
⊢ (𝑡 ∈ (𝑋 × 𝑌) → (2^{nd} ‘𝑡) ∈ 𝑌) |
23 | 22 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (2^{nd} ‘𝑡) ∈ 𝑌) |
24 | 3, 18, 19, 21, 23 | catidcl 16931 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (𝐽‘(2^{nd} ‘𝑡)) ∈ ((2^{nd}
‘𝑡)(Hom ‘𝐷)(2^{nd} ‘𝑡))) |
25 | 17, 24 | opelxpd 5566 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → ⟨(𝐼‘(1^{st} ‘𝑡)), (𝐽‘(2^{nd} ‘𝑡))⟩ ∈
(((1^{st} ‘𝑡)(Hom ‘𝐶)(1^{st} ‘𝑡)) × ((2^{nd} ‘𝑡)(Hom ‘𝐷)(2^{nd} ‘𝑡)))) |
26 | | eqid 2821 |
. . . . 5
⊢ (Hom
‘𝑇) = (Hom
‘𝑇) |
27 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → 𝑡 ∈ (𝑋 × 𝑌)) |
28 | 1, 4, 11, 18, 26, 27, 27 | xpchom 17408 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → (𝑡(Hom ‘𝑇)𝑡) = (((1^{st} ‘𝑡)(Hom ‘𝐶)(1^{st} ‘𝑡)) × ((2^{nd} ‘𝑡)(Hom ‘𝐷)(2^{nd} ‘𝑡)))) |
29 | 25, 28 | eleqtrrd 2915 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋 × 𝑌)) → ⟨(𝐼‘(1^{st} ‘𝑡)), (𝐽‘(2^{nd} ‘𝑡))⟩ ∈ (𝑡(Hom ‘𝑇)𝑡)) |
30 | | fvex 6656 |
. . . . . . . 8
⊢ (𝐼‘(1^{st}
‘𝑡)) ∈
V |
31 | | fvex 6656 |
. . . . . . . 8
⊢ (𝐽‘(2^{nd}
‘𝑡)) ∈
V |
32 | 30, 31 | op1st 7672 |
. . . . . . 7
⊢
(1^{st} ‘⟨(𝐼‘(1^{st} ‘𝑡)), (𝐽‘(2^{nd} ‘𝑡))⟩) = (𝐼‘(1^{st} ‘𝑡)) |
33 | 32 | oveq1i 7140 |
. . . . . 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} ‘𝑓)) |
34 | 13 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝐶 ∈ Cat) |
35 | | simpr1l 1227 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑠 ∈ (𝑋 × 𝑌)) |
36 | | xp1st 7696 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝑋 × 𝑌) → (1^{st} ‘𝑠) ∈ 𝑋) |
37 | 35, 36 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^{st} ‘𝑠) ∈ 𝑋) |
38 | | eqid 2821 |
. . . . . . 7
⊢
(comp‘𝐶) =
(comp‘𝐶) |
39 | | simpr1r 1228 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑡 ∈ (𝑋 × 𝑌)) |
40 | 39, 15 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^{st} ‘𝑡) ∈ 𝑋) |
41 | | simpr31 1260 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡)) |
42 | 1, 4, 11, 18, 26, 35, 39 | xpchom 17408 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑠(Hom ‘𝑇)𝑡) = (((1^{st} ‘𝑠)(Hom ‘𝐶)(1^{st} ‘𝑡)) × ((2^{nd} ‘𝑠)(Hom ‘𝐷)(2^{nd} ‘𝑡)))) |
43 | 41, 42 | eleqtrd 2914 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 ∈ (((1^{st} ‘𝑠)(Hom ‘𝐶)(1^{st} ‘𝑡)) × ((2^{nd} ‘𝑠)(Hom ‘𝐷)(2^{nd} ‘𝑡)))) |
44 | | xp1st 7696 |
. . . . . . . 8
⊢ (𝑓 ∈ (((1^{st}
‘𝑠)(Hom ‘𝐶)(1^{st} ‘𝑡)) × ((2^{nd}
‘𝑠)(Hom ‘𝐷)(2^{nd} ‘𝑡))) → (1^{st}
‘𝑓) ∈
((1^{st} ‘𝑠)(Hom ‘𝐶)(1^{st} ‘𝑡))) |
45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^{st} ‘𝑓) ∈ ((1^{st}
‘𝑠)(Hom ‘𝐶)(1^{st} ‘𝑡))) |
46 | 2, 11, 12, 34, 37, 38, 40, 45 | catlid 16932 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((𝐼‘(1^{st} ‘𝑡))(⟨(1^{st}
‘𝑠), (1^{st}
‘𝑡)⟩(comp‘𝐶)(1^{st} ‘𝑡))(1^{st} ‘𝑓)) = (1^{st} ‘𝑓)) |
47 | 33, 46 | syl5eq 2868 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1^{st}
‘⟨(𝐼‘(1^{st} ‘𝑡)), (𝐽‘(2^{nd} ‘𝑡))⟩)(⟨(1^{st}
‘𝑠), (1^{st}
‘𝑡)⟩(comp‘𝐶)(1^{st} ‘𝑡))(1^{st} ‘𝑓)) = (1^{st} ‘𝑓)) |
48 | 30, 31 | op2nd 7673 |
. . . . . . 7
⊢
(2^{nd} ‘⟨(𝐼‘(1^{st} ‘𝑡)), (𝐽‘(2^{nd} ‘𝑡))⟩) = (𝐽‘(2^{nd} ‘𝑡)) |
49 | 48 | oveq1i 7140 |
. . . . . 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} ‘𝑓)) |
50 | 20 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝐷 ∈ Cat) |
51 | | xp2nd 7697 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝑋 × 𝑌) → (2^{nd} ‘𝑠) ∈ 𝑌) |
52 | 35, 51 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^{nd} ‘𝑠) ∈ 𝑌) |
53 | | eqid 2821 |
. . . . . . 7
⊢
(comp‘𝐷) =
(comp‘𝐷) |
54 | 39, 22 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^{nd} ‘𝑡) ∈ 𝑌) |
55 | | xp2nd 7697 |
. . . . . . . 8
⊢ (𝑓 ∈ (((1^{st}
‘𝑠)(Hom ‘𝐶)(1^{st} ‘𝑡)) × ((2^{nd}
‘𝑠)(Hom ‘𝐷)(2^{nd} ‘𝑡))) → (2^{nd}
‘𝑓) ∈
((2^{nd} ‘𝑠)(Hom ‘𝐷)(2^{nd} ‘𝑡))) |
56 | 43, 55 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^{nd} ‘𝑓) ∈ ((2^{nd}
‘𝑠)(Hom ‘𝐷)(2^{nd} ‘𝑡))) |
57 | 3, 18, 19, 50, 52, 53, 54, 56 | catlid 16932 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((𝐽‘(2^{nd} ‘𝑡))(⟨(2^{nd}
‘𝑠), (2^{nd}
‘𝑡)⟩(comp‘𝐷)(2^{nd} ‘𝑡))(2^{nd} ‘𝑓)) = (2^{nd} ‘𝑓)) |
58 | 49, 57 | syl5eq 2868 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2^{nd}
‘⟨(𝐼‘(1^{st} ‘𝑡)), (𝐽‘(2^{nd} ‘𝑡))⟩)(⟨(2^{nd}
‘𝑠), (2^{nd}
‘𝑡)⟩(comp‘𝐷)(2^{nd} ‘𝑡))(2^{nd} ‘𝑓)) = (2^{nd} ‘𝑓)) |
59 | 47, 58 | opeq12d 4784 |
. . . 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}
‘𝑓)⟩) |
60 | | eqid 2821 |
. . . . 5
⊢
(comp‘𝑇) =
(comp‘𝑇) |
61 | 39, 29 | syldan 594 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ⟨(𝐼‘(1^{st} ‘𝑡)), (𝐽‘(2^{nd} ‘𝑡))⟩ ∈ (𝑡(Hom ‘𝑇)𝑡)) |
62 | 1, 4, 26, 38, 53, 60, 35, 39, 39, 41, 61 | xpcco 17411 |
. . . 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} ‘𝑓))⟩) |
63 | | 1st2nd2 7703 |
. . . . 5
⊢ (𝑓 ∈ (((1^{st}
‘𝑠)(Hom ‘𝐶)(1^{st} ‘𝑡)) × ((2^{nd}
‘𝑠)(Hom ‘𝐷)(2^{nd} ‘𝑡))) → 𝑓 = ⟨(1^{st} ‘𝑓), (2^{nd} ‘𝑓)⟩) |
64 | 43, 63 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑓 = ⟨(1^{st} ‘𝑓), (2^{nd} ‘𝑓)⟩) |
65 | 59, 62, 64 | 3eqtr4d 2866 |
. . 3
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (⟨(𝐼‘(1^{st} ‘𝑡)), (𝐽‘(2^{nd} ‘𝑡))⟩(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑡)𝑓) = 𝑓) |
66 | 32 | oveq2i 7141 |
. . . . . 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} ‘𝑡))) |
67 | | simpr2l 1229 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑢 ∈ (𝑋 × 𝑌)) |
68 | | xp1st 7696 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝑋 × 𝑌) → (1^{st} ‘𝑢) ∈ 𝑋) |
69 | 67, 68 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^{st} ‘𝑢) ∈ 𝑋) |
70 | | simpr32 1261 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢)) |
71 | 1, 4, 11, 18, 26, 39, 67 | xpchom 17408 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑡(Hom ‘𝑇)𝑢) = (((1^{st} ‘𝑡)(Hom ‘𝐶)(1^{st} ‘𝑢)) × ((2^{nd} ‘𝑡)(Hom ‘𝐷)(2^{nd} ‘𝑢)))) |
72 | 70, 71 | eleqtrd 2914 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 ∈ (((1^{st} ‘𝑡)(Hom ‘𝐶)(1^{st} ‘𝑢)) × ((2^{nd} ‘𝑡)(Hom ‘𝐷)(2^{nd} ‘𝑢)))) |
73 | | xp1st 7696 |
. . . . . . . 8
⊢ (𝑔 ∈ (((1^{st}
‘𝑡)(Hom ‘𝐶)(1^{st} ‘𝑢)) × ((2^{nd}
‘𝑡)(Hom ‘𝐷)(2^{nd} ‘𝑢))) → (1^{st}
‘𝑔) ∈
((1^{st} ‘𝑡)(Hom ‘𝐶)(1^{st} ‘𝑢))) |
74 | 72, 73 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^{st} ‘𝑔) ∈ ((1^{st}
‘𝑡)(Hom ‘𝐶)(1^{st} ‘𝑢))) |
75 | 2, 11, 12, 34, 40, 38, 69, 74 | catrid 16933 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1^{st} ‘𝑔)(⟨(1^{st}
‘𝑡), (1^{st}
‘𝑡)⟩(comp‘𝐶)(1^{st} ‘𝑢))(𝐼‘(1^{st} ‘𝑡))) = (1^{st}
‘𝑔)) |
76 | 66, 75 | syl5eq 2868 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1^{st} ‘𝑔)(⟨(1^{st}
‘𝑡), (1^{st}
‘𝑡)⟩(comp‘𝐶)(1^{st} ‘𝑢))(1^{st} ‘⟨(𝐼‘(1^{st}
‘𝑡)), (𝐽‘(2^{nd}
‘𝑡))⟩)) =
(1^{st} ‘𝑔)) |
77 | 48 | oveq2i 7141 |
. . . . . 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} ‘𝑡))) |
78 | | xp2nd 7697 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝑋 × 𝑌) → (2^{nd} ‘𝑢) ∈ 𝑌) |
79 | 67, 78 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^{nd} ‘𝑢) ∈ 𝑌) |
80 | | xp2nd 7697 |
. . . . . . . 8
⊢ (𝑔 ∈ (((1^{st}
‘𝑡)(Hom ‘𝐶)(1^{st} ‘𝑢)) × ((2^{nd}
‘𝑡)(Hom ‘𝐷)(2^{nd} ‘𝑢))) → (2^{nd}
‘𝑔) ∈
((2^{nd} ‘𝑡)(Hom ‘𝐷)(2^{nd} ‘𝑢))) |
81 | 72, 80 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^{nd} ‘𝑔) ∈ ((2^{nd}
‘𝑡)(Hom ‘𝐷)(2^{nd} ‘𝑢))) |
82 | 3, 18, 19, 50, 54, 53, 79, 81 | catrid 16933 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘𝑡), (2^{nd}
‘𝑡)⟩(comp‘𝐷)(2^{nd} ‘𝑢))(𝐽‘(2^{nd} ‘𝑡))) = (2^{nd}
‘𝑔)) |
83 | 77, 82 | syl5eq 2868 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘𝑡), (2^{nd}
‘𝑡)⟩(comp‘𝐷)(2^{nd} ‘𝑢))(2^{nd} ‘⟨(𝐼‘(1^{st}
‘𝑡)), (𝐽‘(2^{nd}
‘𝑡))⟩)) =
(2^{nd} ‘𝑔)) |
84 | 76, 83 | opeq12d 4784 |
. . . 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} ‘𝑔)⟩) |
85 | 1, 4, 26, 38, 53, 60, 39, 39, 67, 61, 70 | xpcco 17411 |
. . . 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} ‘𝑡))⟩))⟩) |
86 | | 1st2nd2 7703 |
. . . . 5
⊢ (𝑔 ∈ (((1^{st}
‘𝑡)(Hom ‘𝐶)(1^{st} ‘𝑢)) × ((2^{nd}
‘𝑡)(Hom ‘𝐷)(2^{nd} ‘𝑢))) → 𝑔 = ⟨(1^{st} ‘𝑔), (2^{nd} ‘𝑔)⟩) |
87 | 72, 86 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑔 = ⟨(1^{st} ‘𝑔), (2^{nd} ‘𝑔)⟩) |
88 | 84, 85, 87 | 3eqtr4d 2866 |
. . 3
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(⟨𝑡, 𝑡⟩(comp‘𝑇)𝑢)⟨(𝐼‘(1^{st} ‘𝑡)), (𝐽‘(2^{nd} ‘𝑡))⟩) = 𝑔) |
89 | 2, 11, 38, 34, 37, 40, 69, 45, 74 | catcocl 16934 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1^{st} ‘𝑔)(⟨(1^{st}
‘𝑠), (1^{st}
‘𝑡)⟩(comp‘𝐶)(1^{st} ‘𝑢))(1^{st} ‘𝑓)) ∈ ((1^{st} ‘𝑠)(Hom ‘𝐶)(1^{st} ‘𝑢))) |
90 | 3, 18, 53, 50, 52, 54, 79, 56, 81 | catcocl 16934 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘𝑠), (2^{nd}
‘𝑡)⟩(comp‘𝐷)(2^{nd} ‘𝑢))(2^{nd} ‘𝑓)) ∈ ((2^{nd} ‘𝑠)(Hom ‘𝐷)(2^{nd} ‘𝑢))) |
91 | 89, 90 | opelxpd 5566 |
. . . 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} ‘𝑢)))) |
92 | 1, 4, 26, 38, 53, 60, 35, 39, 67, 41, 70 | xpcco 17411 |
. . . 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} ‘𝑓))⟩) |
93 | 1, 4, 11, 18, 26, 35, 67 | xpchom 17408 |
. . . 4
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑠(Hom ‘𝑇)𝑢) = (((1^{st} ‘𝑠)(Hom ‘𝐶)(1^{st} ‘𝑢)) × ((2^{nd} ‘𝑠)(Hom ‘𝐷)(2^{nd} ‘𝑢)))) |
94 | 91, 92, 93 | 3eltr4d 2927 |
. . 3
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓) ∈ (𝑠(Hom ‘𝑇)𝑢)) |
95 | | simpr2r 1230 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → 𝑣 ∈ (𝑋 × 𝑌)) |
96 | | xp1st 7696 |
. . . . . . . 8
⊢ (𝑣 ∈ (𝑋 × 𝑌) → (1^{st} ‘𝑣) ∈ 𝑋) |
97 | 95, 96 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^{st} ‘𝑣) ∈ 𝑋) |
98 | | simpr33 1262 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)) |
99 | 1, 4, 11, 18, 26, 67, 95 | xpchom 17408 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑢(Hom ‘𝑇)𝑣) = (((1^{st} ‘𝑢)(Hom ‘𝐶)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝐷)(2^{nd} ‘𝑣)))) |
100 | 98, 99 | eleqtrd 2914 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ℎ ∈ (((1^{st} ‘𝑢)(Hom ‘𝐶)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝐷)(2^{nd} ‘𝑣)))) |
101 | | xp1st 7696 |
. . . . . . . 8
⊢ (ℎ ∈ (((1^{st}
‘𝑢)(Hom ‘𝐶)(1^{st} ‘𝑣)) × ((2^{nd}
‘𝑢)(Hom ‘𝐷)(2^{nd} ‘𝑣))) → (1^{st}
‘ℎ) ∈
((1^{st} ‘𝑢)(Hom ‘𝐶)(1^{st} ‘𝑣))) |
102 | 100, 101 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^{st} ‘ℎ) ∈ ((1^{st}
‘𝑢)(Hom ‘𝐶)(1^{st} ‘𝑣))) |
103 | 2, 11, 38, 34, 37, 40, 69, 45, 74, 97, 102 | catass 16935 |
. . . . . 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} ‘𝑓)))) |
104 | 1, 4, 26, 38, 53, 60, 39, 67, 95, 70, 98 | xpcco 17411 |
. . . . . . . . 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} ‘𝑔))⟩) |
105 | 104 | fveq2d 6647 |
. . . . . . . 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} ‘𝑔))⟩)) |
106 | | ovex 7163 |
. . . . . . . . 9
⊢
((1^{st} ‘ℎ)(⟨(1^{st} ‘𝑡), (1^{st} ‘𝑢)⟩(comp‘𝐶)(1^{st} ‘𝑣))(1^{st} ‘𝑔)) ∈ V |
107 | | ovex 7163 |
. . . . . . . . 9
⊢
((2^{nd} ‘ℎ)(⟨(2^{nd} ‘𝑡), (2^{nd} ‘𝑢)⟩(comp‘𝐷)(2^{nd} ‘𝑣))(2^{nd} ‘𝑔)) ∈ V |
108 | 106, 107 | op1st 7672 |
. . . . . . . 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} ‘𝑔)) |
109 | 105, 108 | syl6eq 2872 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^{st} ‘(ℎ(⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)) = ((1^{st} ‘ℎ)(⟨(1^{st}
‘𝑡), (1^{st}
‘𝑢)⟩(comp‘𝐶)(1^{st} ‘𝑣))(1^{st} ‘𝑔))) |
110 | 109 | oveq1d 7145 |
. . . . . 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} ‘𝑓))) |
111 | 92 | fveq2d 6647 |
. . . . . . . 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} ‘𝑓))⟩)) |
112 | | ovex 7163 |
. . . . . . . . 9
⊢
((1^{st} ‘𝑔)(⟨(1^{st} ‘𝑠), (1^{st} ‘𝑡)⟩(comp‘𝐶)(1^{st} ‘𝑢))(1^{st} ‘𝑓)) ∈ V |
113 | | ovex 7163 |
. . . . . . . . 9
⊢
((2^{nd} ‘𝑔)(⟨(2^{nd} ‘𝑠), (2^{nd} ‘𝑡)⟩(comp‘𝐷)(2^{nd} ‘𝑢))(2^{nd} ‘𝑓)) ∈ V |
114 | 112, 113 | op1st 7672 |
. . . . . . . 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} ‘𝑓)) |
115 | 111, 114 | syl6eq 2872 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (1^{st} ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)) = ((1^{st} ‘𝑔)(⟨(1^{st}
‘𝑠), (1^{st}
‘𝑡)⟩(comp‘𝐶)(1^{st} ‘𝑢))(1^{st} ‘𝑓))) |
116 | 115 | oveq2d 7146 |
. . . . . 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} ‘𝑓)))) |
117 | 103, 110,
116 | 3eqtr4d 2866 |
. . . . 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‘𝑇)𝑢)𝑓)))) |
118 | | xp2nd 7697 |
. . . . . . . 8
⊢ (𝑣 ∈ (𝑋 × 𝑌) → (2^{nd} ‘𝑣) ∈ 𝑌) |
119 | 95, 118 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^{nd} ‘𝑣) ∈ 𝑌) |
120 | | xp2nd 7697 |
. . . . . . . 8
⊢ (ℎ ∈ (((1^{st}
‘𝑢)(Hom ‘𝐶)(1^{st} ‘𝑣)) × ((2^{nd}
‘𝑢)(Hom ‘𝐷)(2^{nd} ‘𝑣))) → (2^{nd}
‘ℎ) ∈
((2^{nd} ‘𝑢)(Hom ‘𝐷)(2^{nd} ‘𝑣))) |
121 | 100, 120 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^{nd} ‘ℎ) ∈ ((2^{nd}
‘𝑢)(Hom ‘𝐷)(2^{nd} ‘𝑣))) |
122 | 3, 18, 53, 50, 52, 54, 79, 56, 81, 119, 121 | catass 16935 |
. . . . . 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} ‘𝑓)))) |
123 | 104 | fveq2d 6647 |
. . . . . . . 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} ‘𝑔))⟩)) |
124 | 106, 107 | op2nd 7673 |
. . . . . . . 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} ‘𝑔)) |
125 | 123, 124 | syl6eq 2872 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^{nd} ‘(ℎ(⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)) = ((2^{nd} ‘ℎ)(⟨(2^{nd}
‘𝑡), (2^{nd}
‘𝑢)⟩(comp‘𝐷)(2^{nd} ‘𝑣))(2^{nd} ‘𝑔))) |
126 | 125 | oveq1d 7145 |
. . . . . 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} ‘𝑓))) |
127 | 92 | fveq2d 6647 |
. . . . . . . 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} ‘𝑓))⟩)) |
128 | 112, 113 | op2nd 7673 |
. . . . . . . 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} ‘𝑓)) |
129 | 127, 128 | syl6eq 2872 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (2^{nd} ‘(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓)) = ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘𝑠), (2^{nd}
‘𝑡)⟩(comp‘𝐷)(2^{nd} ‘𝑢))(2^{nd} ‘𝑓))) |
130 | 129 | oveq2d 7146 |
. . . . . 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} ‘𝑓)))) |
131 | 122, 126,
130 | 3eqtr4d 2866 |
. . . . 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‘𝑇)𝑢)𝑓)))) |
132 | 117, 131 | opeq12d 4784 |
. . . 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‘𝑇)𝑢)𝑓)))⟩) |
133 | 2, 11, 38, 34, 40, 69, 97, 74, 102 | catcocl 16934 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((1^{st} ‘ℎ)(⟨(1^{st}
‘𝑡), (1^{st}
‘𝑢)⟩(comp‘𝐶)(1^{st} ‘𝑣))(1^{st} ‘𝑔)) ∈ ((1^{st} ‘𝑡)(Hom ‘𝐶)(1^{st} ‘𝑣))) |
134 | 3, 18, 53, 50, 54, 79, 119, 81, 121 | catcocl 16934 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((2^{nd} ‘ℎ)(⟨(2^{nd}
‘𝑡), (2^{nd}
‘𝑢)⟩(comp‘𝐷)(2^{nd} ‘𝑣))(2^{nd} ‘𝑔)) ∈ ((2^{nd} ‘𝑡)(Hom ‘𝐷)(2^{nd} ‘𝑣))) |
135 | 133, 134 | opelxpd 5566 |
. . . . . 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} ‘𝑣)))) |
136 | 1, 4, 11, 18, 26, 39, 95 | xpchom 17408 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (𝑡(Hom ‘𝑇)𝑣) = (((1^{st} ‘𝑡)(Hom ‘𝐶)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑡)(Hom ‘𝐷)(2^{nd} ‘𝑣)))) |
137 | 135, 104,
136 | 3eltr4d 2927 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → (ℎ(⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔) ∈ (𝑡(Hom ‘𝑇)𝑣)) |
138 | 1, 4, 26, 38, 53, 60, 35, 39, 95, 41, 137 | xpcco 17411 |
. . . 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} ‘𝑓))⟩) |
139 | 1, 4, 26, 38, 53, 60, 35, 67, 95, 94, 98 | xpcco 17411 |
. . . 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‘𝑇)𝑢)𝑓)))⟩) |
140 | 132, 138,
139 | 3eqtr4d 2866 |
. . 3
⊢ ((𝜑 ∧ ((𝑠 ∈ (𝑋 × 𝑌) ∧ 𝑡 ∈ (𝑋 × 𝑌)) ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (𝑋 × 𝑌)) ∧ (𝑓 ∈ (𝑠(Hom ‘𝑇)𝑡) ∧ 𝑔 ∈ (𝑡(Hom ‘𝑇)𝑢) ∧ ℎ ∈ (𝑢(Hom ‘𝑇)𝑣)))) → ((ℎ(⟨𝑡, 𝑢⟩(comp‘𝑇)𝑣)𝑔)(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑣)𝑓) = (ℎ(⟨𝑠, 𝑢⟩(comp‘𝑇)𝑣)(𝑔(⟨𝑠, 𝑡⟩(comp‘𝑇)𝑢)𝑓))) |
141 | 5, 6, 7, 9, 10, 29, 65, 88, 94, 140 | iscatd2 16930 |
. 2
⊢ (𝜑 → (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1^{st} ‘𝑡)), (𝐽‘(2^{nd} ‘𝑡))⟩))) |
142 | | vex 3474 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
143 | | vex 3474 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
144 | 142, 143 | op1std 7674 |
. . . . . . 7
⊢ (𝑡 = ⟨𝑥, 𝑦⟩ → (1^{st} ‘𝑡) = 𝑥) |
145 | 144 | fveq2d 6647 |
. . . . . 6
⊢ (𝑡 = ⟨𝑥, 𝑦⟩ → (𝐼‘(1^{st} ‘𝑡)) = (𝐼‘𝑥)) |
146 | 142, 143 | op2ndd 7675 |
. . . . . . 7
⊢ (𝑡 = ⟨𝑥, 𝑦⟩ → (2^{nd} ‘𝑡) = 𝑦) |
147 | 146 | fveq2d 6647 |
. . . . . 6
⊢ (𝑡 = ⟨𝑥, 𝑦⟩ → (𝐽‘(2^{nd} ‘𝑡)) = (𝐽‘𝑦)) |
148 | 145, 147 | opeq12d 4784 |
. . . . 5
⊢ (𝑡 = ⟨𝑥, 𝑦⟩ → ⟨(𝐼‘(1^{st} ‘𝑡)), (𝐽‘(2^{nd} ‘𝑡))⟩ = ⟨(𝐼‘𝑥), (𝐽‘𝑦)⟩) |
149 | 148 | mpompt 7240 |
. . . 4
⊢ (𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1^{st} ‘𝑡)), (𝐽‘(2^{nd} ‘𝑡))⟩) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐼‘𝑥), (𝐽‘𝑦)⟩) |
150 | 149 | eqeq2i 2834 |
. . 3
⊢
((Id‘𝑇) =
(𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1^{st} ‘𝑡)), (𝐽‘(2^{nd} ‘𝑡))⟩) ↔ (Id‘𝑇) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐼‘𝑥), (𝐽‘𝑦)⟩)) |
151 | 150 | anbi2i 625 |
. 2
⊢ ((𝑇 ∈ Cat ∧
(Id‘𝑇) = (𝑡 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐼‘(1^{st} ‘𝑡)), (𝐽‘(2^{nd} ‘𝑡))⟩)) ↔ (𝑇 ∈ Cat ∧
(Id‘𝑇) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐼‘𝑥), (𝐽‘𝑦)⟩))) |
152 | 141, 151 | sylib 221 |
1
⊢ (𝜑 → (𝑇 ∈ Cat ∧ (Id‘𝑇) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐼‘𝑥), (𝐽‘𝑦)⟩))) |