Step | Hyp | Ref
| Expression |
1 | | oppcbas.1 |
. . . . 5
⊢ 𝑂 = (oppCat‘𝐶) |
2 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝐶) =
(Base‘𝐶) |
3 | 1, 2 | oppcbas 16201 |
. . . 4
⊢
(Base‘𝐶) =
(Base‘𝑂) |
4 | 3 | a1i 11 |
. . 3
⊢ (𝐶 ∈ Cat →
(Base‘𝐶) =
(Base‘𝑂)) |
5 | | eqidd 2611 |
. . 3
⊢ (𝐶 ∈ Cat → (Hom
‘𝑂) = (Hom
‘𝑂)) |
6 | | eqidd 2611 |
. . 3
⊢ (𝐶 ∈ Cat →
(comp‘𝑂) =
(comp‘𝑂)) |
7 | | fvex 6113 |
. . . . 5
⊢
(oppCat‘𝐶)
∈ V |
8 | 1, 7 | eqeltri 2684 |
. . . 4
⊢ 𝑂 ∈ V |
9 | 8 | a1i 11 |
. . 3
⊢ (𝐶 ∈ Cat → 𝑂 ∈ V) |
10 | | biid 250 |
. . 3
⊢ (((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ↔ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) |
11 | | eqid 2610 |
. . . . 5
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
12 | | eqid 2610 |
. . . . 5
⊢
(Id‘𝐶) =
(Id‘𝐶) |
13 | | simpl 472 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ 𝑦 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat) |
14 | | simpr 476 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶)) |
15 | 2, 11, 12, 13, 14 | catidcl 16166 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ 𝑦 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑦) ∈ (𝑦(Hom ‘𝐶)𝑦)) |
16 | 11, 1 | oppchom 16198 |
. . . 4
⊢ (𝑦(Hom ‘𝑂)𝑦) = (𝑦(Hom ‘𝐶)𝑦) |
17 | 15, 16 | syl6eleqr 2699 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ 𝑦 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑦) ∈ (𝑦(Hom ‘𝑂)𝑦)) |
18 | | eqid 2610 |
. . . . 5
⊢
(comp‘𝐶) =
(comp‘𝐶) |
19 | | simpr1l 1111 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑥 ∈ (Base‘𝐶)) |
20 | | simpr1r 1112 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑦 ∈ (Base‘𝐶)) |
21 | 2, 18, 1, 19, 20, 20 | oppcco 16200 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (((Id‘𝐶)‘𝑦)(〈𝑥, 𝑦〉(comp‘𝑂)𝑦)𝑓) = (𝑓(〈𝑦, 𝑦〉(comp‘𝐶)𝑥)((Id‘𝐶)‘𝑦))) |
22 | | simpl 472 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝐶 ∈ Cat) |
23 | | simpr31 1144 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦)) |
24 | 11, 1 | oppchom 16198 |
. . . . . 6
⊢ (𝑥(Hom ‘𝑂)𝑦) = (𝑦(Hom ‘𝐶)𝑥) |
25 | 23, 24 | syl6eleq 2698 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) |
26 | 2, 11, 12, 22, 20, 18, 19, 25 | catrid 16168 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑓(〈𝑦, 𝑦〉(comp‘𝐶)𝑥)((Id‘𝐶)‘𝑦)) = 𝑓) |
27 | 21, 26 | eqtrd 2644 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (((Id‘𝐶)‘𝑦)(〈𝑥, 𝑦〉(comp‘𝑂)𝑦)𝑓) = 𝑓) |
28 | | simpr2l 1113 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑧 ∈ (Base‘𝐶)) |
29 | 2, 18, 1, 20, 20, 28 | oppcco 16200 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑔(〈𝑦, 𝑦〉(comp‘𝑂)𝑧)((Id‘𝐶)‘𝑦)) = (((Id‘𝐶)‘𝑦)(〈𝑧, 𝑦〉(comp‘𝐶)𝑦)𝑔)) |
30 | | simpr32 1145 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧)) |
31 | 11, 1 | oppchom 16198 |
. . . . . 6
⊢ (𝑦(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑦) |
32 | 30, 31 | syl6eleq 2698 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑦)) |
33 | 2, 11, 12, 22, 28, 18, 20, 32 | catlid 16167 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (((Id‘𝐶)‘𝑦)(〈𝑧, 𝑦〉(comp‘𝐶)𝑦)𝑔) = 𝑔) |
34 | 29, 33 | eqtrd 2644 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑔(〈𝑦, 𝑦〉(comp‘𝑂)𝑧)((Id‘𝐶)‘𝑦)) = 𝑔) |
35 | 2, 18, 1, 19, 20, 28 | oppcco 16200 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓) = (𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔)) |
36 | 2, 11, 18, 22, 28, 20, 19, 32, 25 | catcocl 16169 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔) ∈ (𝑧(Hom ‘𝐶)𝑥)) |
37 | 35, 36 | eqeltrd 2688 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓) ∈ (𝑧(Hom ‘𝐶)𝑥)) |
38 | 11, 1 | oppchom 16198 |
. . . 4
⊢ (𝑥(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑥) |
39 | 37, 38 | syl6eleqr 2699 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓) ∈ (𝑥(Hom ‘𝑂)𝑧)) |
40 | | simpr2r 1114 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑤 ∈ (Base‘𝐶)) |
41 | | simpr33 1146 |
. . . . . . 7
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)) |
42 | 11, 1 | oppchom 16198 |
. . . . . . 7
⊢ (𝑧(Hom ‘𝑂)𝑤) = (𝑤(Hom ‘𝐶)𝑧) |
43 | 41, 42 | syl6eleq 2698 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ℎ ∈ (𝑤(Hom ‘𝐶)𝑧)) |
44 | 2, 11, 18, 22, 40, 28, 20, 43, 32, 19, 25 | catass 16170 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔)(〈𝑤, 𝑧〉(comp‘𝐶)𝑥)ℎ) = (𝑓(〈𝑤, 𝑦〉(comp‘𝐶)𝑥)(𝑔(〈𝑤, 𝑧〉(comp‘𝐶)𝑦)ℎ))) |
45 | 2, 18, 1, 19, 28, 40 | oppcco 16200 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (ℎ(〈𝑥, 𝑧〉(comp‘𝑂)𝑤)(𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔)) = ((𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔)(〈𝑤, 𝑧〉(comp‘𝐶)𝑥)ℎ)) |
46 | 2, 18, 1, 19, 20, 40 | oppcco 16200 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((𝑔(〈𝑤, 𝑧〉(comp‘𝐶)𝑦)ℎ)(〈𝑥, 𝑦〉(comp‘𝑂)𝑤)𝑓) = (𝑓(〈𝑤, 𝑦〉(comp‘𝐶)𝑥)(𝑔(〈𝑤, 𝑧〉(comp‘𝐶)𝑦)ℎ))) |
47 | 44, 45, 46 | 3eqtr4rd 2655 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((𝑔(〈𝑤, 𝑧〉(comp‘𝐶)𝑦)ℎ)(〈𝑥, 𝑦〉(comp‘𝑂)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝑂)𝑤)(𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔))) |
48 | 2, 18, 1, 20, 28, 40 | oppcco 16200 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (ℎ(〈𝑦, 𝑧〉(comp‘𝑂)𝑤)𝑔) = (𝑔(〈𝑤, 𝑧〉(comp‘𝐶)𝑦)ℎ)) |
49 | 48 | oveq1d 6564 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((ℎ(〈𝑦, 𝑧〉(comp‘𝑂)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝑂)𝑤)𝑓) = ((𝑔(〈𝑤, 𝑧〉(comp‘𝐶)𝑦)ℎ)(〈𝑥, 𝑦〉(comp‘𝑂)𝑤)𝑓)) |
50 | 35 | oveq2d 6565 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (ℎ(〈𝑥, 𝑧〉(comp‘𝑂)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓)) = (ℎ(〈𝑥, 𝑧〉(comp‘𝑂)𝑤)(𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔))) |
51 | 47, 49, 50 | 3eqtr4d 2654 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((ℎ(〈𝑦, 𝑧〉(comp‘𝑂)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝑂)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝑂)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓))) |
52 | 4, 5, 6, 9, 10, 17, 27, 34, 39, 51 | iscatd2 16165 |
. 2
⊢ (𝐶 ∈ Cat → (𝑂 ∈ Cat ∧
(Id‘𝑂) = (𝑦 ∈ (Base‘𝐶) ↦ ((Id‘𝐶)‘𝑦)))) |
53 | 2, 12 | cidfn 16163 |
. . . . 5
⊢ (𝐶 ∈ Cat →
(Id‘𝐶) Fn
(Base‘𝐶)) |
54 | | dffn5 6151 |
. . . . 5
⊢
((Id‘𝐶) Fn
(Base‘𝐶) ↔
(Id‘𝐶) = (𝑦 ∈ (Base‘𝐶) ↦ ((Id‘𝐶)‘𝑦))) |
55 | 53, 54 | sylib 207 |
. . . 4
⊢ (𝐶 ∈ Cat →
(Id‘𝐶) = (𝑦 ∈ (Base‘𝐶) ↦ ((Id‘𝐶)‘𝑦))) |
56 | 55 | eqeq2d 2620 |
. . 3
⊢ (𝐶 ∈ Cat →
((Id‘𝑂) =
(Id‘𝐶) ↔
(Id‘𝑂) = (𝑦 ∈ (Base‘𝐶) ↦ ((Id‘𝐶)‘𝑦)))) |
57 | 56 | anbi2d 736 |
. 2
⊢ (𝐶 ∈ Cat → ((𝑂 ∈ Cat ∧
(Id‘𝑂) =
(Id‘𝐶)) ↔ (𝑂 ∈ Cat ∧
(Id‘𝑂) = (𝑦 ∈ (Base‘𝐶) ↦ ((Id‘𝐶)‘𝑦))))) |
58 | 52, 57 | mpbird 246 |
1
⊢ (𝐶 ∈ Cat → (𝑂 ∈ Cat ∧
(Id‘𝑂) =
(Id‘𝐶))) |