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

Theorem iscat 16540
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 6344 . . 3 (𝑐 = 𝐶 → (Base‘𝑐) ∈ V)
2 fveq2 6332 . . . 4 (𝑐 = 𝐶 → (Base‘𝑐) = (Base‘𝐶))
3 iscat.b . . . 4 𝐵 = (Base‘𝐶)
42, 3syl6eqr 2823 . . 3 (𝑐 = 𝐶 → (Base‘𝑐) = 𝐵)
5 fvexd 6344 . . . 4 ((𝑐 = 𝐶𝑏 = 𝐵) → (Hom ‘𝑐) ∈ V)
6 simpl 468 . . . . . 6 ((𝑐 = 𝐶𝑏 = 𝐵) → 𝑐 = 𝐶)
76fveq2d 6336 . . . . 5 ((𝑐 = 𝐶𝑏 = 𝐵) → (Hom ‘𝑐) = (Hom ‘𝐶))
8 iscat.h . . . . 5 𝐻 = (Hom ‘𝐶)
97, 8syl6eqr 2823 . . . 4 ((𝑐 = 𝐶𝑏 = 𝐵) → (Hom ‘𝑐) = 𝐻)
10 fvexd 6344 . . . . 5 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → (comp‘𝑐) ∈ V)
11 simpll 750 . . . . . . 7 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → 𝑐 = 𝐶)
1211fveq2d 6336 . . . . . 6 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → (comp‘𝑐) = (comp‘𝐶))
13 iscat.o . . . . . 6 · = (comp‘𝐶)
1412, 13syl6eqr 2823 . . . . 5 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → (comp‘𝑐) = · )
15 simpllr 760 . . . . . 6 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑏 = 𝐵)
16 simplr 752 . . . . . . . . 9 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → = 𝐻)
1716oveqd 6810 . . . . . . . 8 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑥𝑥) = (𝑥𝐻𝑥))
1816oveqd 6810 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑦𝑥) = (𝑦𝐻𝑥))
19 simpr 471 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑜 = · )
2019oveqd 6810 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑦, 𝑥𝑜𝑥) = (⟨𝑦, 𝑥· 𝑥))
2120oveqd 6810 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = (𝑔(⟨𝑦, 𝑥· 𝑥)𝑓))
2221eqeq1d 2773 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ↔ (𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))
2318, 22raleqbidv 3301 . . . . . . . . . 10 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))
2416oveqd 6810 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑥𝑦) = (𝑥𝐻𝑦))
2519oveqd 6810 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑥𝑜𝑦) = (⟨𝑥, 𝑥· 𝑦))
2625oveqd 6810 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = (𝑓(⟨𝑥, 𝑥· 𝑦)𝑔))
2726eqeq1d 2773 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓 ↔ (𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓))
2824, 27raleqbidv 3301 . . . . . . . . . 10 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓))
2923, 28anbi12d 616 . . . . . . . . 9 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓)))
3015, 29raleqbidv 3301 . . . . . . . 8 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ↔ ∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓)))
3117, 30rexeqbidv 3302 . . . . . . 7 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ↔ ∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓)))
3216oveqd 6810 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑦𝑧) = (𝑦𝐻𝑧))
3319oveqd 6810 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑦𝑜𝑧) = (⟨𝑥, 𝑦· 𝑧))
3433oveqd 6810 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))
3516oveqd 6810 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑥𝑧) = (𝑥𝐻𝑧))
3634, 35eleq12d 2844 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ↔ (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)))
3716oveqd 6810 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑧𝑤) = (𝑧𝐻𝑤))
3819oveqd 6810 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑦𝑜𝑤) = (⟨𝑥, 𝑦· 𝑤))
3919oveqd 6810 . . . . . . . . . . . . . . . . 17 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑦, 𝑧𝑜𝑤) = (⟨𝑦, 𝑧· 𝑤))
4039oveqd 6810 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔) = (𝑘(⟨𝑦, 𝑧· 𝑤)𝑔))
41 eqidd 2772 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑓 = 𝑓)
4238, 40, 41oveq123d 6814 . . . . . . . . . . . . . . 15 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓))
4319oveqd 6810 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑧𝑜𝑤) = (⟨𝑥, 𝑧· 𝑤))
44 eqidd 2772 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑘 = 𝑘)
4543, 44, 34oveq123d 6814 . . . . . . . . . . . . . . 15 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
4642, 45eqeq12d 2786 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) ↔ ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
4737, 46raleqbidv 3301 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) ↔ ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
4815, 47raleqbidv 3301 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) ↔ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
4936, 48anbi12d 616 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5032, 49raleqbidv 3301 . . . . . . . . . 10 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5124, 50raleqbidv 3301 . . . . . . . . 9 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5215, 51raleqbidv 3301 . . . . . . . 8 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5315, 52raleqbidv 3301 . . . . . . 7 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5431, 53anbi12d 616 . . . . . 6 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
5515, 54raleqbidv 3301 . . . . 5 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
5610, 14, 55sbcied2 3625 . . . 4 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → ([(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
575, 9, 56sbcied2 3625 . . 3 ((𝑐 = 𝐶𝑏 = 𝐵) → ([(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
581, 4, 57sbcied2 3625 . 2 (𝑐 = 𝐶 → ([(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
59 df-cat 16536 . 2 Cat = {𝑐[(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))}
6058, 59elab2g 3504 1 (𝐶𝑉 → (𝐶 ∈ Cat ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  wral 3061  wrex 3062  Vcvv 3351  [wsbc 3587  cop 4322  cfv 6031  (class class class)co 6793  Basecbs 16064  Hom chom 16160  compcco 16161  Catccat 16532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-nul 4923
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5994  df-fv 6039  df-ov 6796  df-cat 16536
This theorem is referenced by:  iscatd  16541  catidex  16542  catcocl  16553  catass  16554  catpropd  16576
  Copyright terms: Public domain W3C validator