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

Theorem iscat 16102
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 fvex 6098 . . . 4 (Base‘𝑐) ∈ V
21a1i 11 . . 3 (𝑐 = 𝐶 → (Base‘𝑐) ∈ V)
3 fveq2 6088 . . . 4 (𝑐 = 𝐶 → (Base‘𝑐) = (Base‘𝐶))
4 iscat.b . . . 4 𝐵 = (Base‘𝐶)
53, 4syl6eqr 2661 . . 3 (𝑐 = 𝐶 → (Base‘𝑐) = 𝐵)
6 fvex 6098 . . . . 5 (Hom ‘𝑐) ∈ V
76a1i 11 . . . 4 ((𝑐 = 𝐶𝑏 = 𝐵) → (Hom ‘𝑐) ∈ V)
8 simpl 471 . . . . . 6 ((𝑐 = 𝐶𝑏 = 𝐵) → 𝑐 = 𝐶)
98fveq2d 6092 . . . . 5 ((𝑐 = 𝐶𝑏 = 𝐵) → (Hom ‘𝑐) = (Hom ‘𝐶))
10 iscat.h . . . . 5 𝐻 = (Hom ‘𝐶)
119, 10syl6eqr 2661 . . . 4 ((𝑐 = 𝐶𝑏 = 𝐵) → (Hom ‘𝑐) = 𝐻)
12 fvex 6098 . . . . . 6 (comp‘𝑐) ∈ V
1312a1i 11 . . . . 5 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → (comp‘𝑐) ∈ V)
14 simpll 785 . . . . . . 7 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → 𝑐 = 𝐶)
1514fveq2d 6092 . . . . . 6 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → (comp‘𝑐) = (comp‘𝐶))
16 iscat.o . . . . . 6 · = (comp‘𝐶)
1715, 16syl6eqr 2661 . . . . 5 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → (comp‘𝑐) = · )
18 simpllr 794 . . . . . 6 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑏 = 𝐵)
19 simplr 787 . . . . . . . . 9 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → = 𝐻)
2019oveqd 6544 . . . . . . . 8 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑥𝑥) = (𝑥𝐻𝑥))
2119oveqd 6544 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑦𝑥) = (𝑦𝐻𝑥))
22 simpr 475 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑜 = · )
2322oveqd 6544 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑦, 𝑥𝑜𝑥) = (⟨𝑦, 𝑥· 𝑥))
2423oveqd 6544 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = (𝑔(⟨𝑦, 𝑥· 𝑥)𝑓))
2524eqeq1d 2611 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ↔ (𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))
2621, 25raleqbidv 3128 . . . . . . . . . 10 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))
2719oveqd 6544 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑥𝑦) = (𝑥𝐻𝑦))
2822oveqd 6544 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑥𝑜𝑦) = (⟨𝑥, 𝑥· 𝑦))
2928oveqd 6544 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = (𝑓(⟨𝑥, 𝑥· 𝑦)𝑔))
3029eqeq1d 2611 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓 ↔ (𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓))
3127, 30raleqbidv 3128 . . . . . . . . . 10 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓))
3226, 31anbi12d 742 . . . . . . . . 9 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓)))
3318, 32raleqbidv 3128 . . . . . . . 8 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ↔ ∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓)))
3420, 33rexeqbidv 3129 . . . . . . 7 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ↔ ∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓)))
3519oveqd 6544 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑦𝑧) = (𝑦𝐻𝑧))
3622oveqd 6544 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑦𝑜𝑧) = (⟨𝑥, 𝑦· 𝑧))
3736oveqd 6544 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))
3819oveqd 6544 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑥𝑧) = (𝑥𝐻𝑧))
3937, 38eleq12d 2681 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ↔ (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)))
4019oveqd 6544 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑧𝑤) = (𝑧𝐻𝑤))
4122oveqd 6544 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑦𝑜𝑤) = (⟨𝑥, 𝑦· 𝑤))
4222oveqd 6544 . . . . . . . . . . . . . . . . 17 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑦, 𝑧𝑜𝑤) = (⟨𝑦, 𝑧· 𝑤))
4342oveqd 6544 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔) = (𝑘(⟨𝑦, 𝑧· 𝑤)𝑔))
44 eqidd 2610 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑓 = 𝑓)
4541, 43, 44oveq123d 6548 . . . . . . . . . . . . . . 15 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓))
4622oveqd 6544 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑧𝑜𝑤) = (⟨𝑥, 𝑧· 𝑤))
47 eqidd 2610 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑘 = 𝑘)
4846, 47, 37oveq123d 6548 . . . . . . . . . . . . . . 15 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
4945, 48eqeq12d 2624 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) ↔ ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
5040, 49raleqbidv 3128 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) ↔ ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
5118, 50raleqbidv 3128 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) ↔ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
5239, 51anbi12d 742 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5335, 52raleqbidv 3128 . . . . . . . . . 10 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5427, 53raleqbidv 3128 . . . . . . . . 9 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5518, 54raleqbidv 3128 . . . . . . . 8 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5618, 55raleqbidv 3128 . . . . . . 7 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5734, 56anbi12d 742 . . . . . 6 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
5818, 57raleqbidv 3128 . . . . 5 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
5913, 17, 58sbcied2 3439 . . . 4 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → ([(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
607, 11, 59sbcied2 3439 . . 3 ((𝑐 = 𝐶𝑏 = 𝐵) → ([(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
612, 5, 60sbcied2 3439 . 2 (𝑐 = 𝐶 → ([(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
62 df-cat 16098 . 2 Cat = {𝑐[(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))}
6361, 62elab2g 3321 1 (𝐶𝑉 → (𝐶 ∈ Cat ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wral 2895  wrex 2896  Vcvv 3172  [wsbc 3401  cop 4130  cfv 5790  (class class class)co 6527  Basecbs 15641  Hom chom 15725  compcco 15726  Catccat 16094
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-nul 4712
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530  df-cat 16098
This theorem is referenced by:  iscatd  16103  catidex  16104  catcocl  16115  catass  16116  catpropd  16138
  Copyright terms: Public domain W3C validator