Detailed syntax breakdown of Definition df-bj-end
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | cend 34622 |
. 2
class
End |
| 2 | | vc |
. . 3
setvar 𝑐 |
| 3 | | ccat 16928 |
. . 3
class
Cat |
| 4 | | vx |
. . . 4
setvar 𝑥 |
| 5 | 2 | cv 1535 |
. . . . 5
class 𝑐 |
| 6 | | cbs 16476 |
. . . . 5
class
Base |
| 7 | 5, 6 | cfv 6348 |
. . . 4
class
(Base‘𝑐) |
| 8 | | cnx 16473 |
. . . . . . 7
class
ndx |
| 9 | 8, 6 | cfv 6348 |
. . . . . 6
class
(Base‘ndx) |
| 10 | 4 | cv 1535 |
. . . . . . 7
class 𝑥 |
| 11 | | chom 16569 |
. . . . . . . 8
class
Hom |
| 12 | 5, 11 | cfv 6348 |
. . . . . . 7
class (Hom
‘𝑐) |
| 13 | 10, 10, 12 | co 7149 |
. . . . . 6
class (𝑥(Hom ‘𝑐)𝑥) |
| 14 | 9, 13 | cop 4566 |
. . . . 5
class
⟨(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)⟩ |
| 15 | | cplusg 16558 |
. . . . . . 7
class
+g |
| 16 | 8, 15 | cfv 6348 |
. . . . . 6
class
(+g‘ndx) |
| 17 | 10, 10 | cop 4566 |
. . . . . . 7
class
⟨𝑥, 𝑥⟩ |
| 18 | | cco 16570 |
. . . . . . . 8
class
comp |
| 19 | 5, 18 | cfv 6348 |
. . . . . . 7
class
(comp‘𝑐) |
| 20 | 17, 10, 19 | co 7149 |
. . . . . 6
class
(⟨𝑥, 𝑥⟩(comp‘𝑐)𝑥) |
| 21 | 16, 20 | cop 4566 |
. . . . 5
class
⟨(+g‘ndx), (⟨𝑥, 𝑥⟩(comp‘𝑐)𝑥)⟩ |
| 22 | 14, 21 | cpr 4562 |
. . . 4
class
{⟨(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)⟩, ⟨(+g‘ndx),
(⟨𝑥, 𝑥⟩(comp‘𝑐)𝑥)⟩} |
| 23 | 4, 7, 22 | cmpt 5139 |
. . 3
class (𝑥 ∈ (Base‘𝑐) ↦
{⟨(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)⟩, ⟨(+g‘ndx),
(⟨𝑥, 𝑥⟩(comp‘𝑐)𝑥)⟩}) |
| 24 | 2, 3, 23 | cmpt 5139 |
. 2
class (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦
{⟨(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)⟩, ⟨(+g‘ndx),
(⟨𝑥, 𝑥⟩(comp‘𝑐)𝑥)⟩})) |
| 25 | 1, 24 | wceq 1536 |
1
wff End =
(𝑐 ∈ Cat ↦
(𝑥 ∈ (Base‘𝑐) ↦
{⟨(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)⟩, ⟨(+g‘ndx),
(⟨𝑥, 𝑥⟩(comp‘𝑐)𝑥)⟩})) |
