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 17418

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 483	. . . . . . . . 9 ⊢ (((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
2	1	2ralimi 3088	. . . . . . . 8 ⊢ (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
3	2	2ralimi 3088	. . . . . . 7 ⊢ (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
4	3	adantl 482	. . . . . 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 3087	. . . . 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 483	. . . . . . . . 9 ⊢ (((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
8	7	2ralimi 3088	. . . . . . . 8 ⊢ (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
9	8	2ralimi 3088	. . . . . . 7 ⊢ (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ∧ ∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
10	9	adantl 482	. . . . . 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 3087	. . . . 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 3144	. . . . . . . 8 ⊢ Ⅎ𝑦∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)
14		nfv 1917	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)
15		nfra1 3144	. . . . . . . . . 10 ⊢ Ⅎ𝑧∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)
16		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑦∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)
17		nfra1 3144	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑔∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)
18		nfv 1917	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑓∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)
19		oveq1 7282	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = ℎ → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))
20	19	eleq1d 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = ℎ → ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)))
21	20	cbvralvw 3383	. . . . . . . . . . . . . . 15 ⊢ (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
22		oveq2 7283	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔))
23	22	eleq1d 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ((ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)))
24	23	ralbidv 3112	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)))
25	21, 24	bitrid 282	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧)))
26	17, 18, 25	cbvralw 3373	. . . . . . . . . . . . 13 ⊢ (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧))
27		oveq2 7283	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑤 → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐶)𝑤))
28		oveq2 7283	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑤 → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧) = (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤))
29	28	oveqd 7292	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) = (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔))
30		oveq2 7283	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑤 → (𝑥(Hom ‘𝐶)𝑧) = (𝑥(Hom ‘𝐶)𝑤))
31	29, 30	eleq12d 2833	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑤 → ((ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
32	27, 31	raleqbidv 3336	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑤 → (∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
33	32	ralbidv 3112	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑧)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
34	26, 33	bitrid 282	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
35	34	cbvralvw 3383	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))
36		oveq2 7283	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐶)𝑧))
37		oveq1 7282	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → (𝑦(Hom ‘𝐶)𝑤) = (𝑧(Hom ‘𝐶)𝑤))
38		opeq2 4805	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑧 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑧⟩)
39	38	oveq1d 7290	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑧 → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤) = (⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤))
40	39	oveqd 7292	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → (ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔))
41	40	eleq1d 2823	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → ((ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
42	37, 41	raleqbidv 3336	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑧 → (∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
43	36, 42	raleqbidv 3336	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
44	43	ralbidv 3112	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)∀ℎ ∈ (𝑦(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
45	35, 44	bitrid 282	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤)))
46	15, 16, 45	cbvralw 3373	. . . . . . . . 9 ⊢ (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤))
47		oveq1 7282	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐶)𝑧))
48		opeq1 4804	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑧⟩ = ⟨𝑦, 𝑧⟩)
49	48	oveq1d 7290	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤) = (⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤))
50	49	oveqd 7292	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) = (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔))
51		oveq1 7282	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑥(Hom ‘𝐶)𝑤) = (𝑦(Hom ‘𝐶)𝑤))
52	50, 51	eleq12d 2833	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
53	52	ralbidv 3112	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
54	47, 53	raleqbidv 3336	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
55	54	ralbidv 3112	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
56		ralcom 3166	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))
57	55, 56	bitrdi 287	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
58	57	ralbidv 3112	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ (Base‘𝐶)∀𝑤 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑥(Hom ‘𝐶)𝑧)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑥(Hom ‘𝐶)𝑤) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
59	46, 58	bitrid 282	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)))
60	13, 14, 59	cbvralw 3373	. . . . . . 7 ⊢ (∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))
61	60	biimpi 215	. . . . . 6 ⊢ (∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤))
62	61	ancri 550	. . . . 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 3095	. . . . . . . . . . . 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 3095	. . . . . . . . . . . . . . 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 3095	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ↔ (∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) ∧ ∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)))
66		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (Base‘𝐶) = (Base‘𝐶)
67		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
68		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (comp‘𝐶) = (comp‘𝐶)
69		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (comp‘𝐷) = (comp‘𝐷)
70		catpropd.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
71	70	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
72	71	ad4antr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
73	72	ad4antr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (comp_f‘𝐶) = (comp_f‘𝐷))
76	75	ad4antr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (comp_f‘𝐶) = (comp_f‘𝐷))
77		simpllr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
78	77	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑥 ∈ (Base‘𝐶))
79	78	ad4antr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑥 ∈ (Base‘𝐶))
80		simp-4r 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑦 ∈ (Base‘𝐶))
81	80	ad4antr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑦 ∈ (Base‘𝐶))
82		simpllr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑤 ∈ (Base‘𝐶))
83		simplr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
84	83	ad4antr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
85		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓))
87		simpllr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑧 ∈ (Base‘𝐶))
88	87	ad4antr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → 𝑧 ∈ (Base‘𝐶))
89		simp-4r 781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
90		simplr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))
92	86, 91	eqeq12d 2754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤)) → (((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))))
93	92	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → (((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
94	93	ralimdva 3108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐶)𝑤) → ∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)(((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐶)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)))))
95		ralbi 3089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 455	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3089	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 629	. . . . . . . . . . . . . . . . . . . . . . . . . 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 413	. . . . . . . . . . . . . . . . . . . . . . . . 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 3108	. . . . . . . . . . . . . . . . . . . . . . . 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 242	. . . . . . . . . . . . . . . . . . . . . . 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 453	. . . . . . . . . . . . . . . . . . . . . 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 3089	. . . . . . . . . . . . . . . . . . . . . 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 649	. . . . . . . . . . . . . . . . . . . 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 3108	. . . . . . . . . . . . . . . . . . 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 3089	. . . . . . . . . . . . . . . . . . 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 454	. . . . . . . . . . . . . . . . 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 3108	. . . . . . . . . . . . . . . 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 3089	. . . . . . . . . . . . . . . 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 242	. . . . . . . . . . . . . 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 3108	. . . . . . . . . . . . 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 3089	. . . . . . . . . . . . 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 242	. . . . . . . . . . 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 407	. . . . . . . . . 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 657	. . . . . . . . 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 629	. . . . . . . 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 457	. . . . . . 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 3108	. . . . . 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 454	. . . . 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 3089	. . . . 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 381	. . 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 17405	. . . 4 ⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷))
132		eqid 2738	. . . . . . 7 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
133		simpr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
134	66, 67, 132, 71, 133, 133	homfeqval 17406	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑥) = (𝑥(Hom ‘𝐷)𝑥))
135	131	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) → (Base‘𝐶) = (Base‘𝐷))
136	71	ad2antrr 723	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
137		simpr 485	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶))
138		simpllr 773	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
139	66, 67, 132, 136, 137, 138	homfeqval 17406	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐷)𝑥))
140	70	ad4antr 729	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
141	74	ad4antr 729	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (comp_f‘𝐶) = (comp_f‘𝐷))
142		simplr 766	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑦 ∈ (Base‘𝐶))
143		simp-4r 781	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑥 ∈ (Base‘𝐶))
144		simpr 485	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥))
145		simpllr 773	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥))
146	66, 67, 68, 69, 140, 141, 142, 143, 143, 144, 145	comfeqval 17417	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓))
147	146	eqeq1d 2740	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → ((𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ↔ (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓))
148	139, 147	raleqbidva 3354	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓))
149	66, 67, 132, 136, 138, 137	homfeqval 17406	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐷)𝑦))
150	70	ad4antr 729	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
151	74	ad4antr 729	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (comp_f‘𝐶) = (comp_f‘𝐷))
152		simp-4r 781	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑥 ∈ (Base‘𝐶))
153		simplr 766	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑦 ∈ (Base‘𝐶))
154		simpllr 773	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥))
155		simpr 485	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
156	66, 67, 68, 69, 150, 151, 152, 152, 153, 154, 155	comfeqval 17417	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔))
157	156	eqeq1d 2740	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓 ↔ (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓))
158	149, 157	raleqbidva 3354	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓))
159	148, 158	anbi12d 631	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → ((∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
160	135, 159	raleqbidva 3354	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) → (∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
161	134, 160	rexeqbidva 3355	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (∃𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ ∃𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
162	131	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐷))
163	162	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐷))
164	71	ad2antrr 723	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
165		simplr 766	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶))
166	66, 67, 132, 164, 77, 165	homfeqval 17406	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐷)𝑦))
167		simpr 485	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑧 ∈ (Base‘𝐶))
168	66, 67, 132, 164, 165, 167	homfeqval 17406	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐷)𝑧))
169	168	adantr 481	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑦(Hom ‘𝐶)𝑧) = (𝑦(Hom ‘𝐷)𝑧))
170		simpr 485	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
171	66, 67, 68, 69, 72, 75, 78, 80, 87, 83, 170	comfeqval 17417	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))
172	66, 67, 132, 164, 77, 167	homfeqval 17406	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑧) = (𝑥(Hom ‘𝐷)𝑧))
173	172	ad2antrr 723	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (𝑥(Hom ‘𝐶)𝑧) = (𝑥(Hom ‘𝐷)𝑧))
174	171, 173	eleq12d 2833	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧) ↔ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧)))
175	162	ad4antr 729	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (Base‘𝐶) = (Base‘𝐷))
176	72	adantr 481	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
177		simp-4r 781	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → 𝑧 ∈ (Base‘𝐶))
178		simpr 485	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → 𝑤 ∈ (Base‘𝐶))
179	66, 67, 132, 176, 177, 178	homfeqval 17406	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (𝑧(Hom ‘𝐶)𝑤) = (𝑧(Hom ‘𝐷)𝑤))
180	164	ad4antr 729	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
181	74	ad7antr 735	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (comp_f‘𝐶) = (comp_f‘𝐷))
182	165	ad4antr 729	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑦 ∈ (Base‘𝐶))
183	167	ad4antr 729	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧 ∈ (Base‘𝐶))
184		simplr 766	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤 ∈ (Base‘𝐶))
185		simpllr 773	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
186		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ℎ ∈ (𝑧(Hom ‘𝐶)𝑤))
187	66, 67, 68, 69, 180, 181, 182, 183, 184, 185, 186	comfeqval 17417	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔) = (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔))
188	187	oveq1d 7290	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓))
189	77	ad4antr 729	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑥 ∈ (Base‘𝐶))
190		simp-4r 781	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
191	66, 67, 68, 69, 180, 181, 189, 182, 183, 190, 185	comfeqval 17417	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))
192	191	oveq2d 7291	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓)))
193	188, 192	eqeq12d 2754	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))
194	179, 193	raleqbidva 3354	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) ∧ 𝑤 ∈ (Base‘𝐶)) → (∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))
195	175, 194	raleqbidva 3354	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (∀𝑤 ∈ (Base‘𝐶)∀ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) ↔ ∀𝑤 ∈ (Base‘𝐷)∀ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)((ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑤)𝑓) = (ℎ(⟨𝑥, 𝑧⟩(comp‘𝐷)𝑤)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐷)𝑧)𝑓))))
196	174, 195	anbi12d 631	. . . . . . . . 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 3354	. . . . . . . 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 3354	. . . . . . 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 3354	. . . . . 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 3354	. . . . 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 631	. . . 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 3354	. . 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 278	. 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 17381	. . 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 2738	. . . 4 ⊢ (Base‘𝐷) = (Base‘𝐷)
209	208, 132, 69	iscat 17381	. . 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 311	1 ⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ∈ wcel 2106 ∀wral 3064 ∃wrex 3065 ⟨cop 4567 ‘cfv 6433 (class class class)co 7275 Basecbs 16912 Hom chom 16973 compcco 16974 Catccat 17373 Hom_f chomf 17375 comp_fccomf 17376

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-ov 7278 df-oprab 7279 df-mpo 7280 df-1st 7831 df-2nd 7832 df-cat 17377 df-homf 17379 df-comf 17380

This theorem is referenced by: cidpropd 17419 resscat 17567 funcpropd 17616

W3C validator