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

Theorem iscat 16156
 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 6113 . . . 4 (Base‘𝑐) ∈ V
21a1i 11 . . 3 (𝑐 = 𝐶 → (Base‘𝑐) ∈ V)
3 fveq2 6103 . . . 4 (𝑐 = 𝐶 → (Base‘𝑐) = (Base‘𝐶))
4 iscat.b . . . 4 𝐵 = (Base‘𝐶)
53, 4syl6eqr 2662 . . 3 (𝑐 = 𝐶 → (Base‘𝑐) = 𝐵)
6 fvex 6113 . . . . 5 (Hom ‘𝑐) ∈ V
76a1i 11 . . . 4 ((𝑐 = 𝐶𝑏 = 𝐵) → (Hom ‘𝑐) ∈ V)
8 simpl 472 . . . . . 6 ((𝑐 = 𝐶𝑏 = 𝐵) → 𝑐 = 𝐶)
98fveq2d 6107 . . . . 5 ((𝑐 = 𝐶𝑏 = 𝐵) → (Hom ‘𝑐) = (Hom ‘𝐶))
10 iscat.h . . . . 5 𝐻 = (Hom ‘𝐶)
119, 10syl6eqr 2662 . . . 4 ((𝑐 = 𝐶𝑏 = 𝐵) → (Hom ‘𝑐) = 𝐻)
12 fvex 6113 . . . . . 6 (comp‘𝑐) ∈ V
1312a1i 11 . . . . 5 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → (comp‘𝑐) ∈ V)
14 simpll 786 . . . . . . 7 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → 𝑐 = 𝐶)
1514fveq2d 6107 . . . . . 6 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → (comp‘𝑐) = (comp‘𝐶))
16 iscat.o . . . . . 6 · = (comp‘𝐶)
1715, 16syl6eqr 2662 . . . . 5 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → (comp‘𝑐) = · )
18 simpllr 795 . . . . . 6 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑏 = 𝐵)
19 simplr 788 . . . . . . . . 9 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → = 𝐻)
2019oveqd 6566 . . . . . . . 8 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑥𝑥) = (𝑥𝐻𝑥))
2119oveqd 6566 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑦𝑥) = (𝑦𝐻𝑥))
22 simpr 476 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑜 = · )
2322oveqd 6566 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑦, 𝑥𝑜𝑥) = (⟨𝑦, 𝑥· 𝑥))
2423oveqd 6566 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = (𝑔(⟨𝑦, 𝑥· 𝑥)𝑓))
2524eqeq1d 2612 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ↔ (𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))
2621, 25raleqbidv 3129 . . . . . . . . . 10 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓))
2719oveqd 6566 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑥𝑦) = (𝑥𝐻𝑦))
2822oveqd 6566 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑥𝑜𝑦) = (⟨𝑥, 𝑥· 𝑦))
2928oveqd 6566 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = (𝑓(⟨𝑥, 𝑥· 𝑦)𝑔))
3029eqeq1d 2612 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓 ↔ (𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓))
3127, 30raleqbidv 3129 . . . . . . . . . 10 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓))
3226, 31anbi12d 743 . . . . . . . . 9 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓)))
3318, 32raleqbidv 3129 . . . . . . . 8 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ↔ ∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓)))
3420, 33rexeqbidv 3130 . . . . . . 7 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ↔ ∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓)))
3519oveqd 6566 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑦𝑧) = (𝑦𝐻𝑧))
3622oveqd 6566 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑦𝑜𝑧) = (⟨𝑥, 𝑦· 𝑧))
3736oveqd 6566 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))
3819oveqd 6566 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑥𝑧) = (𝑥𝐻𝑧))
3937, 38eleq12d 2682 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ↔ (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧)))
4019oveqd 6566 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑧𝑤) = (𝑧𝐻𝑤))
4122oveqd 6566 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑦𝑜𝑤) = (⟨𝑥, 𝑦· 𝑤))
4222oveqd 6566 . . . . . . . . . . . . . . . . 17 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑦, 𝑧𝑜𝑤) = (⟨𝑦, 𝑧· 𝑤))
4342oveqd 6566 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔) = (𝑘(⟨𝑦, 𝑧· 𝑤)𝑔))
44 eqidd 2611 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑓 = 𝑓)
4541, 43, 44oveq123d 6570 . . . . . . . . . . . . . . 15 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓))
4622oveqd 6566 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (⟨𝑥, 𝑧𝑜𝑤) = (⟨𝑥, 𝑧· 𝑤))
47 eqidd 2611 . . . . . . . . . . . . . . . 16 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → 𝑘 = 𝑘)
4846, 47, 37oveq123d 6570 . . . . . . . . . . . . . . 15 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))
4945, 48eqeq12d 2625 . . . . . . . . . . . . . 14 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) ↔ ((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
5040, 49raleqbidv 3129 . . . . . . . . . . . . 13 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) ↔ ∀𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
5118, 50raleqbidv 3129 . . . . . . . . . . . 12 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)) ↔ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))
5239, 51anbi12d 743 . . . . . . . . . . 11 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5335, 52raleqbidv 3129 . . . . . . . . . 10 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5427, 53raleqbidv 3129 . . . . . . . . 9 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5518, 54raleqbidv 3129 . . . . . . . 8 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5618, 55raleqbidv 3129 . . . . . . 7 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))) ↔ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓)))))
5734, 56anbi12d 743 . . . . . 6 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → ((∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
5818, 57raleqbidv 3129 . . . . 5 ((((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) ∧ 𝑜 = · ) → (∀𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
5913, 17, 58sbcied2 3440 . . . 4 (((𝑐 = 𝐶𝑏 = 𝐵) ∧ = 𝐻) → ([(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
607, 11, 59sbcied2 3440 . . 3 ((𝑐 = 𝐶𝑏 = 𝐵) → ([(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
612, 5, 60sbcied2 3440 . 2 (𝑐 = 𝐶 → ([(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓)))) ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
62 df-cat 16152 . 2 Cat = {𝑐[(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ][(comp‘𝑐) / 𝑜]𝑥𝑏 (∃𝑔 ∈ (𝑥𝑥)∀𝑦𝑏 (∀𝑓 ∈ (𝑦𝑥)(𝑔(⟨𝑦, 𝑥𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝑦)(𝑓(⟨𝑥, 𝑥𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝑏𝑧𝑏𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)((𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓) ∈ (𝑥𝑧) ∧ ∀𝑤𝑏𝑘 ∈ (𝑧𝑤)((𝑘(⟨𝑦, 𝑧𝑜𝑤)𝑔)(⟨𝑥, 𝑦𝑜𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧𝑜𝑤)(𝑔(⟨𝑥, 𝑦𝑜𝑧)𝑓))))}
6361, 62elab2g 3322 1 (𝐶𝑉 → (𝐶 ∈ Cat ↔ ∀𝑥𝐵 (∃𝑔 ∈ (𝑥𝐻𝑥)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑥)(𝑔(⟨𝑦, 𝑥· 𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥𝐻𝑦)(𝑓(⟨𝑥, 𝑥· 𝑦)𝑔) = 𝑓) ∧ ∀𝑦𝐵𝑧𝐵𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐻𝑧) ∧ ∀𝑤𝐵𝑘 ∈ (𝑧𝐻𝑤)((𝑘(⟨𝑦, 𝑧· 𝑤)𝑔)(⟨𝑥, 𝑦· 𝑤)𝑓) = (𝑘(⟨𝑥, 𝑧· 𝑤)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  Vcvv 3173  [wsbc 3402  ⟨cop 4131  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  Hom chom 15779  compcco 15780  Catccat 16148 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-cat 16152 This theorem is referenced by:  iscatd  16157  catidex  16158  catcocl  16169  catass  16170  catpropd  16192
 Copyright terms: Public domain W3C validator