Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  oppccatid Structured version   Visualization version   GIF version

Theorem oppccatid 16303
 Description: Lemma for oppccat 16306. (Contributed by Mario Carneiro, 3-Jan-2017.)
Hypothesis
Ref Expression
oppcbas.1 𝑂 = (oppCat‘𝐶)
Assertion
Ref Expression
oppccatid (𝐶 ∈ Cat → (𝑂 ∈ Cat ∧ (Id‘𝑂) = (Id‘𝐶)))

Proof of Theorem oppccatid
Dummy variables 𝑓 𝑔 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oppcbas.1 . . . . 5 𝑂 = (oppCat‘𝐶)
2 eqid 2621 . . . . 5 (Base‘𝐶) = (Base‘𝐶)
31, 2oppcbas 16302 . . . 4 (Base‘𝐶) = (Base‘𝑂)
43a1i 11 . . 3 (𝐶 ∈ Cat → (Base‘𝐶) = (Base‘𝑂))
5 eqidd 2622 . . 3 (𝐶 ∈ Cat → (Hom ‘𝑂) = (Hom ‘𝑂))
6 eqidd 2622 . . 3 (𝐶 ∈ Cat → (comp‘𝑂) = (comp‘𝑂))
7 fvex 6160 . . . . 5 (oppCat‘𝐶) ∈ V
81, 7eqeltri 2694 . . . 4 𝑂 ∈ V
98a1i 11 . . 3 (𝐶 ∈ Cat → 𝑂 ∈ V)
10 biid 251 . . 3 (((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤))) ↔ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤))))
11 eqid 2621 . . . . 5 (Hom ‘𝐶) = (Hom ‘𝐶)
12 eqid 2621 . . . . 5 (Id‘𝐶) = (Id‘𝐶)
13 simpl 473 . . . . 5 ((𝐶 ∈ Cat ∧ 𝑦 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
14 simpr 477 . . . . 5 ((𝐶 ∈ Cat ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶))
152, 11, 12, 13, 14catidcl 16267 . . . 4 ((𝐶 ∈ Cat ∧ 𝑦 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑦) ∈ (𝑦(Hom ‘𝐶)𝑦))
1611, 1oppchom 16299 . . . 4 (𝑦(Hom ‘𝑂)𝑦) = (𝑦(Hom ‘𝐶)𝑦)
1715, 16syl6eleqr 2709 . . 3 ((𝐶 ∈ Cat ∧ 𝑦 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑦) ∈ (𝑦(Hom ‘𝑂)𝑦))
18 eqid 2621 . . . . 5 (comp‘𝐶) = (comp‘𝐶)
19 simpr1l 1116 . . . . 5 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑥 ∈ (Base‘𝐶))
20 simpr1r 1117 . . . . 5 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑦 ∈ (Base‘𝐶))
212, 18, 1, 19, 20, 20oppcco 16301 . . . 4 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (((Id‘𝐶)‘𝑦)(⟨𝑥, 𝑦⟩(comp‘𝑂)𝑦)𝑓) = (𝑓(⟨𝑦, 𝑦⟩(comp‘𝐶)𝑥)((Id‘𝐶)‘𝑦)))
22 simpl 473 . . . . 5 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝐶 ∈ Cat)
23 simpr31 1149 . . . . . 6 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦))
2411, 1oppchom 16299 . . . . . 6 (𝑥(Hom ‘𝑂)𝑦) = (𝑦(Hom ‘𝐶)𝑥)
2523, 24syl6eleq 2708 . . . . 5 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥))
262, 11, 12, 22, 20, 18, 19, 25catrid 16269 . . . 4 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑓(⟨𝑦, 𝑦⟩(comp‘𝐶)𝑥)((Id‘𝐶)‘𝑦)) = 𝑓)
2721, 26eqtrd 2655 . . 3 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (((Id‘𝐶)‘𝑦)(⟨𝑥, 𝑦⟩(comp‘𝑂)𝑦)𝑓) = 𝑓)
28 simpr2l 1118 . . . . 5 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑧 ∈ (Base‘𝐶))
292, 18, 1, 20, 20, 28oppcco 16301 . . . 4 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑔(⟨𝑦, 𝑦⟩(comp‘𝑂)𝑧)((Id‘𝐶)‘𝑦)) = (((Id‘𝐶)‘𝑦)(⟨𝑧, 𝑦⟩(comp‘𝐶)𝑦)𝑔))
30 simpr32 1150 . . . . . 6 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))
3111, 1oppchom 16299 . . . . . 6 (𝑦(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑦)
3230, 31syl6eleq 2708 . . . . 5 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑦))
332, 11, 12, 22, 28, 18, 20, 32catlid 16268 . . . 4 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (((Id‘𝐶)‘𝑦)(⟨𝑧, 𝑦⟩(comp‘𝐶)𝑦)𝑔) = 𝑔)
3429, 33eqtrd 2655 . . 3 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑔(⟨𝑦, 𝑦⟩(comp‘𝑂)𝑧)((Id‘𝐶)‘𝑦)) = 𝑔)
352, 18, 1, 19, 20, 28oppcco 16301 . . . . 5 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑂)𝑧)𝑓) = (𝑓(⟨𝑧, 𝑦⟩(comp‘𝐶)𝑥)𝑔))
362, 11, 18, 22, 28, 20, 19, 32, 25catcocl 16270 . . . . 5 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑓(⟨𝑧, 𝑦⟩(comp‘𝐶)𝑥)𝑔) ∈ (𝑧(Hom ‘𝐶)𝑥))
3735, 36eqeltrd 2698 . . . 4 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑂)𝑧)𝑓) ∈ (𝑧(Hom ‘𝐶)𝑥))
3811, 1oppchom 16299 . . . 4 (𝑥(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑥)
3937, 38syl6eleqr 2709 . . 3 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑂)𝑧)𝑓) ∈ (𝑥(Hom ‘𝑂)𝑧))
40 simpr2r 1119 . . . . . 6 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → 𝑤 ∈ (Base‘𝐶))
41 simpr33 1151 . . . . . . 7 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ∈ (𝑧(Hom ‘𝑂)𝑤))
4211, 1oppchom 16299 . . . . . . 7 (𝑧(Hom ‘𝑂)𝑤) = (𝑤(Hom ‘𝐶)𝑧)
4341, 42syl6eleq 2708 . . . . . 6 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ∈ (𝑤(Hom ‘𝐶)𝑧))
442, 11, 18, 22, 40, 28, 20, 43, 32, 19, 25catass 16271 . . . . 5 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((𝑓(⟨𝑧, 𝑦⟩(comp‘𝐶)𝑥)𝑔)(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑥)) = (𝑓(⟨𝑤, 𝑦⟩(comp‘𝐶)𝑥)(𝑔(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑦))))
452, 18, 1, 19, 28, 40oppcco 16301 . . . . 5 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((⟨𝑥, 𝑧⟩(comp‘𝑂)𝑤)(𝑓(⟨𝑧, 𝑦⟩(comp‘𝐶)𝑥)𝑔)) = ((𝑓(⟨𝑧, 𝑦⟩(comp‘𝐶)𝑥)𝑔)(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑥)))
462, 18, 1, 19, 20, 40oppcco 16301 . . . . 5 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((𝑔(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑦))(⟨𝑥, 𝑦⟩(comp‘𝑂)𝑤)𝑓) = (𝑓(⟨𝑤, 𝑦⟩(comp‘𝐶)𝑥)(𝑔(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑦))))
4744, 45, 463eqtr4rd 2666 . . . 4 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((𝑔(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑦))(⟨𝑥, 𝑦⟩(comp‘𝑂)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝑂)𝑤)(𝑓(⟨𝑧, 𝑦⟩(comp‘𝐶)𝑥)𝑔)))
482, 18, 1, 20, 28, 40oppcco 16301 . . . . 5 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((⟨𝑦, 𝑧⟩(comp‘𝑂)𝑤)𝑔) = (𝑔(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑦)))
4948oveq1d 6622 . . . 4 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (((⟨𝑦, 𝑧⟩(comp‘𝑂)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝑂)𝑤)𝑓) = ((𝑔(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑦))(⟨𝑥, 𝑦⟩(comp‘𝑂)𝑤)𝑓))
5035oveq2d 6623 . . . 4 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → ((⟨𝑥, 𝑧⟩(comp‘𝑂)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑂)𝑧)𝑓)) = ((⟨𝑥, 𝑧⟩(comp‘𝑂)𝑤)(𝑓(⟨𝑧, 𝑦⟩(comp‘𝐶)𝑥)𝑔)))
5147, 49, 503eqtr4d 2665 . . 3 ((𝐶 ∈ Cat ∧ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑧 ∈ (Base‘𝐶) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧) ∧ ∈ (𝑧(Hom ‘𝑂)𝑤)))) → (((⟨𝑦, 𝑧⟩(comp‘𝑂)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝑂)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝑂)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑂)𝑧)𝑓)))
524, 5, 6, 9, 10, 17, 27, 34, 39, 51iscatd2 16266 . 2 (𝐶 ∈ Cat → (𝑂 ∈ Cat ∧ (Id‘𝑂) = (𝑦 ∈ (Base‘𝐶) ↦ ((Id‘𝐶)‘𝑦))))
532, 12cidfn 16264 . . . . 5 (𝐶 ∈ Cat → (Id‘𝐶) Fn (Base‘𝐶))
54 dffn5 6200 . . . . 5 ((Id‘𝐶) Fn (Base‘𝐶) ↔ (Id‘𝐶) = (𝑦 ∈ (Base‘𝐶) ↦ ((Id‘𝐶)‘𝑦)))
5553, 54sylib 208 . . . 4 (𝐶 ∈ Cat → (Id‘𝐶) = (𝑦 ∈ (Base‘𝐶) ↦ ((Id‘𝐶)‘𝑦)))
5655eqeq2d 2631 . . 3 (𝐶 ∈ Cat → ((Id‘𝑂) = (Id‘𝐶) ↔ (Id‘𝑂) = (𝑦 ∈ (Base‘𝐶) ↦ ((Id‘𝐶)‘𝑦))))
5756anbi2d 739 . 2 (𝐶 ∈ Cat → ((𝑂 ∈ Cat ∧ (Id‘𝑂) = (Id‘𝐶)) ↔ (𝑂 ∈ Cat ∧ (Id‘𝑂) = (𝑦 ∈ (Base‘𝐶) ↦ ((Id‘𝐶)‘𝑦)))))
5852, 57mpbird 247 1 (𝐶 ∈ Cat → (𝑂 ∈ Cat ∧ (Id‘𝑂) = (Id‘𝐶)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987  Vcvv 3186  ⟨cop 4156   ↦ cmpt 4675   Fn wfn 5844  ‘cfv 5849  (class class class)co 6607  Basecbs 15784  Hom chom 15876  compcco 15877  Catccat 16249  Idccid 16250  oppCatcoppc 16295 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-1st 7116  df-2nd 7117  df-tpos 7300  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-er 7690  df-en 7903  df-dom 7904  df-sdom 7905  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-nn 10968  df-2 11026  df-3 11027  df-4 11028  df-5 11029  df-6 11030  df-7 11031  df-8 11032  df-9 11033  df-n0 11240  df-z 11325  df-dec 11441  df-ndx 15787  df-slot 15788  df-base 15789  df-sets 15790  df-hom 15890  df-cco 15891  df-cat 16253  df-cid 16254  df-oppc 16296 This theorem is referenced by:  oppcid  16305  oppccat  16306
 Copyright terms: Public domain W3C validator