| Step | Hyp | Ref
| Expression |
| 1 | | oppcbas.1 |
. . . . 5
⊢ 𝑂 = (oppCat‘𝐶) |
| 2 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 3 | 1, 2 | oppcbas 17761 |
. . . 4
⊢
(Base‘𝐶) =
(Base‘𝑂) |
| 4 | 3 | a1i 11 |
. . 3
⊢ (𝐶 ∈ Cat →
(Base‘𝐶) =
(Base‘𝑂)) |
| 5 | | eqidd 2738 |
. . 3
⊢ (𝐶 ∈ Cat → (Hom
‘𝑂) = (Hom
‘𝑂)) |
| 6 | | eqidd 2738 |
. . 3
⊢ (𝐶 ∈ Cat →
(comp‘𝑂) =
(comp‘𝑂)) |
| 7 | 1 | fvexi 6920 |
. . . 4
⊢ 𝑂 ∈ V |
| 8 | 7 | a1i 11 |
. . 3
⊢ (𝐶 ∈ Cat → 𝑂 ∈ V) |
| 9 | | biid 261 |
. . 3
⊢ (((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ↔ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) |
| 10 | | eqid 2737 |
. . . . 5
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 11 | | eqid 2737 |
. . . . 5
⊢
(Id‘𝐶) =
(Id‘𝐶) |
| 12 | | simpl 482 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ 𝑦 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat) |
| 13 | | simpr 484 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶)) |
| 14 | 2, 10, 11, 12, 13 | catidcl 17725 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ 𝑦 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑦) ∈ (𝑦(Hom ‘𝐶)𝑦)) |
| 15 | 10, 1 | oppchom 17758 |
. . . 4
⊢ (𝑦(Hom ‘𝑂)𝑦) = (𝑦(Hom ‘𝐶)𝑦) |
| 16 | 14, 15 | eleqtrrdi 2852 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ 𝑦 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑦) ∈ (𝑦(Hom ‘𝑂)𝑦)) |
| 17 | | eqid 2737 |
. . . . 5
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 18 | | simpr1l 1231 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑥 ∈ (Base‘𝐶)) |
| 19 | | simpr1r 1232 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑦 ∈ (Base‘𝐶)) |
| 20 | 2, 17, 1, 18, 19, 19 | oppcco 17760 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (((Id‘𝐶)‘𝑦)(〈𝑥, 𝑦〉(comp‘𝑂)𝑦)𝑓) = (𝑓(〈𝑦, 𝑦〉(comp‘𝐶)𝑥)((Id‘𝐶)‘𝑦))) |
| 21 | | simpl 482 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝐶 ∈ Cat) |
| 22 | | simpr31 1264 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦)) |
| 23 | 10, 1 | oppchom 17758 |
. . . . . 6
⊢ (𝑥(Hom ‘𝑂)𝑦) = (𝑦(Hom ‘𝐶)𝑥) |
| 24 | 22, 23 | eleqtrdi 2851 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) |
| 25 | 2, 10, 11, 21, 19, 17, 18, 24 | catrid 17727 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑓(〈𝑦, 𝑦〉(comp‘𝐶)𝑥)((Id‘𝐶)‘𝑦)) = 𝑓) |
| 26 | 20, 25 | eqtrd 2777 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (((Id‘𝐶)‘𝑦)(〈𝑥, 𝑦〉(comp‘𝑂)𝑦)𝑓) = 𝑓) |
| 27 | | simpr2l 1233 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑧 ∈ (Base‘𝐶)) |
| 28 | 2, 17, 1, 19, 19, 27 | oppcco 17760 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑔(〈𝑦, 𝑦〉(comp‘𝑂)𝑧)((Id‘𝐶)‘𝑦)) = (((Id‘𝐶)‘𝑦)(〈𝑧, 𝑦〉(comp‘𝐶)𝑦)𝑔)) |
| 29 | | simpr32 1265 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧)) |
| 30 | 10, 1 | oppchom 17758 |
. . . . . 6
⊢ (𝑦(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑦) |
| 31 | 29, 30 | eleqtrdi 2851 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑦)) |
| 32 | 2, 10, 11, 21, 27, 17, 19, 31 | catlid 17726 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (((Id‘𝐶)‘𝑦)(〈𝑧, 𝑦〉(comp‘𝐶)𝑦)𝑔) = 𝑔) |
| 33 | 28, 32 | eqtrd 2777 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑔(〈𝑦, 𝑦〉(comp‘𝑂)𝑧)((Id‘𝐶)‘𝑦)) = 𝑔) |
| 34 | 2, 17, 1, 18, 19, 27 | oppcco 17760 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓) = (𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔)) |
| 35 | 2, 10, 17, 21, 27, 19, 18, 31, 24 | catcocl 17728 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔) ∈ (𝑧(Hom ‘𝐶)𝑥)) |
| 36 | 34, 35 | eqeltrd 2841 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓) ∈ (𝑧(Hom ‘𝐶)𝑥)) |
| 37 | 10, 1 | oppchom 17758 |
. . . 4
⊢ (𝑥(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑥) |
| 38 | 36, 37 | eleqtrrdi 2852 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓) ∈ (𝑥(Hom ‘𝑂)𝑧)) |
| 39 | | simpr2r 1234 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑤 ∈ (Base‘𝐶)) |
| 40 | | simpr33 1266 |
. . . . . . 7
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)) |
| 41 | 10, 1 | oppchom 17758 |
. . . . . . 7
⊢ (𝑧(Hom ‘𝑂)𝑤) = (𝑤(Hom ‘𝐶)𝑧) |
| 42 | 40, 41 | eleqtrdi 2851 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ℎ ∈ (𝑤(Hom ‘𝐶)𝑧)) |
| 43 | 2, 10, 17, 21, 39, 27, 19, 42, 31, 18, 24 | catass 17729 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔)(〈𝑤, 𝑧〉(comp‘𝐶)𝑥)ℎ) = (𝑓(〈𝑤, 𝑦〉(comp‘𝐶)𝑥)(𝑔(〈𝑤, 𝑧〉(comp‘𝐶)𝑦)ℎ))) |
| 44 | 2, 17, 1, 18, 27, 39 | oppcco 17760 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (ℎ(〈𝑥, 𝑧〉(comp‘𝑂)𝑤)(𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔)) = ((𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔)(〈𝑤, 𝑧〉(comp‘𝐶)𝑥)ℎ)) |
| 45 | 2, 17, 1, 18, 19, 39 | oppcco 17760 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((𝑔(〈𝑤, 𝑧〉(comp‘𝐶)𝑦)ℎ)(〈𝑥, 𝑦〉(comp‘𝑂)𝑤)𝑓) = (𝑓(〈𝑤, 𝑦〉(comp‘𝐶)𝑥)(𝑔(〈𝑤, 𝑧〉(comp‘𝐶)𝑦)ℎ))) |
| 46 | 43, 44, 45 | 3eqtr4rd 2788 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((𝑔(〈𝑤, 𝑧〉(comp‘𝐶)𝑦)ℎ)(〈𝑥, 𝑦〉(comp‘𝑂)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝑂)𝑤)(𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔))) |
| 47 | 2, 17, 1, 19, 27, 39 | oppcco 17760 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (ℎ(〈𝑦, 𝑧〉(comp‘𝑂)𝑤)𝑔) = (𝑔(〈𝑤, 𝑧〉(comp‘𝐶)𝑦)ℎ)) |
| 48 | 47 | oveq1d 7446 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((ℎ(〈𝑦, 𝑧〉(comp‘𝑂)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝑂)𝑤)𝑓) = ((𝑔(〈𝑤, 𝑧〉(comp‘𝐶)𝑦)ℎ)(〈𝑥, 𝑦〉(comp‘𝑂)𝑤)𝑓)) |
| 49 | 34 | oveq2d 7447 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (ℎ(〈𝑥, 𝑧〉(comp‘𝑂)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓)) = (ℎ(〈𝑥, 𝑧〉(comp‘𝑂)𝑤)(𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔))) |
| 50 | 46, 48, 49 | 3eqtr4d 2787 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((ℎ(〈𝑦, 𝑧〉(comp‘𝑂)𝑤)𝑔)(〈𝑥, 𝑦〉(comp‘𝑂)𝑤)𝑓) = (ℎ(〈𝑥, 𝑧〉(comp‘𝑂)𝑤)(𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓))) |
| 51 | 4, 5, 6, 8, 9, 16,
26, 33, 38, 50 | iscatd2 17724 |
. 2
⊢ (𝐶 ∈ Cat → (𝑂 ∈ Cat ∧
(Id‘𝑂) = (𝑦 ∈ (Base‘𝐶) ↦ ((Id‘𝐶)‘𝑦)))) |
| 52 | 2, 11 | cidfn 17722 |
. . . . 5
⊢ (𝐶 ∈ Cat →
(Id‘𝐶) Fn
(Base‘𝐶)) |
| 53 | | dffn5 6967 |
. . . . 5
⊢
((Id‘𝐶) Fn
(Base‘𝐶) ↔
(Id‘𝐶) = (𝑦 ∈ (Base‘𝐶) ↦ ((Id‘𝐶)‘𝑦))) |
| 54 | 52, 53 | sylib 218 |
. . . 4
⊢ (𝐶 ∈ Cat →
(Id‘𝐶) = (𝑦 ∈ (Base‘𝐶) ↦ ((Id‘𝐶)‘𝑦))) |
| 55 | 54 | eqeq2d 2748 |
. . 3
⊢ (𝐶 ∈ Cat →
((Id‘𝑂) =
(Id‘𝐶) ↔
(Id‘𝑂) = (𝑦 ∈ (Base‘𝐶) ↦ ((Id‘𝐶)‘𝑦)))) |
| 56 | 55 | anbi2d 630 |
. 2
⊢ (𝐶 ∈ Cat → ((𝑂 ∈ Cat ∧
(Id‘𝑂) =
(Id‘𝐶)) ↔ (𝑂 ∈ Cat ∧
(Id‘𝑂) = (𝑦 ∈ (Base‘𝐶) ↦ ((Id‘𝐶)‘𝑦))))) |
| 57 | 51, 56 | mpbird 257 |
1
⊢ (𝐶 ∈ Cat → (𝑂 ∈ Cat ∧
(Id‘𝑂) =
(Id‘𝐶))) |