Users' Mathboxes Mathbox for Zhi Wang < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mndtcval Structured version   Visualization version   GIF version

Theorem mndtcval 46406
Description: Value of the category built from a monoid. (Contributed by Zhi Wang, 22-Sep-2024.) (New usage is discouraged.)
Hypotheses
Ref Expression
mndtcbas.c (𝜑𝐶 = (MndToCat‘𝑀))
mndtcbas.m (𝜑𝑀 ∈ Mnd)
Assertion
Ref Expression
mndtcval (𝜑𝐶 = {⟨(Base‘ndx), {𝑀}⟩, ⟨(Hom ‘ndx), {⟨𝑀, 𝑀, (Base‘𝑀)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑀, 𝑀, 𝑀⟩, (+g𝑀)⟩}⟩})

Proof of Theorem mndtcval
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 mndtcbas.c . 2 (𝜑𝐶 = (MndToCat‘𝑀))
2 mndtcbas.m . . 3 (𝜑𝑀 ∈ Mnd)
3 sneq 4574 . . . . . 6 (𝑚 = 𝑀 → {𝑚} = {𝑀})
43opeq2d 4813 . . . . 5 (𝑚 = 𝑀 → ⟨(Base‘ndx), {𝑚}⟩ = ⟨(Base‘ndx), {𝑀}⟩)
5 id 22 . . . . . . . 8 (𝑚 = 𝑀𝑚 = 𝑀)
6 fveq2 6792 . . . . . . . 8 (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀))
75, 5, 6oteq123d 4821 . . . . . . 7 (𝑚 = 𝑀 → ⟨𝑚, 𝑚, (Base‘𝑚)⟩ = ⟨𝑀, 𝑀, (Base‘𝑀)⟩)
87sneqd 4576 . . . . . 6 (𝑚 = 𝑀 → {⟨𝑚, 𝑚, (Base‘𝑚)⟩} = {⟨𝑀, 𝑀, (Base‘𝑀)⟩})
98opeq2d 4813 . . . . 5 (𝑚 = 𝑀 → ⟨(Hom ‘ndx), {⟨𝑚, 𝑚, (Base‘𝑚)⟩}⟩ = ⟨(Hom ‘ndx), {⟨𝑀, 𝑀, (Base‘𝑀)⟩}⟩)
105, 5, 5oteq123d 4821 . . . . . . . 8 (𝑚 = 𝑀 → ⟨𝑚, 𝑚, 𝑚⟩ = ⟨𝑀, 𝑀, 𝑀⟩)
11 fveq2 6792 . . . . . . . 8 (𝑚 = 𝑀 → (+g𝑚) = (+g𝑀))
1210, 11opeq12d 4814 . . . . . . 7 (𝑚 = 𝑀 → ⟨⟨𝑚, 𝑚, 𝑚⟩, (+g𝑚)⟩ = ⟨⟨𝑀, 𝑀, 𝑀⟩, (+g𝑀)⟩)
1312sneqd 4576 . . . . . 6 (𝑚 = 𝑀 → {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g𝑚)⟩} = {⟨⟨𝑀, 𝑀, 𝑀⟩, (+g𝑀)⟩})
1413opeq2d 4813 . . . . 5 (𝑚 = 𝑀 → ⟨(comp‘ndx), {⟨⟨𝑚, 𝑚, 𝑚⟩, (+g𝑚)⟩}⟩ = ⟨(comp‘ndx), {⟨⟨𝑀, 𝑀, 𝑀⟩, (+g𝑀)⟩}⟩)
154, 9, 14tpeq123d 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
1815, 16, 17fvmpt 6895 . . 3 (𝑀 ∈ Mnd → (MndToCat‘𝑀) = {⟨(Base‘ndx), {𝑀}⟩, ⟨(Hom ‘ndx), {⟨𝑀, 𝑀, (Base‘𝑀)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑀, 𝑀, 𝑀⟩, (+g𝑀)⟩}⟩})
192, 18syl 17 . 2 (𝜑 → (MndToCat‘𝑀) = {⟨(Base‘ndx), {𝑀}⟩, ⟨(Hom ‘ndx), {⟨𝑀, 𝑀, (Base‘𝑀)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑀, 𝑀, 𝑀⟩, (+g𝑀)⟩}⟩})
201, 19eqtrd 2773 1 (𝜑𝐶 = {⟨(Base‘ndx), {𝑀}⟩, ⟨(Hom ‘ndx), {⟨𝑀, 𝑀, (Base‘𝑀)⟩}⟩, ⟨(comp‘ndx), {⟨⟨𝑀, 𝑀, 𝑀⟩, (+g𝑀)⟩}⟩})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  wcel 2101  {csn 4564  {ctp 4568  cop 4570  cotp 4572  cfv 6447  ndxcnx 16922  Basecbs 16940  +gcplusg 16990  Hom chom 17001  compcco 17002  Mndcmnd 18413  MndToCatcmndtc 46404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-10 2132  ax-11 2149  ax-12 2166  ax-ext 2704  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7608
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2063  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2884  df-ral 3060  df-rex 3069  df-rab 3224  df-v 3436  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4260  df-if 4463  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-ot 4573  df-uni 4842  df-br 5078  df-opab 5140  df-mpt 5161  df-id 5491  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-iota 6399  df-fun 6449  df-fv 6455  df-mndtc 46405
This theorem is referenced by:  mndtcbasval  46407  mndtchom  46411  mndtcco  46412
  Copyright terms: Public domain W3C validator