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 16973

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 485	. . . . . . . . 9 ⊢ (((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
2	1	2ralimi 3161	. . . . . . . 8 ⊢ (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
3	2	2ralimi 3161	. . . . . . 7 ⊢ (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
4	3	adantl 484	. . . . . 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 3160	. . . . 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 485	. . . . . . . . 9 ⊢ (((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
8	7	2ralimi 3161	. . . . . . . 8 ⊢ (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
9	8	2ralimi 3161	. . . . . . 7 ⊢ (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
10	9	adantl 484	. . . . . 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 3160	. . . . 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 3219	. . . . . . . 8 ⊢ Ⅎ𝑦∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)
14		nfv 1911	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)
15		nfra1 3219	. . . . . . . . . 10 ⊢ Ⅎ𝑧∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)
16		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑦∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)
17		nfra1 3219	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)
18		nfv 1911	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)
19		oveq1 7157	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = ℎ → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))
20	19	eleq1d 2897	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = ℎ → ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)))
21	20	cbvralvw 3449	. . . . . . . . . . . . . . 15 ⊢ (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
22		oveq2 7158	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔))
23	22	eleq1d 2897	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)))
24	23	ralbidv 3197	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)))
25	21, 24	syl5bb 285	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)))
26	17, 18, 25	cbvralw 3441	. . . . . . . . . . . . 13 ⊢ (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧))
27		oveq2 7158	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑤 → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐶)𝑤))
28		oveq2 7158	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑤 → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧) = (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤))
29	28	oveqd 7167	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) = (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔))
30		oveq2 7158	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → (𝑥(Hom ‘𝐶)𝑧) = (𝑥(Hom ‘𝐶)𝑤))
31	29, 30	eleq12d 2907	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑤 → ((ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
32	27, 31	raleqbidv 3401	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑤 → (∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
33	32	ralbidv 3197	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
34	26, 33	syl5bb 285	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
35	34	cbvralvw 3449	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))
36		oveq2 7158	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐶)𝑧))
37		oveq1 7157	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (𝑦(Hom ‘𝐶)𝑤) = (𝑧(Hom ‘𝐶)𝑤))
38		opeq2 4797	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑧 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩)
39	38	oveq1d 7165	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤) = (⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤))
40	39	oveqd 7167	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔))
41	40	eleq1d 2897	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → ((ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
42	37, 41	raleqbidv 3401	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
43	36, 42	raleqbidv 3401	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
44	43	ralbidv 3197	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
45	35, 44	syl5bb 285	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
46	15, 16, 45	cbvralw 3441	. . . . . . . . 9 ⊢ (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))
47		oveq1 7157	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐶)𝑧))
48		opeq1 4796	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑧⟩ = ⟨𝑦, 𝑧⟩)
49	48	oveq1d 7165	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤) = (⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤))
50	49	oveqd 7167	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) = (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔))
51		oveq1 7157	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑥(Hom ‘𝐶)𝑤) = (𝑦(Hom ‘𝐶)𝑤))
52	50, 51	eleq12d 2907	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
53	52	ralbidv 3197	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
54	47, 53	raleqbidv 3401	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
55	54	ralbidv 3197	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
56		ralcom 3354	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))
57	55, 56	syl6bb 289	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
58	57	ralbidv 3197	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (Base‘𝐶)∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
59	46, 58	syl5bb 285	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
60	13, 14, 59	cbvralw 3441	. . . . . . 7 ⊢ (∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))
61	60	biimpi 218	. . . . . 6 ⊢ (∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))
62	61	ancri 552	. . . . 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 3170	. . . . . . . . . . . 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 3170	. . . . . . . . . . . . . . 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 3170	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ↔ (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)))
66		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (Base‘𝐶) = (Base‘𝐶)
67		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
68		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (comp‘𝐶) = (comp‘𝐶)
69		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (comp‘𝐷) = (comp‘𝐷)
70		catpropd.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
71	70	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
72	71	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
73	72	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (comp_f‘𝐶) = (comp_f‘𝐷))
76	75	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (comp_f‘𝐶) = (comp_f‘𝐷))
77		simpllr 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
78	77	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑥 ∈ (Base‘𝐶))
79	78	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑥 ∈ (Base‘𝐶))
80		simp-4r 782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑦 ∈ (Base‘𝐶))
81	80	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑦 ∈ (Base‘𝐶))
82		simpllr 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑤 ∈ (Base‘𝐶))
83		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
84	83	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
85		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 16972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓))
87		simpllr 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑧 ∈ (Base‘𝐶))
88	87	ad4antr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑧 ∈ (Base‘𝐶))
89		simp-4r 782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
90		simplr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 16972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
92	86, 91	eqeq12d 2837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
93	92	ex 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → (((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
94	93	ralimdva 3177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
95		ralbi 3167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
96	94, 95	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3167	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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‘𝐶)𝑧)𝑓))))
102	101	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . . . . 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 415	. . . . . . . . . . . . . . . . . . . . . . . . 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 3177	. . . . . . . . . . . . . . . . . . . . . . . 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	syl5bir 245	. . . . . . . . . . . . . . . . . . . . . . 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 455	. . . . . . . . . . . . . . . . . . . . . 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 3167	. . . . . . . . . . . . . . . . . . . . . 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 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‘𝐶)𝑧)𝑓))))))
109	108	an32s 650	. . . . . . . . . . . . . . . . . . . 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 3177	. . . . . . . . . . . . . . . . . . 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 3167	. . . . . . . . . . . . . . . . . . 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 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‘𝐶)𝑧)𝑓))))))
113	112	expimpd 456	. . . . . . . . . . . . . . . . 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 3177	. . . . . . . . . . . . . . . 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 3167	. . . . . . . . . . . . . . . 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 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‘𝐶)𝑧)𝑓))))))
117	64, 116	syl5bir 245	. . . . . . . . . . . . . 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 3177	. . . . . . . . . . . . 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 3167	. . . . . . . . . . . . 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 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‘𝐶)𝑧)𝑓))))))
121	63, 120	syl5bir 245	. . . . . . . . . . 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 409	. . . . . . . . . 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 658	. . . . . . . . 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 630	. . . . . . . 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 459	. . . . . . 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 3177	. . . . . 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 456	. . . . 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 3167	. . . . 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 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‘𝐶)𝑧)𝑓)))))))
130	6, 12, 129	pm5.21ndd 383	. . 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 16960	. . . 4 ⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷))
132		eqid 2821	. . . . . . 7 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
133		simpr 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
134	66, 67, 132, 71, 133, 133	homfeqval 16961	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑥) = (𝑥(Hom ‘𝐷)𝑥))
135	131	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) → (Base‘𝐶) = (Base‘𝐷))
136	71	ad2antrr 724	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
137		simpr 487	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶))
138		simpllr 774	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
139	66, 67, 132, 136, 137, 138	homfeqval 16961	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐷)𝑥))
140	70	ad4antr 730	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
141	74	ad4antr 730	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (comp_f‘𝐶) = (comp_f‘𝐷))
142		simplr 767	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑦 ∈ (Base‘𝐶))
143		simp-4r 782	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑥 ∈ (Base‘𝐶))
144		simpr 487	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥))
145		simpllr 774	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥))
146	66, 67, 68, 69, 140, 141, 142, 143, 143, 144, 145	comfeqval 16972	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓))
147	146	eqeq1d 2823	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → ((𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ↔ (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓))
148	139, 147	raleqbidva 3425	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓))
149	66, 67, 132, 136, 138, 137	homfeqval 16961	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐷)𝑦))
150	70	ad4antr 730	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
151	74	ad4antr 730	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (comp_f‘𝐶) = (comp_f‘𝐷))
152		simp-4r 782	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑥 ∈ (Base‘𝐶))
153		simplr 767	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑦 ∈ (Base‘𝐶))
154		simpllr 774	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥))
155		simpr 487	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
156	66, 67, 68, 69, 150, 151, 152, 152, 153, 154, 155	comfeqval 16972	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔))
157	156	eqeq1d 2823	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓 ↔ (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓))
158	149, 157	raleqbidva 3425	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓))
159	148, 158	anbi12d 632	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → ((∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
160	135, 159	raleqbidva 3425	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) → (∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
161	134, 160	rexeqbidva 3426	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ ∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
162	131	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐷))
163	162	adantr 483	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐷))
164	71	ad2antrr 724	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
165		simplr 767	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶))
166	66, 67, 132, 164, 77, 165	homfeqval 16961	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐷)𝑦))
167		simpr 487	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑧 ∈ (Base‘𝐶))
168	66, 67, 132, 164, 165, 167	homfeqval 16961	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐷)𝑧))
169	168	adantr 483	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐷)𝑧))
170		simpr 487	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
171	66, 67, 68, 69, 72, 75, 78, 80, 87, 83, 170	comfeqval 16972	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))
172	66, 67, 132, 164, 77, 167	homfeqval 16961	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑧) = (𝑥(Hom ‘𝐷)𝑧))
173	172	ad2antrr 724	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (𝑥(Hom ‘𝐶)𝑧) = (𝑥(Hom ‘𝐷)𝑧))
174	171, 173	eleq12d 2907	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧)))
175	162	ad4antr 730	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (Base‘𝐶) = (Base‘𝐷))
176	72	adantr 483	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
177		simp-4r 782	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → 𝑧 ∈ (Base‘𝐶))
178		simpr 487	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → 𝑤 ∈ (Base‘𝐶))
179	66, 67, 132, 176, 177, 178	homfeqval 16961	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (𝑧(Hom ‘𝐶)𝑤) = (𝑧(Hom ‘𝐷)𝑤))
180	164	ad4antr 730	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
181	74	ad7antr 736	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (comp_f‘𝐶) = (comp_f‘𝐷))
182	165	ad4antr 730	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑦 ∈ (Base‘𝐶))
183	167	ad4antr 730	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧 ∈ (Base‘𝐶))
184		simplr 767	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤 ∈ (Base‘𝐶))
185		simpllr 774	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
186		simpr 487	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ℎ ∈ (𝑧(Hom ‘𝐶)𝑤))
187	66, 67, 68, 69, 180, 181, 182, 183, 184, 185, 186	comfeqval 16972	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) = (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔))
188	187	oveq1d 7165	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓))
189	77	ad4antr 730	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑥 ∈ (Base‘𝐶))
190		simp-4r 782	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
191	66, 67, 68, 69, 180, 181, 189, 182, 183, 190, 185	comfeqval 16972	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))
192	191	oveq2d 7166	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓)))
193	188, 192	eqeq12d 2837	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))
194	179, 193	raleqbidva 3425	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))
195	175, 194	raleqbidva 3425	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))
196	174, 195	anbi12d 632	. . . . . . . . 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 3425	. . . . . . . 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 3425	. . . . . . 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 3425	. . . . . 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 3425	. . . . 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 632	. . . 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 3425	. . 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 281	. 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 16937	. . 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 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 2821	. . . 4 ⊢ (Base‘𝐷) = (Base‘𝐷)
209	208, 132, 69	iscat 16937	. . 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 17	. 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 313	1 ⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1533 ∈ wcel 2110 ∀wral 3138 ∃wrex 3139 ⟨cop 4566 ‘cfv 6349 (class class class)co 7150 Basecbs 16477 Hom chom 16570 compcco 16571 Catccat 16929 Hom_f chomf 16931 comp_fccomf 16932

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5182 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-op 4567 df-uni 4832 df-iun 4913 df-br 5059 df-opab 5121 df-mpt 5139 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-ov 7153 df-oprab 7154 df-mpo 7155 df-1st 7683 df-2nd 7684 df-cat 16933 df-homf 16935 df-comf 16936

This theorem is referenced by: cidpropd 16974 resscat 17116 funcpropd 17164

W3C validator