P. 187 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18601-18700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	acsmap2d 18601*	In an algebraic closure system, if 𝑆 and 𝑇 have the same closure and 𝑆 is independent, then there is a map 𝑓 from 𝑇 into the set of finite subsets of 𝑆 such that 𝑆 equals the union of ran 𝑓. This is proven by taking the map 𝑓 from acsmapd 18600 and observing that, since 𝑆 and 𝑇 have the same closure, the closure of ∪ ran 𝑓 must contain 𝑆. Since 𝑆 is independent, by mrissmrcd 17686, ∪ ran 𝑓 must equal 𝑆. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ 𝑆 = ∪ ran 𝑓))
Theorem	acsinfd 18602	In an algebraic closure system, if 𝑆 and 𝑇 have the same closure and 𝑆 is infinite independent, then 𝑇 is infinite. This follows from applying unirnffid 9292 to the map given in acsmap2d 18601. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    &   ⊢ (𝜑 → ¬ 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → ¬ 𝑇 ∈ Fin)
Theorem	acsdomd 18603	In an algebraic closure system, if 𝑆 and 𝑇 have the same closure and 𝑆 is infinite independent, then 𝑇 dominates 𝑆. This follows from applying acsinfd 18602 and then applying unirnfdomd 10540 to the map given in acsmap2d 18601. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    &   ⊢ (𝜑 → ¬ 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑆 ≼ 𝑇)
Theorem	acsinfdimd 18604	In an algebraic closure system, if two independent sets have equal closure and one is infinite, then they are equinumerous. This is proven by using acsdomd 18603 twice with acsinfd 18602. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐼)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    &   ⊢ (𝜑 → ¬ 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑆 ≈ 𝑇)
Theorem	acsexdimd 18605*	In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 17696 for the finite case and acsinfdimd 18604 for the infinite case. This is a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐼)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    ⇒   ⊢ (𝜑 → 𝑆 ≈ 𝑇)
Theorem	mrelatglb 18606	Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015.) See mrelatglbALT 49625 for an alternate proof.
⊢ 𝐼 = (toInc‘𝐶)    &   ⊢ 𝐺 = (glb‘𝐼)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅) → (𝐺‘𝑈) = ∩ 𝑈)
Theorem	mrelatglb0 18607	The empty intersection in a Moore space is realized by the base set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐼 = (toInc‘𝐶)    &   ⊢ 𝐺 = (glb‘𝐼)    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐺‘∅) = 𝑋)
Theorem	mrelatlub 18608	Least upper bounds in a Moore space are realized by the closure of the union. (Contributed by Stefan O'Rear, 31-Jan-2015.) See mrelatlubALT 49624 for an alternate proof.
⊢ 𝐼 = (toInc‘𝐶)    &   ⊢ 𝐹 = (mrCls‘𝐶)    &   ⊢ 𝐿 = (lub‘𝐼)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶) → (𝐿‘𝑈) = (𝐹‘∪ 𝑈))
Theorem	mreclatBAD 18609*	A Moore space is a complete lattice under inclusion. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 7357 update): Reprove using isclat 18546 instead of the isclatBAD. hypothesis. See commented-out mreclat above. See mreclat 49626 for a good version.
⊢ 𝐼 = (toInc‘𝐶)    &   ⊢ (𝐼 ∈ CLat ↔ (𝐼 ∈ Poset ∧ ∀𝑥(𝑥 ⊆ (Base‘𝐼) → (((lub‘𝐼)‘𝑥) ∈ (Base‘𝐼) ∧ ((glb‘𝐼)‘𝑥) ∈ (Base‘𝐼)))))    ⇒   ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ CLat)
9.6  Posets, directed sets, and lattices as relations
9.6.1  Posets and lattices as relations See commented-out notes for lattices as relations.
Syntax	cps 18610	Extend class notation with the class of all posets.
class PosetRel
Syntax	ctsr 18611	Extend class notation with the class of all totally ordered sets.
class TosetRel
Definition	df-ps 18612	Define the class of all posets (partially ordered sets) with weak ordering (e.g., "less than or equal to" instead of "less than"). A poset is a relation which is transitive, reflexive, and antisymmetric. (Contributed by NM, 11-May-2008.)
⊢ PosetRel = {𝑟 ∣ (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))}
Definition	df-tsr 18613	Define the class of all totally ordered sets. (Contributed by FL, 1-Nov-2009.)
⊢ TosetRel = {𝑟 ∈ PosetRel ∣ (dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)}
Theorem	isps 18614	The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation. (Contributed by NM, 11-May-2008.)
⊢ (𝑅 ∈ 𝐴 → (𝑅 ∈ PosetRel ↔ (Rel 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅))))
Theorem	psrel 18615	A poset is a relation. (Contributed by NM, 12-May-2008.)
⊢ (𝐴 ∈ PosetRel → Rel 𝐴)
Theorem	psref2 18616	A poset is antisymmetric and reflexive. (Contributed by FL, 3-Aug-2009.)
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅))
Theorem	pstr2 18617	A poset is transitive. (Contributed by FL, 3-Aug-2009.)
⊢ (𝑅 ∈ PosetRel → (𝑅 ∘ 𝑅) ⊆ 𝑅)
Theorem	pslem 18618	Lemma for psref 18620 and others. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝑅 ∈ PosetRel → (((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) ∧ (𝐴 ∈ ∪ ∪ 𝑅 → 𝐴𝑅𝐴) ∧ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵)))
Theorem	psdmrn 18619	The domain and range of a poset equal its field. (Contributed by NM, 13-May-2008.)
⊢ (𝑅 ∈ PosetRel → (dom 𝑅 = ∪ ∪ 𝑅 ∧ ran 𝑅 = ∪ ∪ 𝑅))
Theorem	psref 18620	A poset is reflexive. (Contributed by NM, 13-May-2008.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑋) → 𝐴𝑅𝐴)
Theorem	psrn 18621	The range of a poset equals it domain. (Contributed by NM, 7-Jul-2008.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ PosetRel → 𝑋 = ran 𝑅)
Theorem	psasym 18622	A poset is antisymmetric. (Contributed by NM, 12-May-2008.)
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵)
Theorem	pstr 18623	A poset is transitive. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Theorem	cnvps 18624	The converse of a poset is a poset. In the general case (◡𝑅 ∈ PosetRel → 𝑅 ∈ PosetRel) is not true. See cnvpsb 18625 for a special case where the property holds. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 3-Sep-2015.)
⊢ (𝑅 ∈ PosetRel → ◡𝑅 ∈ PosetRel)
Theorem	cnvpsb 18625	The converse of a poset is a poset. (Contributed by FL, 5-Jan-2009.)
⊢ (Rel 𝑅 → (𝑅 ∈ PosetRel ↔ ◡𝑅 ∈ PosetRel))
Theorem	psss 18626	Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010.)
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel)
Theorem	psssdm2 18627	Field of a subposet. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ PosetRel → dom (𝑅 ∩ (𝐴 × 𝐴)) = (𝑋 ∩ 𝐴))
Theorem	psssdm 18628	Field of a subposet. (Contributed by FL, 19-Sep-2011.) (Revised by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ⊆ 𝑋) → dom (𝑅 ∩ (𝐴 × 𝐴)) = 𝐴)
Theorem	istsr 18629	The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ TosetRel ↔ (𝑅 ∈ PosetRel ∧ (𝑋 × 𝑋) ⊆ (𝑅 ∪ ◡𝑅)))
Theorem	istsr2 18630*	The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ TosetRel ↔ (𝑅 ∈ PosetRel ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)))
Theorem	tsrlin 18631	A toset is a linear order. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ∨ 𝐵𝑅𝐴))
Theorem	tsrlemax 18632	Two ways of saying a number is less than or equal to the maximum of two others. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ TosetRel ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑅if(𝐵𝑅𝐶, 𝐶, 𝐵) ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑅𝐶)))
Theorem	tsrps 18633	A toset is a poset. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (𝑅 ∈ TosetRel → 𝑅 ∈ PosetRel)
Theorem	cnvtsr 18634	The converse of a toset is a toset. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝑅 ∈ TosetRel → ◡𝑅 ∈ TosetRel )
Theorem	tsrss 18635	Any subset of a totally ordered set is totally ordered. (Contributed by FL, 24-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Nov-2013.)
⊢ (𝑅 ∈ TosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ TosetRel )
Theorem	ledm 18636	The domain of ≤ is ℝ*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.)
⊢ ℝ* = dom ≤
Theorem	lern 18637	The range of ≤ is ℝ*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
⊢ ℝ* = ran ≤
Theorem	lefld 18638	The field of the 'less or equal to' relationship on the extended real. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.)
⊢ ℝ* = ∪ ∪ ≤
Theorem	letsr 18639	The "less than or equal to" relationship on the extended reals is a toset. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
⊢ ≤ ∈ TosetRel
9.6.2  Directed sets, nets
Syntax	cdir 18640	Extend class notation with the class of directed sets.
class DirRel
Syntax	ctail 18641	Extend class notation with the tail function for directed sets.
class tail
Definition	df-dir 18642	Define the class of directed sets (the order relation itself is sometimes called a direction, and a directed set is a set equipped with a direction). (Contributed by Jeff Hankins, 25-Nov-2009.)
⊢ DirRel = {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟) ∧ ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)))}
Definition	df-tail 18643*	Define the tail function for directed sets. (Contributed by Jeff Hankins, 25-Nov-2009.)
⊢ tail = (𝑟 ∈ DirRel ↦ (𝑥 ∈ ∪ ∪ 𝑟 ↦ (𝑟 “ {𝑥})))
Theorem	isdir 18644	A condition for a relation to be a direction. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ 𝐴 = ∪ ∪ 𝑅    ⇒   ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ DirRel ↔ ((Rel 𝑅 ∧ ( I ↾ 𝐴) ⊆ 𝑅) ∧ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝐴 × 𝐴) ⊆ (◡𝑅 ∘ 𝑅)))))
Theorem	reldir 18645	A direction is a relation. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ (𝑅 ∈ DirRel → Rel 𝑅)
Theorem	dirdm 18646	A direction's domain is equal to its field. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ (𝑅 ∈ DirRel → dom 𝑅 = ∪ ∪ 𝑅)
Theorem	dirref 18647	A direction is reflexive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ DirRel ∧ 𝐴 ∈ 𝑋) → 𝐴𝑅𝐴)
Theorem	dirtr 18648	A direction is transitive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ (((𝑅 ∈ DirRel ∧ 𝐶 ∈ 𝑉) ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐴𝑅𝐶)
Theorem	dirge 18649*	For any two elements of a directed set, there exists a third element greater than or equal to both. Note that this does not say that the two elements have a least upper bound. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∃𝑥 ∈ 𝑋 (𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))
Theorem	tsrdir 18650	A totally ordered set is a directed set. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ (𝐴 ∈ TosetRel → 𝐴 ∈ DirRel)
9.7  Chains
Syntax	cchn 18651	Extend class notation with the class of (finite) chains.
class ( < Chain 𝐴)
Definition	df-chn 18652*	Define the class of (finite) chains. A chain is defined to be a sequence of objects, where each object is less than the next one in the sequence. The term "chain" is usually used in order theory. In the context of algebra, chains are often called "towers", for example for fields, or "series", for example for subgroup or subnormal series. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ ( < Chain 𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)}
Theorem	ischn 18653*	Property of being a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝐶 ∈ ( < Chain 𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛)))
Theorem	chnwrd 18654	A chain is an ordered sequence, i.e. a word. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    ⇒   ⊢ (𝜑 → 𝐶 ∈ Word 𝐴)
Theorem	chnltm1 18655	Basic property of a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ (dom 𝐶 ∖ {0}))    ⇒   ⊢ (𝜑 → (𝐶‘(𝑁 − 1)) < (𝐶‘𝑁))
Theorem	pfxchn 18656	A prefix of a chain is still a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐿 ∈ (0...(♯‘𝐶)))    ⇒   ⊢ (𝜑 → (𝐶 prefix 𝐿) ∈ ( < Chain 𝐴))
Theorem	nfchnd 18657	Bound-variable hypothesis builder for chain collection constructor. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝜑 → Ⅎ𝑥 < )    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥( < Chain 𝐴))
Theorem	chneq1 18658	Equality theorem for chains. (Contributed by Ender Ting, 17-Jan-2026.)
⊢ ( < = 𝑅 → ( < Chain 𝐴) = (𝑅 Chain 𝐴))
Theorem	chneq2 18659	Equality theorem for chains. (Contributed by Ender Ting, 17-Jan-2026.)
⊢ (𝐴 = 𝐵 → ( < Chain 𝐴) = ( < Chain 𝐵))
Theorem	chneq12 18660	Equality theorem for chains. (Contributed by Ender Ting, 17-Jan-2026.)
⊢ (( < = 𝑅 ∧ 𝐴 = 𝐵) → ( < Chain 𝐴) = (𝑅 Chain 𝐵))
Theorem	chnrss 18661	Chains under a relation are also chains under any superset relation. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ ( < ⊆ 𝑅 → ( < Chain 𝐴) ⊆ (𝑅 Chain 𝐴))
Theorem	chndss 18662	Chains with an alphabet are also chains with any superset alphabet. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝐴 ⊆ 𝐵 → ( < Chain 𝐴) ⊆ ( < Chain 𝐵))
Theorem	chnrdss 18663	Subset theorem for chains. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (( < ⊆ 𝑅 ∧ 𝐴 ⊆ 𝐵) → ( < Chain 𝐴) ⊆ (𝑅 Chain 𝐵))
Theorem	chnexg 18664	Chains with a set given for range form a set. (Contributed by Ender Ting, 21-Nov-2024.) (Revised by Ender Ting, 17-Jan-2026.)
⊢ (𝐴 ∈ 𝑉 → ( < Chain 𝐴) ∈ V)
Theorem	nulchn 18665	Empty set is an increasing chain for every range and every relation. (Contributed by Ender Ting, 19-Nov-2024.) (Revised by Ender Ting, 17-Jan-2026.)
⊢ ∅ ∈ ( < Chain 𝐴)
Theorem	s1chn 18666	A singleton word is always a chain. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ⟨“𝑋”⟩ ∈ ( < Chain 𝐴))
Theorem	chnind 18667*	Induction over a chain. See nnind 12242 for an explanation about the hypotheses. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝑐 = ∅ → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝑑 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑐 = 𝐶 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (((((𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	chnub 18668	In a chain, the last element is an upper bound. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → < Po 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^((♯‘𝐶) − 1)))    ⇒   ⊢ (𝜑 → (𝐶‘𝐼) < (lastS‘𝐶))
Theorem	chnlt 18669	Compare any two elements in a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → < Po 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶)))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^𝐽))    ⇒   ⊢ (𝜑 → (𝐶‘𝐼) < (𝐶‘𝐽))
Theorem	chnso 18670	A chain induces a total order. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → < Or ran 𝐶)
Theorem	chnccats1 18671	Extend a chain with a single element. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑇 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → (𝑇 = ∅ ∨ (lastS‘𝑇) < 𝑋))    ⇒   ⊢ (𝜑 → (𝑇 ++ ⟨“𝑋”⟩) ∈ ( < Chain 𝐴))
Theorem	chnccat 18672	Concatenate two chains. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝜑 → 𝑇 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝑈 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → (𝑇 = ∅ ∨ 𝑈 = ∅ ∨ (lastS‘𝑇) < (𝑈‘0)))    ⇒   ⊢ (𝜑 → (𝑇 ++ 𝑈) ∈ ( < Chain 𝐴))
Theorem	chnrev 18673	Reverse of a chain is chain under the converse relation and same domain. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝐵 ∈ ( < Chain 𝐴) → (reverse‘𝐵) ∈ (◡ < Chain 𝐴))
Theorem	chnflenfi 18674*	There is a finite number of chains with fixed length over finite alphabet. Trivially holds for invalid lengths as there're no matching sequences. (Contributed by Ender Ting, 5-Jan-2025.) (Revised by Ender Ting, 17-Jan-2026.)
⊢ (𝐴 ∈ Fin → {𝑎 ∈ ( < Chain 𝐴) ∣ (♯‘𝑎) = 𝑇} ∈ Fin)
Theorem	chnf 18675	A chain is a zero-based finite sequence with a recoverable upper limit. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝐵 ∈ ( < Chain 𝐴) → 𝐵:(0..^(♯‘𝐵))⟶𝐴)
Theorem	chnpof1 18676	A chain under relation which orders the alphabet is a one-to-one function from its domain to alphabet. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝜑 → < Po 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ( < Chain 𝐴))    ⇒   ⊢ (𝜑 → 𝐵:(0..^(♯‘𝐵))–1-1→𝐴)
Theorem	chnpoadomd 18677	A chain under relation which orders the alphabet cannot have more elements than the alphabet itself. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝜑 → < Po 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (0..^(♯‘𝐵)) ≼ 𝐴)
Theorem	chnpolleha 18678	A chain under relation which orders the alphabet has at most alphabet's size elements in it. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝜑 → < Po 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (♯‘𝐵) ≤ (♯‘𝐴))
Theorem	chnpolfz 18679	Provided that chain's relation is a partial order, the chain length is restricted to a specific integer range. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝜑 → < Po 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → (♯‘𝐵) ∈ (0...(♯‘𝐴)))
Theorem	chnfi 18680	There is a finite number of chains over finite domain, as long as the relation orders it. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ ((𝐴 ∈ Fin ∧ < Po 𝐴) → ( < Chain 𝐴) ∈ Fin)
Theorem	chninf 18681	There is an infinite number of chains for any infinite alphabet and any relation. For instance, all the singletons of alphabet characters match. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝐴 ∉ Fin → ( < Chain 𝐴) ∉ Fin)
Theorem	chnfibg 18682	Given a partial order, the set of chains is finite iff the alphabet is finite. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ ( < Po 𝐴 → (𝐴 ∈ Fin ↔ ( < Chain 𝐴) ∈ Fin))
Theorem	ex-chn1 18683	Example: a doubleton of twos is a valid chain under the identity relation and domain of integers. (Contributed by Ender Ting, 17-Jan-2026.)
⊢ ⟨“22”⟩ ∈ ( I Chain ℤ)
Theorem	ex-chn2 18684	Example: sequence <" ZZ NN QQ "> is a valid chain under the equinumerosity relation in universal domain. (Contributed by Ender Ting, 17-Jan-2026.)
⊢ ⟨“ℤℕℚ”⟩ ∈ ( ≈ Chain V)
PART 10  BASIC ALGEBRAIC STRUCTURES
10.1  Monoids
10.1.1  Magmas According to Wikipedia ("Magma (algebra)", 08-Jan-2020, https://en.wikipedia.org/wiki/magma_(algebra)) "In abstract algebra, a magma [...] is a basic kind of algebraic structure. Specifically, a magma consists of a set equipped with a single binary operation. The binary operation must be closed by definition but no other properties are imposed.". Since the concept of a "binary operation" is used in different variants, these differences are explained in more detail in the following: With df-mpo 7405, binary operations are defined by a rule, and with df-ov 7403, the value of a binary operation applied to two operands can be expressed. In both cases, the two operands can belong to different sets, and the result can be an element of a third set. However, according to Wikipedia "Binary operation", see https://en.wikipedia.org/wiki/Binary_operation 7403 (19-Jan-2020), "... a binary operation on a set 𝑆 is a mapping of the elements of the Cartesian product 𝑆 × 𝑆 to S: 𝑓:𝑆 × 𝑆⟶𝑆. Because the result of performing the operation on a pair of elements of S is again an element of S, the operation is called a closed binary operation on S (or sometimes expressed as having the property of closure).". To distinguish this more restrictive definition (in Wikipedia and most of the literature) from the general case, binary operations mapping the elements of the Cartesian product 𝑆 × 𝑆 are more precisely called internal binary operations. If, in addition, the result is also contained in the set 𝑆, the operation should be called closed internal binary operation. Therefore, a "binary operation on a set 𝑆" according to Wikipedia is a "closed internal binary operation" in a more precise terminology. If the sets are different, the operation is explicitly called external binary operation (see Wikipedia https://en.wikipedia.org/wiki/Binary_operation#External_binary_operations 7403). The definition of magmas (Mgm, see df-mgm 18688) concentrates on the closure property of the associated operation, and poses no additional restrictions on it. In this way, it is most general and flexible.
Syntax	cplusf 18685	Extend class notation with group addition as a function.
class +𝑓
Syntax	cmgm 18686	Extend class notation with class of all magmas.
class Mgm
Definition	df-plusf 18687*	Define group addition function. Usually we will use +g directly instead of +𝑓, and they have the same behavior in most cases. The main advantage of +𝑓 for any magma is that it is a guaranteed function (mgmplusf 18698), while +g only has closure (mgmcl 18691). (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ +𝑓 = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)𝑦)))
Definition	df-mgm 18688*	A magma is a set equipped with an everywhere defined internal operation. Definition 1 in [BourbakiAlg1] p. 1, or definition of a groupoid in section I.1 of [Bruck] p. 1. Note: The term "groupoid" is now widely used to refer to other objects: (small) categories all of whose morphisms are invertible, or groups with a partial function replacing the binary operation. Therefore, we will only use the term "magma" for the present notion in set.mm. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
⊢ Mgm = {𝑔 ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏}
Theorem	ismgm 18689*	The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵))
Theorem	ismgmn0 18690*	The predicate "is a magma" for a structure with a nonempty base set. (Contributed by AV, 29-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝐴 ∈ 𝐵 → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵))
Theorem	mgmcl 18691	Closure of the operation of a magma. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 13-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⚬ 𝑌) ∈ 𝐵)
Theorem	isnmgm 18692	A condition for a structure not to be a magma. (Contributed by AV, 30-Jan-2020.) (Proof shortened by NM, 5-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 ⚬ 𝑌) ∉ 𝐵) → 𝑀 ∉ Mgm)
Theorem	mgmsscl 18693	If the base set of a magma is contained in the base set of another magma, and the group operation of the magma is the restriction of the group operation of the other magma to its base set, then the base set of the magma is closed under the group operation of the other magma. Formerly part of proof of grpissubg 19204. (Contributed by AV, 17-Feb-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = (Base‘𝐻)    ⇒   ⊢ (((𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝑋(+g‘𝐺)𝑌) ∈ 𝑆)
Theorem	plusffval 18694*	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof shortened by AV, 2-Mar-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+𝑓‘𝐺)    ⇒   ⊢ ⨣ = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦))
Theorem	plusfval 18695	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+𝑓‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⨣ 𝑌) = (𝑋 + 𝑌))
Theorem	plusfeq 18696	If the addition operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+𝑓‘𝐺)    ⇒   ⊢ ( + Fn (𝐵 × 𝐵) → ⨣ = + )
Theorem	plusffn 18697	The group addition operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⨣ = (+𝑓‘𝐺)    ⇒   ⊢ ⨣ Fn (𝐵 × 𝐵)
Theorem	mgmplusf 18698	The group addition function of a magma is a function into its base set. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revisd by AV, 28-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⨣ = (+𝑓‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mgm → ⨣ :(𝐵 × 𝐵)⟶𝐵)
Theorem	mgmpropd 18699*	If two structures have the same (nonempty) base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a magma iff the other one is. (Contributed by AV, 25-Feb-2020.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ Mgm ↔ 𝐿 ∈ Mgm))
Theorem	ismgmd 18700*	Deduce a magma from its properties. (Contributed by AV, 25-Feb-2020.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Mgm)