P. 191 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19001-19100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gsumccatsn 19001	Homomorphic property of composites with a singleton. (Contributed by AV, 20-Jan-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ ⟨“𝑍”⟩)) = ((𝐺 Σg 𝑊) + 𝑍))
Theorem	gsumspl 19002	The primary purpose of the splice construction is to enable local rewrites. Thus, in any monoidal valuation, if a splice does not cause a local change it does not cause a global change. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝑆 ∈ Word 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (0...𝑇))    &   ⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆)))    &   ⊢ (𝜑 → 𝑋 ∈ Word 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ Word 𝐵)    &   ⊢ (𝜑 → (𝑀 Σg 𝑋) = (𝑀 Σg 𝑌))    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑆 splice ⟨𝐹, 𝑇, 𝑋⟩)) = (𝑀 Σg (𝑆 splice ⟨𝐹, 𝑇, 𝑌⟩)))
Theorem	gsumwmhm 19003	Behavior of homomorphisms on finite monoidal sums. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊)))
Theorem	gsumwspan 19004*	The submonoid generated by a set of elements is precisely the set of elements which can be expressed as finite products of the generator. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝐾 = (mrCls‘(SubMnd‘𝑀))    ⇒   ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) = ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))
10.1.9  Free monoids
Syntax	cfrmd 19005	Extend class definition with the free monoid construction.
class freeMnd
Syntax	cvrmd 19006	Extend class notation with free monoid injection.
class varFMnd
Definition	df-frmd 19007	Define a free monoid over a set 𝑖 of generators, defined as the set of finite strings on 𝐼 with the operation of concatenation. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ freeMnd = (𝑖 ∈ V ↦ {⟨(Base‘ndx), Word 𝑖⟩, ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩})
Definition	df-vrmd 19008*	Define a free monoid over a set 𝑖 of generators, defined as the set of finite strings on 𝐼 with the operation of concatenation. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ varFMnd = (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ ⟨“𝑗”⟩))
Theorem	frmdval 19009	Value of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ (𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼)    &   ⊢ + = ( ++ ↾ (𝐵 × 𝐵))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩})
Theorem	frmdbas 19010	The base set of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼)
Theorem	frmdelbas 19011	An element of the base set of a free monoid is a string on the generators. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ Word 𝐼)
Theorem	frmdplusg 19012	The monoid operation of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) (Proof shortened by AV, 6-Nov-2024.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ + = ( ++ ↾ (𝐵 × 𝐵))
Theorem	frmdadd 19013	Value of the monoid operation of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ++ 𝑌))
Theorem	vrmdfval 19014*	The canonical injection from the generating set 𝐼 to the base set of the free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑈 = (𝑗 ∈ 𝐼 ↦ ⟨“𝑗”⟩))
Theorem	vrmdval 19015	The value of the generating elements of a free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑈‘𝐴) = ⟨“𝐴”⟩)
Theorem	vrmdf 19016	The mapping from the index set to the generators is a function into the free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑈:𝐼⟶Word 𝐼)
Theorem	frmdmnd 19017	A free monoid is a monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd)
Theorem	frmd0 19018	The identity of the free monoid is the empty word. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    ⇒   ⊢ ∅ = (0g‘𝑀)
Theorem	frmdsssubm 19019	The set of words taking values in a subset is a (free) submonoid of the free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼) → Word 𝐽 ∈ (SubMnd‘𝑀))
Theorem	frmdgsum 19020	Any word in a free monoid can be expressed as the sum of the singletons composing it. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝐼) → (𝑀 Σg (𝑈 ∘ 𝑊)) = 𝑊)
Theorem	frmdss2 19021	A subset of generators is contained in a submonoid iff the set of words on the generators is in the submonoid. This can be viewed as an elementary way of saying "the monoidal closure of 𝐽 is Word 𝐽". (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ (SubMnd‘𝑀)) → ((𝑈 “ 𝐽) ⊆ 𝐴 ↔ Word 𝐽 ⊆ 𝐴))
Theorem	frmdup1 19022*	Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐸 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥)))    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴:𝐼⟶𝐵)    ⇒   ⊢ (𝜑 → 𝐸 ∈ (𝑀 MndHom 𝐺))
Theorem	frmdup2 19023*	The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐸 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥)))    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴:𝐼⟶𝐵)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝐸‘(𝑈‘𝑌)) = (𝐴‘𝑌))
Theorem	frmdup3lem 19024*	Lemma for frmdup3 19025. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ (((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) → 𝐹 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥))))
Theorem	frmdup3 19025*	Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) → ∃!𝑚 ∈ (𝑀 MndHom 𝐺)(𝑚 ∘ 𝑈) = 𝐴)
10.1.9.1  Monoid of endofunctions According to Wikipedia ("Endomorphism", 25-Jan-2024, https://en.wikipedia.org/wiki/Endomorphism) "An endofunction is a function whose domain is equal to its codomain.". An endofunction is sometimes also called "self-mapping" (see https://www.wikidata.org/wiki/Q1691962) or "self-map" (see https://mathworld.wolfram.com/Self-Map.html), in German "Selbstabbildung" (see https://de.wikipedia.org/wiki/Selbstabbildung).
Syntax	cefmnd 19026	Extend class notation to include the class of monoids of endofunctions.
class EndoFMnd
Definition	df-efmnd 19027*	Define the monoid of endofunctions on set 𝑥. We represent the monoid as the set of functions from 𝑥 to itself ((𝑥 ↑m 𝑥)) under function composition, and topologize it as a function space assuming the set is discrete. Analogous to the former definition of SymGrp, see df-symg 19546 and symgvalstruct 19573. (Contributed by AV, 25-Jan-2024.)
⊢ EndoFMnd = (𝑥 ∈ V ↦ ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
Theorem	efmnd 19028*	The monoid of endofunctions on set 𝐴. (Contributed by AV, 25-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (𝐴 ↑m 𝐴)    &   ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔))    &   ⊢ 𝐽 = (∏t‘(𝐴 × {𝒫 𝐴}))    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
Theorem	efmndbas 19029	The base set of the monoid of endofunctions on class 𝐴. (Contributed by AV, 25-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝐵 = (𝐴 ↑m 𝐴)
Theorem	efmndbasabf 19030*	The base set of the monoid of endofunctions on class 𝐴 is the set of functions from 𝐴 into itself. (Contributed by AV, 29-Mar-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝐵 = {𝑓 ∣ 𝑓:𝐴⟶𝐴}
Theorem	elefmndbas 19031	Two ways of saying a function is a mapping of 𝐴 to itself. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐴))
Theorem	elefmndbas2 19032	Two ways of saying a function is a mapping of 𝐴 to itself. (Contributed by AV, 27-Jan-2024.) (Proof shortened by AV, 29-Mar-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐴))
Theorem	efmndbasf 19033	Elements in the monoid of endofunctions on 𝐴 are functions from 𝐴 into itself. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴⟶𝐴)
Theorem	efmndhash 19034	The monoid of endofunctions on 𝑛 objects has cardinality 𝑛↑𝑛. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → (♯‘𝐵) = ((♯‘𝐴)↑(♯‘𝐴)))
Theorem	efmndbasfi 19035	The monoid of endofunctions on a finite set 𝐴 is finite. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → 𝐵 ∈ Fin)
Theorem	efmndfv 19036	The function value of an endofunction. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ 𝐴)
Theorem	efmndtset 19037	The topology of the monoid of endofunctions on 𝐴. This component is defined on a larger set than the true base - the product topology is defined on the set of all functions, not just endofunctions - but the definition of TopOpen ensures that it is trimmed down before it gets use. (Contributed by AV, 25-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∏t‘(𝐴 × {𝒫 𝐴})) = (TopSet‘𝐺))
Theorem	efmndplusg 19038*	The group operation of a monoid of endofunctions is the function composition. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔))
Theorem	efmndov 19039	The value of the group operation of the monoid of endofunctions on 𝐴. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))
Theorem	efmndcl 19040	The group operation of the monoid of endofunctions on 𝐴 is closed. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	efmndtopn 19041	The topology of the monoid of endofunctions on 𝐴. (Contributed by AV, 31-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑉 → ((∏t‘(𝑋 × {𝒫 𝑋})) ↾t 𝐵) = (TopOpen‘𝐺))
Theorem	symggrplem 19042*	Lemma for symggrp 19576 and efmndsgrp 19044. Conditions for an operation to be associative. Formerly part of proof for symggrp 19576. (Contributed by AV, 28-Jan-2024.)
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑥 ∘ 𝑦))    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	efmndmgm 19043	The monoid of endofunctions on a class 𝐴 is a magma. (Contributed by AV, 28-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ 𝐺 ∈ Mgm
Theorem	efmndsgrp 19044	The monoid of endofunctions on a class 𝐴 is a semigroup. (Contributed by AV, 28-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ 𝐺 ∈ Smgrp
Theorem	ielefmnd 19045	The identity function restricted to a set 𝐴 is an element of the base set of the monoid of endofunctions on 𝐴. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ (Base‘𝐺))
Theorem	efmndid 19046	The identity function restricted to a set 𝐴 is the identity element of the monoid of endofunctions on 𝐴. (Contributed by AV, 25-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) = (0g‘𝐺))
Theorem	efmndmnd 19047	The monoid of endofunctions on a set 𝐴 is actually a monoid. (Contributed by AV, 31-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Mnd)
Theorem	efmnd0nmnd 19048	Even the monoid of endofunctions on the empty set is actually a monoid. (Contributed by AV, 31-Jan-2024.)
⊢ (EndoFMnd‘∅) ∈ Mnd
Theorem	efmndbas0 19049	The base set of the monoid of endofunctions on the empty set is the singleton containing the empty set. (Contributed by AV, 27-Jan-2024.) (Proof shortened by AV, 31-Mar-2024.)
⊢ (Base‘(EndoFMnd‘∅)) = {∅}
Theorem	efmnd1hash 19050	The monoid of endofunctions on a singleton has cardinality 1. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (♯‘𝐵) = 1)
Theorem	efmnd1bas 19051	The monoid of endofunctions on a singleton consists of the identity only. (Contributed by AV, 31-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼}    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐵 = {{⟨𝐼, 𝐼⟩}})
Theorem	efmnd2hash 19052	The monoid of endofunctions on a (proper) pair has cardinality 4. (Contributed by AV, 18-Feb-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼, 𝐽}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 4)
Theorem	submefmnd 19053*	If the base set of a monoid is contained in the base set of the monoid of endofunctions on a set 𝐴, contains the identity function and has the function composition as group operation, then its base set is a submonoid of the monoid of endofunctions on set 𝐴. Analogous to pgrpsubgsymg 19585. (Contributed by AV, 17-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ 𝐹 = (Base‘𝑆)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (((𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹) ∧ (+g‘𝑆) = (𝑓 ∈ 𝐹, 𝑔 ∈ 𝐹 ↦ (𝑓 ∘ 𝑔))) → 𝐹 ∈ (SubMnd‘𝑀)))
Theorem	sursubmefmnd 19054*	The set of surjective endofunctions on a set 𝐴 is a submonoid of the monoid of endofunctions on 𝐴. (Contributed by AV, 25-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → {ℎ ∣ ℎ:𝐴–onto→𝐴} ∈ (SubMnd‘𝑀))
Theorem	injsubmefmnd 19055*	The set of injective endofunctions on a set 𝐴 is a submonoid of the monoid of endofunctions on 𝐴. (Contributed by AV, 25-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → {ℎ ∣ ℎ:𝐴–1-1→𝐴} ∈ (SubMnd‘𝑀))
Theorem	idressubmefmnd 19056	The singleton containing only the identity function restricted to a set is a submonoid of the monoid of endofunctions on this set. (Contributed by AV, 17-Feb-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → {( I ↾ 𝐴)} ∈ (SubMnd‘𝐺))
Theorem	idresefmnd 19057	The structure with the singleton containing only the identity function restricted to a set 𝐴 as base set and the function composition as group operation, constructed by (structure) restricting the monoid of endofunctions on 𝐴 to that singleton, is a monoid whose base set is a subset of the base set of the monoid of endofunctions on 𝐴. (Contributed by AV, 17-Feb-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐸 = (𝐺 ↾s {( I ↾ 𝐴)})    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐸 ∈ Mnd ∧ (Base‘𝐸) ⊆ (Base‘𝐺)))
Theorem	smndex1ibas 19058	The modulo function 𝐼 is an endofunction on ℕ0. (Contributed by AV, 12-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    ⇒   ⊢ 𝐼 ∈ (Base‘𝑀)
Theorem	smndex1iidm 19059*	The modulo function 𝐼 is idempotent. (Contributed by AV, 12-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    ⇒   ⊢ (𝐼 ∘ 𝐼) = 𝐼
Theorem	smndex1gbas 19060*	The constant functions (𝐺‘𝐾) are endofunctions on ℕ0. (Contributed by AV, 12-Feb-2024.) Avoid ax-rep 5231 and shorten proof. (Revised by GG, 2-Apr-2026.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    ⇒   ⊢ (𝐾 ∈ (0..^𝑁) → (𝐺‘𝐾) ∈ (Base‘𝑀))
Theorem	smndex1gbasOLD 19061*	Obsolete version of smndex1gbas 19060 as of 2-Apr-2026. (Contributed by AV, 12-Feb-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    ⇒   ⊢ (𝐾 ∈ (0..^𝑁) → (𝐺‘𝐾) ∈ (Base‘𝑀))
Theorem	smndex1gid 19062*	The composition of a constant function (𝐺‘𝐾) with another endofunction on ℕ0 results in (𝐺‘𝐾) itself. (Contributed by AV, 14-Feb-2024.) Avoid ax-rep 5231. (Revised by GG, 2-Apr-2026.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    ⇒   ⊢ ((𝐹 ∈ (Base‘𝑀) ∧ 𝐾 ∈ (0..^𝑁)) → ((𝐺‘𝐾) ∘ 𝐹) = (𝐺‘𝐾))
Theorem	smndex1gidOLD 19063*	Obsolete version of smndex1gid 19062 as of 2-Apr-2026. (Contributed by AV, 14-Feb-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    ⇒   ⊢ ((𝐹 ∈ (Base‘𝑀) ∧ 𝐾 ∈ (0..^𝑁)) → ((𝐺‘𝐾) ∘ 𝐹) = (𝐺‘𝐾))
Theorem	smndex1igid 19064*	The composition of the modulo function 𝐼 and a constant function (𝐺‘𝐾) results in (𝐺‘𝐾) itself. (Contributed by AV, 14-Feb-2024.) Avoid ax-rep 5231. (Revised by GG, 2-Apr-2026.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    ⇒   ⊢ (𝐾 ∈ (0..^𝑁) → (𝐼 ∘ (𝐺‘𝐾)) = (𝐺‘𝐾))
Theorem	smndex1igidOLD 19065*	Obsolete version of smndex1igid 19064 as of 2-Apr-2026. (Contributed by AV, 14-Feb-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    ⇒   ⊢ (𝐾 ∈ (0..^𝑁) → (𝐼 ∘ (𝐺‘𝐾)) = (𝐺‘𝐾))
Theorem	smndex1basss 19066*	The modulo function 𝐼 and the constant functions (𝐺‘𝐾) are endofunctions on ℕ0. (Contributed by AV, 12-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    ⇒   ⊢ 𝐵 ⊆ (Base‘𝑀)
Theorem	smndex1bas 19067*	The base set of the monoid of endofunctions on ℕ0 restricted to the modulo function 𝐼 and the constant functions (𝐺‘𝐾). (Contributed by AV, 12-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ (Base‘𝑆) = 𝐵
Theorem	smndex1mgm 19068*	The monoid of endofunctions on ℕ0 restricted to the modulo function 𝐼 and the constant functions (𝐺‘𝐾) is a magma. (Contributed by AV, 14-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ 𝑆 ∈ Mgm
Theorem	smndex1sgrp 19069*	The monoid of endofunctions on ℕ0 restricted to the modulo function 𝐼 and the constant functions (𝐺‘𝐾) is a semigroup. (Contributed by AV, 14-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ 𝑆 ∈ Smgrp
Theorem	smndex1mndlem 19070*	Lemma for smndex1mnd 19071 and smndex1id 19072. (Contributed by AV, 16-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ (𝑋 ∈ 𝐵 → ((𝐼 ∘ 𝑋) = 𝑋 ∧ (𝑋 ∘ 𝐼) = 𝑋))
Theorem	smndex1mnd 19071*	The monoid of endofunctions on ℕ0 restricted to the modulo function 𝐼 and the constant functions (𝐺‘𝐾) is a monoid. (Contributed by AV, 16-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ 𝑆 ∈ Mnd
Theorem	smndex1id 19072*	The modulo function 𝐼 is the identity of the monoid of endofunctions on ℕ0 restricted to the modulo function 𝐼 and the constant functions (𝐺‘𝐾). (Contributed by AV, 16-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ 𝐼 = (0g‘𝑆)
Theorem	smndex1n0mnd 19073*	The identity of the monoid 𝑀 of endofunctions on set ℕ0 is not contained in the base set of the constructed monoid 𝑆. (Contributed by AV, 17-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ (0g‘𝑀) ∉ 𝐵
Theorem	nsmndex1 19074*	The base set 𝐵 of the constructed monoid 𝑆 is not a submonoid of the monoid 𝑀 of endofunctions on set ℕ0, although 𝑀 ∈ Mnd and 𝑆 ∈ Mnd and 𝐵 ⊆ (Base‘𝑀) hold. (Contributed by AV, 17-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ 𝐵 ∉ (SubMnd‘𝑀)
Theorem	smndex2dbas 19075	The doubling function 𝐷 is an endofunction on ℕ0. (Contributed by AV, 18-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ 𝐷 = (𝑥 ∈ ℕ0 ↦ (2 · 𝑥))    ⇒   ⊢ 𝐷 ∈ 𝐵
Theorem	smndex2dnrinv 19076	The doubling function 𝐷 has no right inverse in the monoid of endofunctions on ℕ0. (Contributed by AV, 18-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ 𝐷 = (𝑥 ∈ ℕ0 ↦ (2 · 𝑥))    ⇒   ⊢ ∀𝑓 ∈ 𝐵 (𝐷 ∘ 𝑓) ≠ 0
Theorem	smndex2hbas 19077	The halving functions 𝐻 are endofunctions on ℕ0. (Contributed by AV, 18-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ 𝐷 = (𝑥 ∈ ℕ0 ↦ (2 · 𝑥))    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝐻 = (𝑥 ∈ ℕ0 ↦ if(2 ∥ 𝑥, (𝑥 / 2), 𝑁))    ⇒   ⊢ 𝐻 ∈ 𝐵
Theorem	smndex2dlinvh 19078*	The halving functions 𝐻 are left inverses of the doubling function 𝐷. (Contributed by AV, 18-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ 𝐷 = (𝑥 ∈ ℕ0 ↦ (2 · 𝑥))    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝐻 = (𝑥 ∈ ℕ0 ↦ if(2 ∥ 𝑥, (𝑥 / 2), 𝑁))    ⇒   ⊢ (𝐻 ∘ 𝐷) = 0
10.1.10  Examples and counterexamples for magmas, semigroups and monoids
Theorem	mgm2nsgrplem1 19079*	Lemma 1 for mgm2nsgrp 19083: 𝑀 is a magma, even if 𝐴 = 𝐵 (𝑀 is the trivial magma in this case, see mgmb1mgm1 18795). (Contributed by AV, 27-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝑀 ∈ Mgm)
Theorem	mgm2nsgrplem2 19080*	Lemma 2 for mgm2nsgrp 19083. (Contributed by AV, 27-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴))    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ⚬ 𝐴) ⚬ 𝐵) = 𝐴)
Theorem	mgm2nsgrplem3 19081*	Lemma 3 for mgm2nsgrp 19083. (Contributed by AV, 28-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴))    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⚬ (𝐴 ⚬ 𝐵)) = 𝐵)
Theorem	mgm2nsgrplem4 19082*	Lemma 4 for mgm2nsgrp 19083: M is not a semigroup. (Contributed by AV, 28-Jan-2020.) (Proof shortened by AV, 31-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴))    ⇒   ⊢ ((♯‘𝑆) = 2 → 𝑀 ∉ Smgrp)
Theorem	mgm2nsgrp 19083*	A small magma (with two elements) which is not a semigroup. (Contributed by AV, 28-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴))    ⇒   ⊢ ((♯‘𝑆) = 2 → (𝑀 ∈ Mgm ∧ 𝑀 ∉ Smgrp))
Theorem	sgrp2nmndlem1 19084*	Lemma 1 for sgrp2nmnd 19091: 𝑀 is a magma, even if 𝐴 = 𝐵 (𝑀 is the trivial magma in this case, see mgmb1mgm1 18795). (Contributed by AV, 29-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝑀 ∈ Mgm)
Theorem	sgrp2nmndlem2 19085*	Lemma 2 for sgrp2nmnd 19091. (Contributed by AV, 29-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴 ⚬ 𝐶) = 𝐴)
Theorem	sgrp2nmndlem3 19086*	Lemma 3 for sgrp2nmnd 19091. (Contributed by AV, 29-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐵 ⚬ 𝐶) = 𝐵)
Theorem	sgrp2rid2 19087*	A small semigroup (with two elements) with two right identities which are different if 𝐴 ≠ 𝐵. (Contributed by AV, 10-Feb-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑦 ⚬ 𝑥) = 𝑦)
Theorem	sgrp2rid2ex 19088*	A small semigroup (with two elements) with two right identities which are different. (Contributed by AV, 10-Feb-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((♯‘𝑆) = 2 → ∃𝑥 ∈ 𝑆 ∃𝑧 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ≠ 𝑧 ∧ (𝑦 ⚬ 𝑥) = 𝑦 ∧ (𝑦 ⚬ 𝑧) = 𝑦))
Theorem	sgrp2nmndlem4 19089*	Lemma 4 for sgrp2nmnd 19091: M is a semigroup. (Contributed by AV, 29-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    ⇒   ⊢ ((♯‘𝑆) = 2 → 𝑀 ∈ Smgrp)
Theorem	sgrp2nmndlem5 19090*	Lemma 5 for sgrp2nmnd 19091: M is not a monoid. (Contributed by AV, 29-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    ⇒   ⊢ ((♯‘𝑆) = 2 → 𝑀 ∉ Mnd)
Theorem	sgrp2nmnd 19091*	A small semigroup (with two elements) which is not a monoid. (Contributed by AV, 26-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    ⇒   ⊢ ((♯‘𝑆) = 2 → (𝑀 ∈ Smgrp ∧ 𝑀 ∉ Mnd))
Theorem	mgmnsgrpex 19092	There is a magma which is not a semigroup. (Contributed by AV, 29-Jan-2020.)
⊢ ∃𝑚 ∈ Mgm 𝑚 ∉ Smgrp
Theorem	sgrpnmndex 19093	There is a semigroup which is not a monoid. (Contributed by AV, 29-Jan-2020.)
⊢ ∃𝑚 ∈ Smgrp 𝑚 ∉ Mnd
Theorem	sgrpssmgm 19094	The class of all semigroups is a proper subclass of the class of all magmas. (Contributed by AV, 29-Jan-2020.)
⊢ Smgrp ⊊ Mgm
Theorem	mndsssgrp 19095	The class of all monoids is a proper subclass of the class of all semigroups. (Contributed by AV, 29-Jan-2020.)
⊢ Mnd ⊊ Smgrp
Theorem	degenmgmopdm 19096	The domain of the operation of a degenerate magma. (Contributed by AV, 18-Aug-2026.)
⊢ 𝑀 = {⟨(Base‘ndx), {∅, 1o}⟩, ⟨(+g‘ndx), {⟨⟨1o, 1o⟩, 1o⟩, ⟨⟨1o, 2o⟩, 1o⟩, ⟨⟨1o, ∅⟩, 1o⟩}⟩}    ⇒   ⊢ dom (+g‘𝑀) = ({1o} × {∅, 1o, 2o})
Theorem	degenmgmbas 19097	The base set of a degenerate magma. (Contributed by AV, 21-Aug-2026.)
⊢ 𝑀 = {⟨(Base‘ndx), {∅, 1o}⟩, ⟨(+g‘ndx), {⟨⟨1o, 1o⟩, 1o⟩, ⟨⟨1o, 2o⟩, 1o⟩, ⟨⟨1o, ∅⟩, 1o⟩}⟩}    &   ⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ 𝐵 = {∅, 1o}
Theorem	degenmgmnfn 19098	The operation of a degenerate magma is not a function on its base set. (Contributed by AV, 21-Aug-2026.)
⊢ 𝑀 = {⟨(Base‘ndx), {∅, 1o}⟩, ⟨(+g‘ndx), {⟨⟨1o, 1o⟩, 1o⟩, ⟨⟨1o, 2o⟩, 1o⟩, ⟨⟨1o, ∅⟩, 1o⟩}⟩}    &   ⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ ¬ (+g‘𝑀) Fn (𝐵 × 𝐵)
Theorem	degenmgm 19099	A degenerate magma: although the operation is not defined for all pairs of elements of the base set ((∅(+g‘𝑀)1o) and (∅(+g‘𝑀)∅) are not defined, and therefore are ∅ by definition, which is contained in the base set), and its domain is not (a subset of) the base set (2o is in the domain of the operation, but not in the base set) , the structure 𝑀 is still a magma according to our definition. (Contributed by AV, 18-Aug-2026.)
⊢ 𝑀 = {⟨(Base‘ndx), {∅, 1o}⟩, ⟨(+g‘ndx), {⟨⟨1o, 1o⟩, 1o⟩, ⟨⟨1o, 2o⟩, 1o⟩, ⟨⟨1o, ∅⟩, 1o⟩}⟩}    ⇒   ⊢ 𝑀 ∈ Mgm
Theorem	degenmgm2opdm 19100	The domain of the operation of a second degenerate magma. (Contributed by AV, 21-Aug-2026.)
⊢ 𝑀 = {⟨(Base‘ndx), {∅, 1o}⟩, ⟨(+g‘ndx), {⟨⟨1o, 1o⟩, 1o⟩, ⟨⟨1o, 2o⟩, 1o⟩, ⟨⟨1o, 2o⟩, 2o⟩}⟩}    ⇒   ⊢ dom (+g‘𝑀) = ({1o} × {1o, 2o})