Detailed syntax breakdown of Definition df-cat
| Step | Hyp | Ref
| Expression |
| 1 | | ccat 17707 |
. 2
class
Cat |
| 2 | | vg |
. . . . . . . . . . . . . . 15
setvar 𝑔 |
| 3 | 2 | cv 1539 |
. . . . . . . . . . . . . 14
class 𝑔 |
| 4 | | vf |
. . . . . . . . . . . . . . 15
setvar 𝑓 |
| 5 | 4 | cv 1539 |
. . . . . . . . . . . . . 14
class 𝑓 |
| 6 | | vy |
. . . . . . . . . . . . . . . . 17
setvar 𝑦 |
| 7 | 6 | cv 1539 |
. . . . . . . . . . . . . . . 16
class 𝑦 |
| 8 | | vx |
. . . . . . . . . . . . . . . . 17
setvar 𝑥 |
| 9 | 8 | cv 1539 |
. . . . . . . . . . . . . . . 16
class 𝑥 |
| 10 | 7, 9 | cop 4632 |
. . . . . . . . . . . . . . 15
class
〈𝑦, 𝑥〉 |
| 11 | | vo |
. . . . . . . . . . . . . . . 16
setvar 𝑜 |
| 12 | 11 | cv 1539 |
. . . . . . . . . . . . . . 15
class 𝑜 |
| 13 | 10, 9, 12 | co 7431 |
. . . . . . . . . . . . . 14
class
(〈𝑦, 𝑥〉𝑜𝑥) |
| 14 | 3, 5, 13 | co 7431 |
. . . . . . . . . . . . 13
class (𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) |
| 15 | 14, 5 | wceq 1540 |
. . . . . . . . . . . 12
wff (𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 |
| 16 | | vh |
. . . . . . . . . . . . . 14
setvar ℎ |
| 17 | 16 | cv 1539 |
. . . . . . . . . . . . 13
class ℎ |
| 18 | 7, 9, 17 | co 7431 |
. . . . . . . . . . . 12
class (𝑦ℎ𝑥) |
| 19 | 15, 4, 18 | wral 3061 |
. . . . . . . . . . 11
wff
∀𝑓 ∈
(𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 |
| 20 | 9, 9 | cop 4632 |
. . . . . . . . . . . . . . 15
class
〈𝑥, 𝑥〉 |
| 21 | 20, 7, 12 | co 7431 |
. . . . . . . . . . . . . 14
class
(〈𝑥, 𝑥〉𝑜𝑦) |
| 22 | 5, 3, 21 | co 7431 |
. . . . . . . . . . . . 13
class (𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) |
| 23 | 22, 5 | wceq 1540 |
. . . . . . . . . . . 12
wff (𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓 |
| 24 | 9, 7, 17 | co 7431 |
. . . . . . . . . . . 12
class (𝑥ℎ𝑦) |
| 25 | 23, 4, 24 | wral 3061 |
. . . . . . . . . . 11
wff
∀𝑓 ∈
(𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓 |
| 26 | 19, 25 | wa 395 |
. . . . . . . . . 10
wff
(∀𝑓 ∈
(𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) |
| 27 | | vb |
. . . . . . . . . . 11
setvar 𝑏 |
| 28 | 27 | cv 1539 |
. . . . . . . . . 10
class 𝑏 |
| 29 | 26, 6, 28 | wral 3061 |
. . . . . . . . 9
wff
∀𝑦 ∈
𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) |
| 30 | 9, 9, 17 | co 7431 |
. . . . . . . . 9
class (𝑥ℎ𝑥) |
| 31 | 29, 2, 30 | wrex 3070 |
. . . . . . . 8
wff
∃𝑔 ∈
(𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) |
| 32 | 9, 7 | cop 4632 |
. . . . . . . . . . . . . . . 16
class
〈𝑥, 𝑦〉 |
| 33 | | vz |
. . . . . . . . . . . . . . . . 17
setvar 𝑧 |
| 34 | 33 | cv 1539 |
. . . . . . . . . . . . . . . 16
class 𝑧 |
| 35 | 32, 34, 12 | co 7431 |
. . . . . . . . . . . . . . 15
class
(〈𝑥, 𝑦〉𝑜𝑧) |
| 36 | 3, 5, 35 | co 7431 |
. . . . . . . . . . . . . 14
class (𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) |
| 37 | 9, 34, 17 | co 7431 |
. . . . . . . . . . . . . 14
class (𝑥ℎ𝑧) |
| 38 | 36, 37 | wcel 2108 |
. . . . . . . . . . . . 13
wff (𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) |
| 39 | | vk |
. . . . . . . . . . . . . . . . . . 19
setvar 𝑘 |
| 40 | 39 | cv 1539 |
. . . . . . . . . . . . . . . . . 18
class 𝑘 |
| 41 | 7, 34 | cop 4632 |
. . . . . . . . . . . . . . . . . . 19
class
〈𝑦, 𝑧〉 |
| 42 | | vw |
. . . . . . . . . . . . . . . . . . . 20
setvar 𝑤 |
| 43 | 42 | cv 1539 |
. . . . . . . . . . . . . . . . . . 19
class 𝑤 |
| 44 | 41, 43, 12 | co 7431 |
. . . . . . . . . . . . . . . . . 18
class
(〈𝑦, 𝑧〉𝑜𝑤) |
| 45 | 40, 3, 44 | co 7431 |
. . . . . . . . . . . . . . . . 17
class (𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔) |
| 46 | 32, 43, 12 | co 7431 |
. . . . . . . . . . . . . . . . 17
class
(〈𝑥, 𝑦〉𝑜𝑤) |
| 47 | 45, 5, 46 | co 7431 |
. . . . . . . . . . . . . . . 16
class ((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) |
| 48 | 9, 34 | cop 4632 |
. . . . . . . . . . . . . . . . . 18
class
〈𝑥, 𝑧〉 |
| 49 | 48, 43, 12 | co 7431 |
. . . . . . . . . . . . . . . . 17
class
(〈𝑥, 𝑧〉𝑜𝑤) |
| 50 | 40, 36, 49 | co 7431 |
. . . . . . . . . . . . . . . 16
class (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓)) |
| 51 | 47, 50 | wceq 1540 |
. . . . . . . . . . . . . . 15
wff ((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓)) |
| 52 | 34, 43, 17 | co 7431 |
. . . . . . . . . . . . . . 15
class (𝑧ℎ𝑤) |
| 53 | 51, 39, 52 | wral 3061 |
. . . . . . . . . . . . . 14
wff
∀𝑘 ∈
(𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓)) |
| 54 | 53, 42, 28 | wral 3061 |
. . . . . . . . . . . . 13
wff
∀𝑤 ∈
𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓)) |
| 55 | 38, 54 | wa 395 |
. . . . . . . . . . . 12
wff ((𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓))) |
| 56 | 7, 34, 17 | co 7431 |
. . . . . . . . . . . 12
class (𝑦ℎ𝑧) |
| 57 | 55, 2, 56 | wral 3061 |
. . . . . . . . . . 11
wff
∀𝑔 ∈
(𝑦ℎ𝑧)((𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓))) |
| 58 | 57, 4, 24 | wral 3061 |
. . . . . . . . . 10
wff
∀𝑓 ∈
(𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓))) |
| 59 | 58, 33, 28 | wral 3061 |
. . . . . . . . 9
wff
∀𝑧 ∈
𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓))) |
| 60 | 59, 6, 28 | wral 3061 |
. . . . . . . 8
wff
∀𝑦 ∈
𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓))) |
| 61 | 31, 60 | wa 395 |
. . . . . . 7
wff
(∃𝑔 ∈
(𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓)))) |
| 62 | 61, 8, 28 | wral 3061 |
. . . . . 6
wff
∀𝑥 ∈
𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓)))) |
| 63 | | vc |
. . . . . . . 8
setvar 𝑐 |
| 64 | 63 | cv 1539 |
. . . . . . 7
class 𝑐 |
| 65 | | cco 17309 |
. . . . . . 7
class
comp |
| 66 | 64, 65 | cfv 6561 |
. . . . . 6
class
(comp‘𝑐) |
| 67 | 62, 11, 66 | wsbc 3788 |
. . . . 5
wff
[(comp‘𝑐) / 𝑜]∀𝑥 ∈ 𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓)))) |
| 68 | | chom 17308 |
. . . . . 6
class
Hom |
| 69 | 64, 68 | cfv 6561 |
. . . . 5
class (Hom
‘𝑐) |
| 70 | 67, 16, 69 | wsbc 3788 |
. . . 4
wff
[(Hom ‘𝑐) / ℎ][(comp‘𝑐) / 𝑜]∀𝑥 ∈ 𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓)))) |
| 71 | | cbs 17247 |
. . . . 5
class
Base |
| 72 | 64, 71 | cfv 6561 |
. . . 4
class
(Base‘𝑐) |
| 73 | 70, 27, 72 | wsbc 3788 |
. . 3
wff
[(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ][(comp‘𝑐) / 𝑜]∀𝑥 ∈ 𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓)))) |
| 74 | 73, 63 | cab 2714 |
. 2
class {𝑐 ∣
[(Base‘𝑐) /
𝑏][(Hom
‘𝑐) / ℎ][(comp‘𝑐) / 𝑜]∀𝑥 ∈ 𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓))))} |
| 75 | 1, 74 | wceq 1540 |
1
wff Cat =
{𝑐 ∣
[(Base‘𝑐) /
𝑏][(Hom
‘𝑐) / ℎ][(comp‘𝑐) / 𝑜]∀𝑥 ∈ 𝑏 (∃𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)((𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓) ∈ (𝑥ℎ𝑧) ∧ ∀𝑤 ∈ 𝑏 ∀𝑘 ∈ (𝑧ℎ𝑤)((𝑘(〈𝑦, 𝑧〉𝑜𝑤)𝑔)(〈𝑥, 𝑦〉𝑜𝑤)𝑓) = (𝑘(〈𝑥, 𝑧〉𝑜𝑤)(𝑔(〈𝑥, 𝑦〉𝑜𝑧)𝑓))))} |