Detailed syntax breakdown of Definition df-cid
| Step | Hyp | Ref
| Expression |
| 1 | | ccid 17708 |
. 2
class
Id |
| 2 | | vc |
. . 3
setvar 𝑐 |
| 3 | | ccat 17707 |
. . 3
class
Cat |
| 4 | | vb |
. . . 4
setvar 𝑏 |
| 5 | 2 | cv 1539 |
. . . . 5
class 𝑐 |
| 6 | | cbs 17247 |
. . . . 5
class
Base |
| 7 | 5, 6 | cfv 6561 |
. . . 4
class
(Base‘𝑐) |
| 8 | | vh |
. . . . 5
setvar ℎ |
| 9 | | chom 17308 |
. . . . . 6
class
Hom |
| 10 | 5, 9 | cfv 6561 |
. . . . 5
class (Hom
‘𝑐) |
| 11 | | vo |
. . . . . 6
setvar 𝑜 |
| 12 | | cco 17309 |
. . . . . . 7
class
comp |
| 13 | 5, 12 | cfv 6561 |
. . . . . 6
class
(comp‘𝑐) |
| 14 | | vx |
. . . . . . 7
setvar 𝑥 |
| 15 | 4 | cv 1539 |
. . . . . . 7
class 𝑏 |
| 16 | | vg |
. . . . . . . . . . . . . 14
setvar 𝑔 |
| 17 | 16 | cv 1539 |
. . . . . . . . . . . . 13
class 𝑔 |
| 18 | | vf |
. . . . . . . . . . . . . 14
setvar 𝑓 |
| 19 | 18 | cv 1539 |
. . . . . . . . . . . . 13
class 𝑓 |
| 20 | | vy |
. . . . . . . . . . . . . . . 16
setvar 𝑦 |
| 21 | 20 | cv 1539 |
. . . . . . . . . . . . . . 15
class 𝑦 |
| 22 | 14 | cv 1539 |
. . . . . . . . . . . . . . 15
class 𝑥 |
| 23 | 21, 22 | cop 4632 |
. . . . . . . . . . . . . 14
class
〈𝑦, 𝑥〉 |
| 24 | 11 | cv 1539 |
. . . . . . . . . . . . . 14
class 𝑜 |
| 25 | 23, 22, 24 | co 7431 |
. . . . . . . . . . . . 13
class
(〈𝑦, 𝑥〉𝑜𝑥) |
| 26 | 17, 19, 25 | co 7431 |
. . . . . . . . . . . 12
class (𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) |
| 27 | 26, 19 | wceq 1540 |
. . . . . . . . . . 11
wff (𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 |
| 28 | 8 | cv 1539 |
. . . . . . . . . . . 12
class ℎ |
| 29 | 21, 22, 28 | co 7431 |
. . . . . . . . . . 11
class (𝑦ℎ𝑥) |
| 30 | 27, 18, 29 | wral 3061 |
. . . . . . . . . 10
wff
∀𝑓 ∈
(𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 |
| 31 | 22, 22 | cop 4632 |
. . . . . . . . . . . . . 14
class
〈𝑥, 𝑥〉 |
| 32 | 31, 21, 24 | co 7431 |
. . . . . . . . . . . . 13
class
(〈𝑥, 𝑥〉𝑜𝑦) |
| 33 | 19, 17, 32 | co 7431 |
. . . . . . . . . . . 12
class (𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) |
| 34 | 33, 19 | wceq 1540 |
. . . . . . . . . . 11
wff (𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓 |
| 35 | 22, 21, 28 | co 7431 |
. . . . . . . . . . 11
class (𝑥ℎ𝑦) |
| 36 | 34, 18, 35 | wral 3061 |
. . . . . . . . . 10
wff
∀𝑓 ∈
(𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓 |
| 37 | 30, 36 | wa 395 |
. . . . . . . . 9
wff
(∀𝑓 ∈
(𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) |
| 38 | 37, 20, 15 | wral 3061 |
. . . . . . . 8
wff
∀𝑦 ∈
𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓) |
| 39 | 22, 22, 28 | co 7431 |
. . . . . . . 8
class (𝑥ℎ𝑥) |
| 40 | 38, 16, 39 | crio 7387 |
. . . . . . 7
class
(℩𝑔
∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓)) |
| 41 | 14, 15, 40 | cmpt 5225 |
. . . . . 6
class (𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓))) |
| 42 | 11, 13, 41 | csb 3899 |
. . . . 5
class
⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓))) |
| 43 | 8, 10, 42 | csb 3899 |
. . . 4
class
⦋(Hom ‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓))) |
| 44 | 4, 7, 43 | csb 3899 |
. . 3
class
⦋(Base‘𝑐) / 𝑏⦌⦋(Hom
‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓))) |
| 45 | 2, 3, 44 | cmpt 5225 |
. 2
class (𝑐 ∈ Cat ↦
⦋(Base‘𝑐) / 𝑏⦌⦋(Hom
‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓)))) |
| 46 | 1, 45 | wceq 1540 |
1
wff Id = (𝑐 ∈ Cat ↦
⦋(Base‘𝑐) / 𝑏⦌⦋(Hom
‘𝑐) / ℎ⦌⦋(comp‘𝑐) / 𝑜⦌(𝑥 ∈ 𝑏 ↦ (℩𝑔 ∈ (𝑥ℎ𝑥)∀𝑦 ∈ 𝑏 (∀𝑓 ∈ (𝑦ℎ𝑥)(𝑔(〈𝑦, 𝑥〉𝑜𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥ℎ𝑦)(𝑓(〈𝑥, 𝑥〉𝑜𝑦)𝑔) = 𝑓)))) |