Step | Hyp | Ref
| Expression |
1 | | mndtcbas.c |
. 2
⊢ (𝜑 → 𝐶 = (MndToCat‘𝑀)) |
2 | | mndtcbas.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ Mnd) |
3 | | sneq 4574 |
. . . . . 6
⊢ (𝑚 = 𝑀 → {𝑚} = {𝑀}) |
4 | 3 | opeq2d 4813 |
. . . . 5
⊢ (𝑚 = 𝑀 → 〈(Base‘ndx), {𝑚}〉 =
〈(Base‘ndx), {𝑀}〉) |
5 | | id 22 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → 𝑚 = 𝑀) |
6 | | fveq2 6792 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀)) |
7 | 5, 5, 6 | oteq123d 4821 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → 〈𝑚, 𝑚, (Base‘𝑚)〉 = 〈𝑀, 𝑀, (Base‘𝑀)〉) |
8 | 7 | sneqd 4576 |
. . . . . 6
⊢ (𝑚 = 𝑀 → {〈𝑚, 𝑚, (Base‘𝑚)〉} = {〈𝑀, 𝑀, (Base‘𝑀)〉}) |
9 | 8 | opeq2d 4813 |
. . . . 5
⊢ (𝑚 = 𝑀 → 〈(Hom ‘ndx), {〈𝑚, 𝑚, (Base‘𝑚)〉}〉 = 〈(Hom ‘ndx),
{〈𝑀, 𝑀, (Base‘𝑀)〉}〉) |
10 | 5, 5, 5 | oteq123d 4821 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → 〈𝑚, 𝑚, 𝑚〉 = 〈𝑀, 𝑀, 𝑀〉) |
11 | | fveq2 6792 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (+g‘𝑚) = (+g‘𝑀)) |
12 | 10, 11 | opeq12d 4814 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → 〈〈𝑚, 𝑚, 𝑚〉, (+g‘𝑚)〉 = 〈〈𝑀, 𝑀, 𝑀〉, (+g‘𝑀)〉) |
13 | 12 | sneqd 4576 |
. . . . . 6
⊢ (𝑚 = 𝑀 → {〈〈𝑚, 𝑚, 𝑚〉, (+g‘𝑚)〉} = {〈〈𝑀, 𝑀, 𝑀〉, (+g‘𝑀)〉}) |
14 | 13 | opeq2d 4813 |
. . . . 5
⊢ (𝑚 = 𝑀 → 〈(comp‘ndx),
{〈〈𝑚, 𝑚, 𝑚〉, (+g‘𝑚)〉}〉 =
〈(comp‘ndx), {〈〈𝑀, 𝑀, 𝑀〉, (+g‘𝑀)〉}〉) |
15 | 4, 9, 14 | tpeq123d 4687 |
. . . 4
⊢ (𝑚 = 𝑀 → {〈(Base‘ndx), {𝑚}〉, 〈(Hom ‘ndx),
{〈𝑚, 𝑚, (Base‘𝑚)〉}〉, 〈(comp‘ndx),
{〈〈𝑚, 𝑚, 𝑚〉, (+g‘𝑚)〉}〉} =
{〈(Base‘ndx), {𝑀}〉, 〈(Hom ‘ndx),
{〈𝑀, 𝑀, (Base‘𝑀)〉}〉, 〈(comp‘ndx),
{〈〈𝑀, 𝑀, 𝑀〉, (+g‘𝑀)〉}〉}) |
16 | | df-mndtc 46405 |
. . . 4
⊢ MndToCat
= (𝑚 ∈ Mnd ↦
{〈(Base‘ndx), {𝑚}〉, 〈(Hom ‘ndx), {〈𝑚, 𝑚, (Base‘𝑚)〉}〉, 〈(comp‘ndx),
{〈〈𝑚, 𝑚, 𝑚〉, (+g‘𝑚)〉}〉}) |
17 | | tpex 7617 |
. . . 4
⊢
{〈(Base‘ndx), {𝑀}〉, 〈(Hom ‘ndx),
{〈𝑀, 𝑀, (Base‘𝑀)〉}〉, 〈(comp‘ndx),
{〈〈𝑀, 𝑀, 𝑀〉, (+g‘𝑀)〉}〉} ∈
V |
18 | 15, 16, 17 | fvmpt 6895 |
. . 3
⊢ (𝑀 ∈ Mnd →
(MndToCat‘𝑀) =
{〈(Base‘ndx), {𝑀}〉, 〈(Hom ‘ndx),
{〈𝑀, 𝑀, (Base‘𝑀)〉}〉, 〈(comp‘ndx),
{〈〈𝑀, 𝑀, 𝑀〉, (+g‘𝑀)〉}〉}) |
19 | 2, 18 | syl 17 |
. 2
⊢ (𝜑 → (MndToCat‘𝑀) = {〈(Base‘ndx),
{𝑀}〉, 〈(Hom
‘ndx), {〈𝑀,
𝑀, (Base‘𝑀)〉}〉,
〈(comp‘ndx), {〈〈𝑀, 𝑀, 𝑀〉, (+g‘𝑀)〉}〉}) |
20 | 1, 19 | eqtrd 2773 |
1
⊢ (𝜑 → 𝐶 = {〈(Base‘ndx), {𝑀}〉, 〈(Hom ‘ndx),
{〈𝑀, 𝑀, (Base‘𝑀)〉}〉, 〈(comp‘ndx),
{〈〈𝑀, 𝑀, 𝑀〉, (+g‘𝑀)〉}〉}) |