catpropd - Metamath Proof Explorer

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

Theorem catpropd 17876

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	⊢ (𝜑 → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
catpropd.2	⊢ (𝜑 → (comp_f‘𝐶) = (comp_f‘𝐷))
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.

Step	Hyp	Ref	Expression
1		simpl 488	. . . . . . . . 9 ⊢ (((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
2	1	2ralimi 3133	. . . . . . . 8 ⊢ (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
3	2	2ralimi 3133	. . . . . . 7 ⊢ (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
4	3	adantl 487	. . . . . 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 ‘𝐶)𝑧))
5	4	ralimi 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 ‘𝐶)𝑧))
6	5	a1i 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 488	. . . . . . . . 9 ⊢ (((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
8	7	2ralimi 3133	. . . . . . . 8 ⊢ (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
9	8	2ralimi 3133	. . . . . . 7 ⊢ (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
10	9	adantl 487	. . . . . 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 ‘𝐶)𝑧))
11	10	ralimi 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 ‘𝐶)𝑧))
12	11	a1i 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 3287	. . . . . . . 8 ⊢ Ⅎ𝑦∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)
14		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)
15		nfra1 3287	. . . . . . . . . 10 ⊢ Ⅎ𝑧∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)
16		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑦∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)
17		nfra1 3287	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)
18		nfv 1947	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)
19		oveq1 7425	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = ℎ → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))
20	19	eleq1d 2846	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = ℎ → ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)))
21	20	cbvralvw 3241	. . . . . . . . . . . . . . 15 ⊢ (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
22		oveq2 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔))
23	22	eleq1d 2846	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)))
24	23	ralbidv 3186	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)))
25	21, 24	bitrid 286	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)))
26	17, 18, 25	cbvralw 3305	. . . . . . . . . . . . 13 ⊢ (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧))
27		oveq2 7426	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑤 → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐶)𝑤))
28		oveq2 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑤 → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧) = (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤))
29	28	oveqd 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) = (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔))
30		oveq2 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → (𝑥(Hom ‘𝐶)𝑧) = (𝑥(Hom ‘𝐶)𝑤))
31	29, 30	eleq12d 2855	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑤 → ((ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
32	27, 31	raleqbidv 3335	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑤 → (∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
33	32	ralbidv 3186	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
34	26, 33	bitrid 286	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
35	34	cbvralvw 3241	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))
36		oveq2 7426	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐶)𝑧))
37		oveq1 7425	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (𝑦(Hom ‘𝐶)𝑤) = (𝑧(Hom ‘𝐶)𝑤))
38		opeq2 4834	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑧 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩)
39	38	oveq1d 7433	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤) = (⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤))
40	39	oveqd 7435	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔))
41	40	eleq1d 2846	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → ((ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
42	37, 41	raleqbidv 3335	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
43	36, 42	raleqbidv 3335	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
44	43	ralbidv 3186	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
45	35, 44	bitrid 286	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
46	15, 16, 45	cbvralw 3305	. . . . . . . . 9 ⊢ (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))
47		oveq1 7425	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐶)𝑧))
48		opeq1 4833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑧⟩ = ⟨𝑦, 𝑧⟩)
49	48	oveq1d 7433	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤) = (⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤))
50	49	oveqd 7435	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) = (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔))
51		oveq1 7425	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑥(Hom ‘𝐶)𝑤) = (𝑦(Hom ‘𝐶)𝑤))
52	50, 51	eleq12d 2855	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
53	52	ralbidv 3186	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
54	47, 53	raleqbidv 3335	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
55	54	ralbidv 3186	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
56		ralcom 3291	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))
57	55, 56	bitrdi 290	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
58	57	ralbidv 3186	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (Base‘𝐶)∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
59	46, 58	bitrid 286	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
60	13, 14, 59	cbvralw 3305	. . . . . . 7 ⊢ (∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))
61	60	biimpi 219	. . . . . 6 ⊢ (∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))
62	61	ancri 559	. . . . 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 3123	. . . . . . . . . . . 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 3123	. . . . . . . . . . . . . . 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 3123	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ↔ (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)))
66		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (Base‘𝐶) = (Base‘𝐶)
67		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
68		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (comp‘𝐶) = (comp‘𝐶)
69		eqid 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (comp‘𝐷) = (comp‘𝐷)
70		catpropd.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
71	70	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
72	71	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
73	72	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
74		catpropd.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (comp_f‘𝐶) = (comp_f‘𝐷))
75	74	ad5antr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (comp_f‘𝐶) = (comp_f‘𝐷))
76	75	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (comp_f‘𝐶) = (comp_f‘𝐷))
77		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
78	77	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑥 ∈ (Base‘𝐶))
79	78	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑥 ∈ (Base‘𝐶))
80		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑦 ∈ (Base‘𝐶))
81	80	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑦 ∈ (Base‘𝐶))
82		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑤 ∈ (Base‘𝐶))
83		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
84	83	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
85		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))
86	66, 67, 68, 69, 73, 76, 79, 81, 82, 84, 85	comfeqval 17875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓))
87		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑧 ∈ (Base‘𝐶))
88	87	ad4antr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑧 ∈ (Base‘𝐶))
89		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
90		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → ℎ ∈ (𝑧(Hom ‘𝐶)𝑤))
91	66, 67, 68, 69, 73, 76, 79, 88, 82, 89, 90	comfeqval 17875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
92	86, 91	eqeq12d 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
93	92	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → (((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
94	93	ralimdva 3175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
95		ralbi 3118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
96	94, 95	syl6 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
97	96	ralimdva 3175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → ∀𝑤 ∈ (Base‘𝐶)(∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
98	97	impancom 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ∀𝑤 ∈ (Base‘𝐶)(∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
99	98	impr 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3118	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑤 ∈ (Base‘𝐶)(∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → (∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
101	99, 100	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))) → (∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
102	101	anbi2d 642	. . . . . . . . . . . . . . . . . . . . . . . . . 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‘𝐶)𝑧)𝑓)))))
103	102	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . 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‘𝐶)𝑧)𝑓))))))
104	103	ralimdva 3175	. . . . . . . . . . . . . . . . . . . . . . . 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‘𝐶)𝑧)𝑓))))))
105	65, 104	biimtrrid 246	. . . . . . . . . . . . . . . . . . . . . . 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‘𝐶)𝑧)𝑓))))))
106	105	expdimp 458	. . . . . . . . . . . . . . . . . . . . . 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 3118	. . . . . . . . . . . . . . . . . . . . . 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‘𝐶)𝑧)𝑓)))))
108	106, 107	syl6 36	. . . . . . . . . . . . . . . . . . . . 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‘𝐶)𝑧)𝑓))))))
109	108	an32s 665	. . . . . . . . . . . . . . . . . . . 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‘𝐶)𝑧)𝑓))))))
110	109	ralimdva 3175	. . . . . . . . . . . . . . . . . . 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 3118	. . . . . . . . . . . . . . . . . . 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‘𝐶)𝑧)𝑓)))))
112	110, 111	syl6 36	. . . . . . . . . . . . . . . . . 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‘𝐶)𝑧)𝑓))))))
113	112	expimpd 459	. . . . . . . . . . . . . . . . 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‘𝐶)𝑧)𝑓))))))
114	113	ralimdva 3175	. . . . . . . . . . . . . . . 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 3118	. . . . . . . . . . . . . . . 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‘𝐶)𝑧)𝑓)))))
116	114, 115	syl6 36	. . . . . . . . . . . . . . 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‘𝐶)𝑧)𝑓))))))
117	64, 116	biimtrrid 246	. . . . . . . . . . . . . 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‘𝐶)𝑧)𝑓))))))
118	117	ralimdva 3175	. . . . . . . . . . . . 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 3118	. . . . . . . . . . . . 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‘𝐶)𝑧)𝑓)))))
120	118, 119	syl6 36	. . . . . . . . . . . 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‘𝐶)𝑧)𝑓))))))
121	63, 120	biimtrrid 246	. . . . . . . . . . 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‘𝐶)𝑧)𝑓))))))
122	121	imp 412	. . . . . . . . . 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‘𝐶)𝑧)𝑓)))))
123	122	an4s 673	. . . . . . . . 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‘𝐶)𝑧)𝑓)))))
124	123	anbi2d 642	. . . . . . . 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‘𝐶)𝑧)𝑓))))))
125	124	expr 462	. . . . . . 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‘𝐶)𝑧)𝑓)))))))
126	125	ralimdva 3175	. . . . . 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‘𝐶)𝑧)𝑓)))))))
127	126	expimpd 459	. . . . 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 3118	. . . . 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‘𝐶)𝑧)𝑓))))))
129	62, 127, 128	syl56 37	. . . 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‘𝐶)𝑧)𝑓)))))))
130	6, 12, 129	pm5.21ndd 382	. . 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‘𝐶)𝑧)𝑓))))))
131	70	homfeqbas 17863	. . . 4 ⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷))
132		eqid 2761	. . . . . . 7 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
133		simpr 490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
134	66, 67, 132, 71, 133, 133	homfeqval 17864	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑥) = (𝑥(Hom ‘𝐷)𝑥))
135	131	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) → (Base‘𝐶) = (Base‘𝐷))
136	71	ad2antrr 739	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
137		simpr 490	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶))
138		simpllr 788	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
139	66, 67, 132, 136, 137, 138	homfeqval 17864	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐷)𝑥))
140	70	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
141	74	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (comp_f‘𝐶) = (comp_f‘𝐷))
142		simplr 781	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑦 ∈ (Base‘𝐶))
143		simp-4r 796	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑥 ∈ (Base‘𝐶))
144		simpr 490	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥))
145		simpllr 788	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥))
146	66, 67, 68, 69, 140, 141, 142, 143, 143, 144, 145	comfeqval 17875	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓))
147	146	eqeq1d 2763	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → ((𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ↔ (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓))
148	139, 147	raleqbidva 3326	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓))
149	66, 67, 132, 136, 138, 137	homfeqval 17864	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐷)𝑦))
150	70	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
151	74	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (comp_f‘𝐶) = (comp_f‘𝐷))
152		simp-4r 796	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑥 ∈ (Base‘𝐶))
153		simplr 781	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑦 ∈ (Base‘𝐶))
154		simpllr 788	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥))
155		simpr 490	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
156	66, 67, 68, 69, 150, 151, 152, 152, 153, 154, 155	comfeqval 17875	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔))
157	156	eqeq1d 2763	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓 ↔ (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓))
158	149, 157	raleqbidva 3326	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓))
159	148, 158	anbi12d 644	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → ((∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
160	135, 159	raleqbidva 3326	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) → (∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
161	134, 160	rexeqbidva 3327	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ ∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
162	131	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐷))
163	162	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐷))
164	71	ad2antrr 739	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
165		simplr 781	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶))
166	66, 67, 132, 164, 77, 165	homfeqval 17864	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐷)𝑦))
167		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑧 ∈ (Base‘𝐶))
168	66, 67, 132, 164, 165, 167	homfeqval 17864	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐷)𝑧))
169	168	adantr 486	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐷)𝑧))
170		simpr 490	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
171	66, 67, 68, 69, 72, 75, 78, 80, 87, 83, 170	comfeqval 17875	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))
172	66, 67, 132, 164, 77, 167	homfeqval 17864	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑧) = (𝑥(Hom ‘𝐷)𝑧))
173	172	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (𝑥(Hom ‘𝐶)𝑧) = (𝑥(Hom ‘𝐷)𝑧))
174	171, 173	eleq12d 2855	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧)))
175	162	ad4antr 745	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (Base‘𝐶) = (Base‘𝐷))
176	72	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
177		simp-4r 796	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → 𝑧 ∈ (Base‘𝐶))
178		simpr 490	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → 𝑤 ∈ (Base‘𝐶))
179	66, 67, 132, 176, 177, 178	homfeqval 17864	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (𝑧(Hom ‘𝐶)𝑤) = (𝑧(Hom ‘𝐷)𝑤))
180	164	ad4antr 745	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
181	74	ad7antr 751	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (comp_f‘𝐶) = (comp_f‘𝐷))
182	165	ad4antr 745	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑦 ∈ (Base‘𝐶))
183	167	ad4antr 745	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧 ∈ (Base‘𝐶))
184		simplr 781	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤 ∈ (Base‘𝐶))
185		simpllr 788	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
186		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ℎ ∈ (𝑧(Hom ‘𝐶)𝑤))
187	66, 67, 68, 69, 180, 181, 182, 183, 184, 185, 186	comfeqval 17875	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) = (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔))
188	187	oveq1d 7433	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓))
189	77	ad4antr 745	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑥 ∈ (Base‘𝐶))
190		simp-4r 796	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
191	66, 67, 68, 69, 180, 181, 189, 182, 183, 190, 185	comfeqval 17875	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))
192	191	oveq2d 7434	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓)))
193	188, 192	eqeq12d 2777	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))
194	179, 193	raleqbidva 3326	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))
195	175, 194	raleqbidva 3326	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))
196	174, 195	anbi12d 644	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓)))))
197	169, 196	raleqbidva 3326	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓)))))
198	166, 197	raleqbidva 3326	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓)))))
199	163, 198	raleqbidva 3326	. . . . . 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‘𝐷)𝑧)𝑓)))))
200	162, 199	raleqbidva 3326	. . . . 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‘𝐷)𝑧)𝑓)))))
201	161, 200	anbi12d 644	. . . 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‘𝐷)𝑧)𝑓))))))
202	131, 201	raleqbidva 3326	. . 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‘𝐷)𝑧)𝑓))))))
203	130, 202	bitrd 282	. 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 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
205	66, 67, 68	iscat 17839	. . 3 ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ Cat ↔ ∀𝑥 ∈ (Base‘𝐶)(∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))))
206	204, 205	syl 18	. 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 2761	. . . 4 ⊢ (Base‘𝐷) = (Base‘𝐷)
209	208, 132, 69	iscat 17839	. . 3 ⊢ (𝐷 ∈ 𝑊 → (𝐷 ∈ Cat ↔ ∀𝑥 ∈ (Base‘𝐷)(∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐷)∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))))
210	207, 209	syl 18	. 2 ⊢ (𝜑 → (𝐷 ∈ Cat ↔ ∀𝑥 ∈ (Base‘𝐷)(∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ (Base‘𝐷)∀𝑧 ∈ (Base‘𝐷)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))))
211	203, 206, 210	3bitr4d 314	1 ⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∀wral 3077 ∃wrex 3087 ⟨cop 4590 ‘cfv 6537 (class class class)co 7418 Basecbs 17380 Hom chom 17432 compcco 17433 Catccat 17831 Hom_f chomf 17833 comp_fccomf 17834

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-ov 7421 df-oprab 7422 df-mpo 7423 df-1st 7999 df-2nd 8000 df-cat 17835 df-homf 17837 df-comf 17838

This theorem is used by: cidpropd 17877 resscat 18020 funcpropd 18070 oppccatb 50093 sectpropdlem 50113 invpropdlem 50115 isopropdlem 50117 cicpropdlem 50126 resccatlem 50150 initopropd 50320 termopropd 50321 zeroopropd 50322 prcofpropd 50456 thincpropd 50519 lanpropd 50692 ranpropd 50693

W3C validator