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

Theorem iscat 16935
 Description: The predicate "is a category". (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
iscat.b 𝐵 = (Base‘𝐶)
iscat.h 𝐻 = (Hom ‘𝐶)
iscat.o · = (comp‘𝐶)
Assertion
Ref Expression
iscat (𝐶𝑉 → (𝐶 ∈ Cat ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
Distinct variable groups:   𝑓,𝑔,𝑘,𝑤,𝑥,𝑦,𝑧, ·   𝐵,𝑓,𝑔,𝑘,𝑤,𝑥,𝑦,𝑧   𝐶,𝑓,𝑔,𝑘,𝑤,𝑥,𝑦,𝑧   𝑓,𝐻,𝑔,𝑘,𝑤,𝑥,𝑦,𝑧
Allowed substitution hints:   𝑉(𝑥,𝑦,𝑧,𝑤,𝑓,𝑔,𝑘)

Proof of Theorem iscat
Dummy variables 𝑏 𝑐 𝑜 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvexd 6660 . . 3 (𝑐 = 𝐶 → (Base‘𝑐) ∈ V)
2 fveq2 6645 . . . 4 (𝑐 = 𝐶 → (Base‘𝑐) = (Base‘𝐶))
3 iscat.b . . . 4 𝐵 = (Base‘𝐶)
42, 3eqtr4di 2851 . . 3 (𝑐 = 𝐶 → (Base‘𝑐) = 𝐵)
5 fvexd 6660 . . . 4 ((𝑐 = 𝐶𝑏 = 𝐵) → (Hom ‘𝑐) ∈ V)
6 simpl 486 . . . . . 6 ((𝑐 = 𝐶𝑏 = 𝐵) → 𝑐 = 𝐶)
76fveq2d 6649 . . . . 5 ((𝑐 = 𝐶𝑏 = 𝐵) → (Hom ‘𝑐) = (Hom ‘𝐶))
8 iscat.h . . . . 5 𝐻 = (Hom ‘𝐶)
97, 8eqtr4di 2851 . . . 4 ((𝑐 = 𝐶𝑏 = 𝐵) → (Hom ‘𝑐) = 𝐻)
10 fvexd 6660 . . . . 5 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → (comp‘𝑐) ∈ V)
11 simpll 766 . . . . . . 7 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → 𝑐 = 𝐶)
1211fveq2d 6649 . . . . . 6 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → (comp‘𝑐) = (comp‘𝐶))
13 iscat.o . . . . . 6 · = (comp‘𝐶)
1412, 13eqtr4di 2851 . . . . 5 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → (comp‘𝑐) = · )
15 simpllr 775 . . . . . 6 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑏 = 𝐵)
16 simplr 768 . . . . . . . . 9 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → = 𝐻)
1716oveqd 7152 . . . . . . . 8 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑥𝑥) = (𝑥𝐻𝑥))
1816oveqd 7152 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑦𝑥) = (𝑦𝐻𝑥))
19 simpr 488 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑜 = · )
2019oveqd 7152 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑦, 𝑥𝑜𝑥) = (⟨𝑦, 𝑥· 𝑥))
2120oveqd 7152 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = (𝑔(⟨𝑦, 𝑥· 𝑥)𝑓))
2221eqeq1d 2800 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ↔ (𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))
2318, 22raleqbidv 3354 . . . . . . . . . 10 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))
2416oveqd 7152 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑥𝑦) = (𝑥𝐻𝑦))
2519oveqd 7152 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑥𝑜𝑦) = (⟨𝑥, 𝑥· 𝑦))
2625oveqd 7152 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = (𝑓(⟨𝑥, 𝑥· 𝑦)𝑔))
2726eqeq1d 2800 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓 ↔ (𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓))
2824, 27raleqbidv 3354 . . . . . . . . . 10 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓))
2923, 28anbi12d 633 . . . . . . . . 9 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓)))
3015, 29raleqbidv 3354 . . . . . . . 8 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ↔ ∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓)))
3117, 30rexeqbidv 3355 . . . . . . 7 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ↔ ∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓)))
3216oveqd 7152 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑦𝑧) = (𝑦𝐻𝑧))
3319oveqd 7152 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑦𝑜𝑧) = (⟨𝑥, 𝑦· 𝑧))
3433oveqd 7152 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))
3516oveqd 7152 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑥𝑧) = (𝑥𝐻𝑧))
3634, 35eleq12d 2884 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ↔ (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)))
3716oveqd 7152 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑧𝑤) = (𝑧𝐻𝑤))
3819oveqd 7152 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑦𝑜𝑤) = (⟨𝑥, 𝑦· 𝑤))
3919oveqd 7152 . . . . . . . . . . . . . . . . 17 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑦, 𝑧𝑜𝑤) = (⟨𝑦, 𝑧· 𝑤))
4039oveqd 7152 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔) = (𝑘(⟨𝑦, 𝑧· 𝑤)𝑔))
41 eqidd 2799 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑓 = 𝑓)
4238, 40, 41oveq123d 7156 . . . . . . . . . . . . . . 15 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓))
4319oveqd 7152 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑧𝑜𝑤) = (⟨𝑥, 𝑧· 𝑤))
44 eqidd 2799 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑘 = 𝑘)
4543, 44, 34oveq123d 7156 . . . . . . . . . . . . . . 15 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
4642, 45eqeq12d 2814 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) ↔ ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
4737, 46raleqbidv 3354 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) ↔ ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
4815, 47raleqbidv 3354 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) ↔ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
4936, 48anbi12d 633 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5032, 49raleqbidv 3354 . . . . . . . . . 10 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5124, 50raleqbidv 3354 . . . . . . . . 9 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5215, 51raleqbidv 3354 . . . . . . . 8 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5315, 52raleqbidv 3354 . . . . . . 7 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5431, 53anbi12d 633 . . . . . 6 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
5515, 54raleqbidv 3354 . . . . 5 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
5610, 14, 55sbcied2 3763 . . . 4 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → ([(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
575, 9, 56sbcied2 3763 . . 3 ((𝑐 = 𝐶𝑏 = 𝐵) → ([(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
581, 4, 57sbcied2 3763 . 2 (𝑐 = 𝐶 → ([(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
59 df-cat 16931 . 2 Cat = {𝑐[(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))}
6058, 59elab2g 3616 1 (𝐶𝑉 → (𝐶 ∈ Cat ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  Vcvv 3441  [wsbc 3720  ⟨cop 4531  ‘cfv 6324  (class class class)co 7135  Basecbs 16475  Hom chom 16568  compcco 16569  Catccat 16927 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-nul 5174 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-cat 16931 This theorem is referenced by:  iscatd  16936  catidex  16937  catcocl  16948  catass  16949  catpropd  16971
 Copyright terms: Public domain W3C validator