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

Theorem catpropd 16575
Description: Two structures with the same base, hom-sets and composition operation are either both categories or neither. (Contributed by Mario Carneiro, 5-Jan-2017.)
Hypotheses
Ref Expression
catpropd.1 (𝜑 → (Homf𝐶) = (Homf𝐷))
catpropd.2 (𝜑 → (compf𝐶) = (compf𝐷))
catpropd.3 (𝜑𝐶𝑉)
catpropd.4 (𝜑𝐷𝑊)
Assertion
Ref Expression
catpropd (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))

Proof of Theorem catpropd
Dummy variables 𝑓 𝑔 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 468 . . . . . . . . 9 (((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
212ralimi 3101 . . . . . . . 8 (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
322ralimi 3101 . . . . . . 7 (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
43adantl 467 . . . . . 6 ((∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
54ralimi 3100 . . . . 5 (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
65a1i 11 . . . 4 (𝜑 → (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)))
7 simpl 468 . . . . . . . . 9 (((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
872ralimi 3101 . . . . . . . 8 (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
982ralimi 3101 . . . . . . 7 (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
109adantl 467 . . . . . 6 ((∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
1110ralimi 3100 . . . . 5 (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
1211a1i 11 . . . 4 (𝜑 → (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)))
13 nfra1 3089 . . . . . . . 8 𝑦𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)
14 nfv 1994 . . . . . . . 8 𝑥𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)
15 nfra1 3089 . . . . . . . . . 10 𝑧𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)
16 nfv 1994 . . . . . . . . . 10 𝑦𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)
17 nfra1 3089 . . . . . . . . . . . . . 14 𝑔𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)
18 nfv 1994 . . . . . . . . . . . . . 14 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧)((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)
19 oveq1 6799 . . . . . . . . . . . . . . . . 17 (𝑔 = → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = ((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))
2019eleq1d 2834 . . . . . . . . . . . . . . . 16 (𝑔 = → ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)))
2120cbvralv 3319 . . . . . . . . . . . . . . 15 (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ ∈ (𝑦(Hom ‘𝐶)𝑧)((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
22 oveq2 6800 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑔 → ((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = ((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔))
2322eleq1d 2834 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔 → (((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)))
2423ralbidv 3134 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (∀ ∈ (𝑦(Hom ‘𝐶)𝑧)((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ ∈ (𝑦(Hom ‘𝐶)𝑧)((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)))
2521, 24syl5bb 272 . . . . . . . . . . . . . 14 (𝑓 = 𝑔 → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ ∈ (𝑦(Hom ‘𝐶)𝑧)((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)))
2617, 18, 25cbvral 3315 . . . . . . . . . . . . 13 (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ ∈ (𝑦(Hom ‘𝐶)𝑧)((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧))
27 oveq2 6800 . . . . . . . . . . . . . . 15 (𝑧 = 𝑤 → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐶)𝑤))
28 oveq2 6800 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧) = (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤))
2928oveqd 6809 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → ((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) = ((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔))
30 oveq2 6800 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑤 → (𝑥(Hom ‘𝐶)𝑧) = (𝑥(Hom ‘𝐶)𝑤))
3129, 30eleq12d 2843 . . . . . . . . . . . . . . 15 (𝑧 = 𝑤 → (((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
3227, 31raleqbidv 3300 . . . . . . . . . . . . . 14 (𝑧 = 𝑤 → (∀ ∈ (𝑦(Hom ‘𝐶)𝑧)((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ ∈ (𝑦(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
3332ralbidv 3134 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → (∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ ∈ (𝑦(Hom ‘𝐶)𝑧)((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ ∈ (𝑦(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
3426, 33syl5bb 272 . . . . . . . . . . . 12 (𝑧 = 𝑤 → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ ∈ (𝑦(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
3534cbvralv 3319 . . . . . . . . . . 11 (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ ∈ (𝑦(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))
36 oveq2 6800 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐶)𝑧))
37 oveq1 6799 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (𝑦(Hom ‘𝐶)𝑤) = (𝑧(Hom ‘𝐶)𝑤))
38 opeq2 4538 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑧 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩)
3938oveq1d 6807 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤) = (⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤))
4039oveqd 6809 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 → ((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔))
4140eleq1d 2834 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
4237, 41raleqbidv 3300 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → (∀ ∈ (𝑦(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
4336, 42raleqbidv 3300 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ ∈ (𝑦(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
4443ralbidv 3134 . . . . . . . . . . 11 (𝑦 = 𝑧 → (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ ∈ (𝑦(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
4535, 44syl5bb 272 . . . . . . . . . 10 (𝑦 = 𝑧 → (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
4615, 16, 45cbvral 3315 . . . . . . . . 9 (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))
47 oveq1 6799 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐶)𝑧))
48 opeq1 4537 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ⟨𝑥, 𝑧⟩ = ⟨𝑦, 𝑧⟩)
4948oveq1d 6807 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤) = (⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤))
5049oveqd 6809 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) = ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔))
51 oveq1 6799 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝑥(Hom ‘𝐶)𝑤) = (𝑦(Hom ‘𝐶)𝑤))
5250, 51eleq12d 2843 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
5352ralbidv 3134 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
5447, 53raleqbidv 3300 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
5554ralbidv 3134 . . . . . . . . . . 11 (𝑥 = 𝑦 → (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
56 ralcom 3245 . . . . . . . . . . 11 (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))
5755, 56syl6bb 276 . . . . . . . . . 10 (𝑥 = 𝑦 → (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
5857ralbidv 3134 . . . . . . . . 9 (𝑥 = 𝑦 → (∀𝑧 ∈ (Base‘𝐶)∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
5946, 58syl5bb 272 . . . . . . . 8 (𝑥 = 𝑦 → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
6013, 14, 59cbvral 3315 . . . . . . 7 (∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))
6160biimpi 206 . . . . . 6 (∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))
6261ancri 531 . . . . 5 (∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)))
63 r19.26 3211 . . . . . . . . . . . 12 (∀𝑦 ∈ (Base‘𝐶)(∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ↔ (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)))
64 r19.26 3211 . . . . . . . . . . . . . . 15 (∀𝑧 ∈ (Base‘𝐶)(∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ↔ (∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)))
65 r19.26 3211 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ↔ (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)))
66 eqid 2770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (Base‘𝐶) = (Base‘𝐶)
67 eqid 2770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (Hom ‘𝐶) = (Hom ‘𝐶)
68 eqid 2770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (comp‘𝐶) = (comp‘𝐶)
69 eqid 2770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (comp‘𝐷) = (comp‘𝐷)
70 catpropd.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (Homf𝐶) = (Homf𝐷))
7170adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑥 ∈ (Base‘𝐶)) → (Homf𝐶) = (Homf𝐷))
7271ad4antr 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (Homf𝐶) = (Homf𝐷))
7372ad4antr 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (Homf𝐶) = (Homf𝐷))
74 catpropd.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (compf𝐶) = (compf𝐷))
7574ad5antr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (compf𝐶) = (compf𝐷))
7675ad4antr 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (compf𝐶) = (compf𝐷))
77 simpllr 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
7877ad2antrr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑥 ∈ (Base‘𝐶))
7978ad4antr 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑥 ∈ (Base‘𝐶))
80 simp-4r 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑦 ∈ (Base‘𝐶))
8180ad4antr 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑦 ∈ (Base‘𝐶))
82 simpllr 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑤 ∈ (Base‘𝐶))
83 simplr 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
8483ad4antr 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
85 simpr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))
8666, 67, 68, 69, 73, 76, 79, 81, 82, 84, 85comfeqval 16574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓))
87 simpllr 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑧 ∈ (Base‘𝐶))
8887ad4antr 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑧 ∈ (Base‘𝐶))
89 simp-4r 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
90 simplr 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → ∈ (𝑧(Hom ‘𝐶)𝑤))
9166, 67, 68, 69, 73, 76, 79, 88, 82, 89, 90comfeqval 16574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
9286, 91eqeq12d 2785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → ((((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ (((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
9392ex 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → ((((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ (((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
9493ralimdva 3110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → ∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ (((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
95 ralbi 3215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ (((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → (∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
9694, 95syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → (∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
9796ralimdva 3110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → ∀𝑤 ∈ (Base‘𝐶)(∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
9897impancom 439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ∀𝑤 ∈ (Base‘𝐶)(∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
9998impr 442 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) → ∀𝑤 ∈ (Base‘𝐶)(∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
100 ralbi 3215 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (∀𝑤 ∈ (Base‘𝐶)(∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → (∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
10199, 100syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) → (∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
102101anbi2d 606 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) → (((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
103102ex 397 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → ((∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
104103ralimdva 3110 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
10565, 104syl5bir 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
106105expdimp 440 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
107 ralbi 3215 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
108106, 107syl6 35 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
109108an32s 623 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
110109ralimdva 3110 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
111 ralbi 3215 . . . . . . . . . . . . . . . . . . 19 (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
112110, 111syl6 35 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
113112expimpd 441 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → ((∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
114113ralimdva 3110 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑧 ∈ (Base‘𝐶)(∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → ∀𝑧 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
115 ralbi 3215 . . . . . . . . . . . . . . . 16 (∀𝑧 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) → (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
116114, 115syl6 35 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑧 ∈ (Base‘𝐶)(∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
11764, 116syl5bir 233 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → ((∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
118117ralimdva 3110 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (Base‘𝐶)) → (∀𝑦 ∈ (Base‘𝐶)(∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → ∀𝑦 ∈ (Base‘𝐶)(∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
119 ralbi 3215 . . . . . . . . . . . . 13 (∀𝑦 ∈ (Base‘𝐶)(∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
120118, 119syl6 35 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (Base‘𝐶)) → (∀𝑦 ∈ (Base‘𝐶)(∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
12163, 120syl5bir 233 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
122121imp 393 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
123122an4s 631 . . . . . . . . 9 (((𝜑 ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) ∧ (𝑥 ∈ (Base‘𝐶) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
124123anbi2d 606 . . . . . . . 8 (((𝜑 ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) ∧ (𝑥 ∈ (Base‘𝐶) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) → ((∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
125124expr 444 . . . . . . 7 (((𝜑 ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) ∧ 𝑥 ∈ (Base‘𝐶)) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ((∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))))
126125ralimdva 3110 . . . . . 6 ((𝜑 ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ∀𝑥 ∈ (Base‘𝐶)((∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))))
127126expimpd 441 . . . . 5 (𝜑 → ((∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → ∀𝑥 ∈ (Base‘𝐶)((∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))))
128 ralbi 3215 . . . . 5 (∀𝑥 ∈ (Base‘𝐶)((∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))) → (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
12962, 127, 128syl56 36 . . . 4 (𝜑 → (∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))))
1306, 12, 129pm5.21ndd 368 . . 3 (𝜑 → (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
13170homfeqbas 16562 . . . 4 (𝜑 → (Base‘𝐶) = (Base‘𝐷))
132 eqid 2770 . . . . . . 7 (Hom ‘𝐷) = (Hom ‘𝐷)
133 simpr 471 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
13466, 67, 132, 71, 133, 133homfeqval 16563 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑥) = (𝑥(Hom ‘𝐷)𝑥))
135131ad2antrr 697 . . . . . . 7 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) → (Base‘𝐶) = (Base‘𝐷))
13671ad2antrr 697 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (Homf𝐶) = (Homf𝐷))
137 simpr 471 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶))
138 simpllr 752 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
13966, 67, 132, 136, 137, 138homfeqval 16563 . . . . . . . . 9 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐷)𝑥))
14070ad4antr 704 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (Homf𝐶) = (Homf𝐷))
14174ad4antr 704 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (compf𝐶) = (compf𝐷))
142 simplr 744 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑦 ∈ (Base‘𝐶))
143 simp-4r 762 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑥 ∈ (Base‘𝐶))
144 simpr 471 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥))
145 simpllr 752 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥))
14666, 67, 68, 69, 140, 141, 142, 143, 143, 144, 145comfeqval 16574 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓))
147146eqeq1d 2772 . . . . . . . . 9 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → ((𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ↔ (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓))
148139, 147raleqbidva 3302 . . . . . . . 8 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓))
14966, 67, 132, 136, 138, 137homfeqval 16563 . . . . . . . . 9 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐷)𝑦))
15070ad4antr 704 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Homf𝐶) = (Homf𝐷))
15174ad4antr 704 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (compf𝐶) = (compf𝐷))
152 simp-4r 762 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑥 ∈ (Base‘𝐶))
153 simplr 744 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑦 ∈ (Base‘𝐶))
154 simpllr 752 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥))
155 simpr 471 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
15666, 67, 68, 69, 150, 151, 152, 152, 153, 154, 155comfeqval 16574 . . . . . . . . . 10 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔))
157156eqeq1d 2772 . . . . . . . . 9 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓 ↔ (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓))
158149, 157raleqbidva 3302 . . . . . . . 8 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓))
159148, 158anbi12d 608 . . . . . . 7 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → ((∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
160135, 159raleqbidva 3302 . . . . . 6 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) → (∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
161134, 160rexeqbidva 3303 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐶)) → (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ ∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
162131adantr 466 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐷))
163162adantr 466 . . . . . . 7 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐷))
16471ad2antrr 697 . . . . . . . . 9 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (Homf𝐶) = (Homf𝐷))
165 simplr 744 . . . . . . . . 9 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶))
16666, 67, 132, 164, 77, 165homfeqval 16563 . . . . . . . 8 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐷)𝑦))
167 simpr 471 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑧 ∈ (Base‘𝐶))
16866, 67, 132, 164, 165, 167homfeqval 16563 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐷)𝑧))
169168adantr 466 . . . . . . . . 9 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐷)𝑧))
170 simpr 471 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
17166, 67, 68, 69, 72, 75, 78, 80, 87, 83, 170comfeqval 16574 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))
17266, 67, 132, 164, 77, 167homfeqval 16563 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑧) = (𝑥(Hom ‘𝐷)𝑧))
173172ad2antrr 697 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (𝑥(Hom ‘𝐶)𝑧) = (𝑥(Hom ‘𝐷)𝑧))
174171, 173eleq12d 2843 . . . . . . . . . 10 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧)))
175162ad4antr 704 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (Base‘𝐶) = (Base‘𝐷))
17672adantr 466 . . . . . . . . . . . . 13 (((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (Homf𝐶) = (Homf𝐷))
177 simp-4r 762 . . . . . . . . . . . . 13 (((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → 𝑧 ∈ (Base‘𝐶))
178 simpr 471 . . . . . . . . . . . . 13 (((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → 𝑤 ∈ (Base‘𝐶))
17966, 67, 132, 176, 177, 178homfeqval 16563 . . . . . . . . . . . 12 (((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (𝑧(Hom ‘𝐶)𝑤) = (𝑧(Hom ‘𝐷)𝑤))
180164ad4antr 704 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (Homf𝐶) = (Homf𝐷))
18174ad7antr 716 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (compf𝐶) = (compf𝐷))
182165ad4antr 704 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑦 ∈ (Base‘𝐶))
183167ad4antr 704 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧 ∈ (Base‘𝐶))
184 simplr 744 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤 ∈ (Base‘𝐶))
185 simpllr 752 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
186 simpr 471 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ∈ (𝑧(Hom ‘𝐶)𝑤))
18766, 67, 68, 69, 180, 181, 182, 183, 184, 185, 186comfeqval 16574 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) = ((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔))
188187oveq1d 6807 . . . . . . . . . . . . 13 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓))
18977ad4antr 704 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑥 ∈ (Base‘𝐶))
190 simp-4r 762 . . . . . . . . . . . . . . 15 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
19166, 67, 68, 69, 180, 181, 189, 182, 183, 190, 185comfeqval 16574 . . . . . . . . . . . . . 14 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))
192191oveq2d 6808 . . . . . . . . . . . . 13 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓)))
193188, 192eqeq12d 2785 . . . . . . . . . . . 12 ((((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ (((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))
194179, 193raleqbidva 3302 . . . . . . . . . . 11 (((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ ∈ (𝑧(Hom ‘𝐷)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))
195175, 194raleqbidva 3302 . . . . . . . . . 10 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀𝑤 ∈ (Base‘𝐷)∀ ∈ (𝑧(Hom ‘𝐷)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))
196174, 195anbi12d 608 . . . . . . . . 9 ((((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ ∈ (𝑧(Hom ‘𝐷)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓)))))
197169, 196raleqbidva 3302 . . . . . . . 8 (((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ ∈ (𝑧(Hom ‘𝐷)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓)))))
198166, 197raleqbidva 3302 . . . . . . 7 ((((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ ∈ (𝑧(Hom ‘𝐷)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓)))))
199163, 198raleqbidva 3302 . . . . . 6 (((𝜑𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ ∈ (𝑧(Hom ‘𝐷)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓)))))
200162, 199raleqbidva 3302 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐶)) → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑦 ∈ (Base‘𝐷)∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ ∈ (𝑧(Hom ‘𝐷)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓)))))
201161, 200anbi12d 608 . . . 4 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐷)∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ ∈ (𝑧(Hom ‘𝐷)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))))
202131, 201raleqbidva 3302 . . 3 (𝜑 → (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) ↔ ∀𝑥 ∈ (Base‘𝐷)(∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐷)∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ ∈ (𝑧(Hom ‘𝐷)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))))
203130, 202bitrd 268 . 2 (𝜑 → (∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))) ↔ ∀𝑥 ∈ (Base‘𝐷)(∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐷)∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ ∈ (𝑧(Hom ‘𝐷)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))))
204 catpropd.3 . . 3 (𝜑𝐶𝑉)
20566, 67, 68iscat 16539 . . 3 (𝐶𝑉 → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
206204, 205syl 17 . 2 (𝜑 → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ ∈ (𝑧(Hom ‘𝐶)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
207 catpropd.4 . . 3 (𝜑𝐷𝑊)
208 eqid 2770 . . . 4 (Base‘𝐷) = (Base‘𝐷)
209208, 132, 69iscat 16539 . . 3 (𝐷𝑊 → (𝐷 ∈ Cat ↔ ∀𝑥 ∈ (Base‘𝐷)(∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐷)∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ ∈ (𝑧(Hom ‘𝐷)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))))
210207, 209syl 17 . 2 (𝜑 → (𝐷 ∈ Cat ↔ ∀𝑥 ∈ (Base‘𝐷)(∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐷)∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ ∈ (𝑧(Hom ‘𝐷)𝑤)(((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))))
211203, 206, 2103bitr4d 300 1 (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1630  wcel 2144  wral 3060  wrex 3061  cop 4320  cfv 6031  (class class class)co 6792  Basecbs 16063  Hom chom 16159  compcco 16160  Catccat 16531  Homf chomf 16533  compfccomf 16534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-rep 4902  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-reu 3067  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-iun 4654  df-br 4785  df-opab 4845  df-mpt 4862  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-1st 7314  df-2nd 7315  df-cat 16535  df-homf 16537  df-comf 16538
This theorem is referenced by:  cidpropd  16576  resscat  16718  funcpropd  16766
  Copyright terms: Public domain W3C validator