Detailed syntax breakdown of Definition df-mndtc
Step | Hyp | Ref
| Expression |
1 | | cmndtc 45865 |
. 2
class
MndToCat |
2 | | vm |
. . 3
setvar 𝑚 |
3 | | cmnd 18039 |
. . 3
class
Mnd |
4 | | cnx 16595 |
. . . . . 6
class
ndx |
5 | | cbs 16598 |
. . . . . 6
class
Base |
6 | 4, 5 | cfv 6349 |
. . . . 5
class
(Base‘ndx) |
7 | 2 | cv 1541 |
. . . . . 6
class 𝑚 |
8 | 7 | csn 4526 |
. . . . 5
class {𝑚} |
9 | 6, 8 | cop 4532 |
. . . 4
class
〈(Base‘ndx), {𝑚}〉 |
10 | | chom 16691 |
. . . . . 6
class
Hom |
11 | 4, 10 | cfv 6349 |
. . . . 5
class (Hom
‘ndx) |
12 | 7, 5 | cfv 6349 |
. . . . . . 7
class
(Base‘𝑚) |
13 | 7, 7, 12 | cotp 4534 |
. . . . . 6
class
〈𝑚, 𝑚, (Base‘𝑚)〉 |
14 | 13 | csn 4526 |
. . . . 5
class
{〈𝑚, 𝑚, (Base‘𝑚)〉} |
15 | 11, 14 | cop 4532 |
. . . 4
class
〈(Hom ‘ndx), {〈𝑚, 𝑚, (Base‘𝑚)〉}〉 |
16 | | cco 16692 |
. . . . . 6
class
comp |
17 | 4, 16 | cfv 6349 |
. . . . 5
class
(comp‘ndx) |
18 | 7, 7, 7 | cotp 4534 |
. . . . . . 7
class
〈𝑚, 𝑚, 𝑚〉 |
19 | | cplusg 16680 |
. . . . . . . 8
class
+g |
20 | 7, 19 | cfv 6349 |
. . . . . . 7
class
(+g‘𝑚) |
21 | 18, 20 | cop 4532 |
. . . . . 6
class
〈〈𝑚, 𝑚, 𝑚〉, (+g‘𝑚)〉 |
22 | 21 | csn 4526 |
. . . . 5
class
{〈〈𝑚,
𝑚, 𝑚〉, (+g‘𝑚)〉} |
23 | 17, 22 | cop 4532 |
. . . 4
class
〈(comp‘ndx), {〈〈𝑚, 𝑚, 𝑚〉, (+g‘𝑚)〉}〉 |
24 | 9, 15, 23 | ctp 4530 |
. . 3
class
{〈(Base‘ndx), {𝑚}〉, 〈(Hom ‘ndx), {〈𝑚, 𝑚, (Base‘𝑚)〉}〉, 〈(comp‘ndx),
{〈〈𝑚, 𝑚, 𝑚〉, (+g‘𝑚)〉}〉} |
25 | 2, 3, 24 | cmpt 5120 |
. 2
class (𝑚 ∈ Mnd ↦
{〈(Base‘ndx), {𝑚}〉, 〈(Hom ‘ndx), {〈𝑚, 𝑚, (Base‘𝑚)〉}〉, 〈(comp‘ndx),
{〈〈𝑚, 𝑚, 𝑚〉, (+g‘𝑚)〉}〉}) |
26 | 1, 25 | wceq 1542 |
1
wff MndToCat =
(𝑚 ∈ Mnd ↦
{〈(Base‘ndx), {𝑚}〉, 〈(Hom ‘ndx), {〈𝑚, 𝑚, (Base‘𝑚)〉}〉, 〈(comp‘ndx),
{〈〈𝑚, 𝑚, 𝑚〉, (+g‘𝑚)〉}〉}) |