P. 188 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18701-18800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	acsficl 18701	A closure in an algebraic closure system is the union of the closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝐹‘𝑆) = ∪ (𝐹 “ (𝒫 𝑆 ∩ Fin)))
Theorem	isacs5 18702*	A closure system is algebraic iff the closure of a generating set is the union of the closures of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝐹‘𝑠) = ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin))))
Theorem	isacs4 18703*	A closure system is algebraic iff closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝒫 𝑋((toInc‘𝑠) ∈ Dirset → (𝐹‘∪ 𝑠) = ∪ (𝐹 “ 𝑠))))
Theorem	isacs3 18704*	A closure system is algebraic iff directed unions of closed sets are closed. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠 ∈ 𝐶)))
Theorem	acsficld 18705	In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 18701. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑁‘𝑆) = ∪ (𝑁 “ (𝒫 𝑆 ∩ Fin)))
Theorem	acsficl2d 18706*	In an algebraic closure system, an element is in the closure of a set if and only if it is in the closure of a finite subset. Alternate form of acsficl 18701. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑌 ∈ (𝑁‘𝑆) ↔ ∃𝑥 ∈ (𝒫 𝑆 ∩ Fin)𝑌 ∈ (𝑁‘𝑥)))
Theorem	acsfiindd 18707	In an algebraic closure system, a set is independent if and only if all its finite subsets are independent. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ (𝒫 𝑆 ∩ Fin) ⊆ 𝐼))
Theorem	acsmapd 18708*	In an algebraic closure system, if 𝑇 is contained in the closure of 𝑆, there is a map 𝑓 from 𝑇 into the set of finite subsets of 𝑆 such that the closure of ∪ ran 𝑓 contains 𝑇. This is proven by applying acsficl2d 18706 to each element of 𝑇. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑇 ⊆ (𝑁‘𝑆))    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ 𝑇 ⊆ (𝑁‘∪ ran 𝑓)))
Theorem	acsmap2d 18709*	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 18708 and observing that, since 𝑆 and 𝑇 have the same closure, the closure of ∪ ran 𝑓 must contain 𝑆. Since 𝑆 is independent, by mrissmrcd 17794, ∪ 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 18710	In an algebraic closure system, if 𝑆 and 𝑇 have the same closure and 𝑆 is infinite independent, then 𝑇 is infinite. This follows from applying unirnffid 9320 to the map given in acsmap2d 18709. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    &   ⊢ (𝜑 → ¬ 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → ¬ 𝑇 ∈ Fin)
Theorem	acsdomd 18711	In an algebraic closure system, if 𝑆 and 𝑇 have the same closure and 𝑆 is infinite independent, then 𝑇 dominates 𝑆. This follows from applying acsinfd 18710 and then applying unirnfdomd 10633 to the map given in acsmap2d 18709. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    &   ⊢ (𝜑 → ¬ 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑆 ≼ 𝑇)
Theorem	acsinfdimd 18712	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 18711 twice with acsinfd 18710. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐼)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    &   ⊢ (𝜑 → ¬ 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑆 ≈ 𝑇)
Theorem	acsexdimd 18713*	In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 17804 for the finite case and acsinfdimd 18712 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 18714	Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015.) See mrelatglbALT 50048 for an alternate proof.
⊢ 𝐼 = (toInc‘𝐶)    &   ⊢ 𝐺 = (glb‘𝐼)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅) → (𝐺‘𝑈) = ∩ 𝑈)
Theorem	mrelatglb0 18715	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 18716	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 50047 for an alternate proof.
⊢ 𝐼 = (toInc‘𝐶)    &   ⊢ 𝐹 = (mrCls‘𝐶)    &   ⊢ 𝐿 = (lub‘𝐼)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶) → (𝐿‘𝑈) = (𝐹‘∪ 𝑈))
Theorem	mreclatBAD 18717*	A Moore space is a complete lattice under inclusion. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 7369 update): Reprove using isclat 18654 instead of the isclatBAD. hypothesis. See commented-out mreclat above. See mreclat 50049 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 18718	Extend class notation with the class of all posets.
class PosetRel
Syntax	ctsr 18719	Extend class notation with the class of all totally ordered sets.
class TosetRel
Definition	df-ps 18720	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 18721	Define the class of all totally ordered sets. (Contributed by FL, 1-Nov-2009.)
⊢ TosetRel = {𝑟 ∈ PosetRel ∣ (dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)}
Theorem	isps 18722	The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation. (Contributed by NM, 11-May-2008.)
⊢ (𝑅 ∈ 𝐴 → (𝑅 ∈ PosetRel ↔ (Rel 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅))))
Theorem	psrel 18723	A poset is a relation. (Contributed by NM, 12-May-2008.)
⊢ (𝐴 ∈ PosetRel → Rel 𝐴)
Theorem	psref2 18724	A poset is antisymmetric and reflexive. (Contributed by FL, 3-Aug-2009.)
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅))
Theorem	pstr2 18725	A poset is transitive. (Contributed by FL, 3-Aug-2009.)
⊢ (𝑅 ∈ PosetRel → (𝑅 ∘ 𝑅) ⊆ 𝑅)
Theorem	pslem 18726	Lemma for psref 18728 and others. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝑅 ∈ PosetRel → (((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) ∧ (𝐴 ∈ ∪ ∪ 𝑅 → 𝐴𝑅𝐴) ∧ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵)))
Theorem	psdmrn 18727	The domain and range of a poset equal its field. (Contributed by NM, 13-May-2008.)
⊢ (𝑅 ∈ PosetRel → (dom 𝑅 = ∪ ∪ 𝑅 ∧ ran 𝑅 = ∪ ∪ 𝑅))
Theorem	psref 18728	A poset is reflexive. (Contributed by NM, 13-May-2008.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑋) → 𝐴𝑅𝐴)
Theorem	psrn 18729	The range of a poset equals it domain. (Contributed by NM, 7-Jul-2008.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ PosetRel → 𝑋 = ran 𝑅)
Theorem	psasym 18730	A poset is antisymmetric. (Contributed by NM, 12-May-2008.)
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵)
Theorem	pstr 18731	A poset is transitive. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Theorem	cnvps 18732	The converse of a poset is a poset. In the general case (◡𝑅 ∈ PosetRel → 𝑅 ∈ PosetRel) is not true. See cnvpsb 18733 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 18733	The converse of a poset is a poset. (Contributed by FL, 5-Jan-2009.)
⊢ (Rel 𝑅 → (𝑅 ∈ PosetRel ↔ ◡𝑅 ∈ PosetRel))
Theorem	psss 18734	Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010.)
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel)
Theorem	psssdm2 18735	Field of a subposet. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ PosetRel → dom (𝑅 ∩ (𝐴 × 𝐴)) = (𝑋 ∩ 𝐴))
Theorem	psssdm 18736	Field of a subposet. (Contributed by FL, 19-Sep-2011.) (Revised by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ⊆ 𝑋) → dom (𝑅 ∩ (𝐴 × 𝐴)) = 𝐴)
Theorem	istsr 18737	The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ TosetRel ↔ (𝑅 ∈ PosetRel ∧ (𝑋 × 𝑋) ⊆ (𝑅 ∪ ◡𝑅)))
Theorem	istsr2 18738*	The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ TosetRel ↔ (𝑅 ∈ PosetRel ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)))
Theorem	tsrlin 18739	A toset is a linear order. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ∨ 𝐵𝑅𝐴))
Theorem	tsrlemax 18740	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 18741	A toset is a poset. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (𝑅 ∈ TosetRel → 𝑅 ∈ PosetRel)
Theorem	cnvtsr 18742	The converse of a toset is a toset. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝑅 ∈ TosetRel → ◡𝑅 ∈ TosetRel )
Theorem	tsrss 18743	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 18744	The domain of ≤ is ℝ*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.)
⊢ ℝ* = dom ≤
Theorem	lern 18745	The range of ≤ is ℝ*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
⊢ ℝ* = ran ≤
Theorem	lefld 18746	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 18747	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 18748	Extend class notation with the class of directed sets.
class DirRel
Syntax	ctail 18749	Extend class notation with the tail function for directed sets.
class tail
Definition	df-dir 18750	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 18751*	Define the tail function for directed sets. (Contributed by Jeff Hankins, 25-Nov-2009.)
⊢ tail = (𝑟 ∈ DirRel ↦ (𝑥 ∈ ∪ ∪ 𝑟 ↦ (𝑟 “ {𝑥})))
Theorem	isdir 18752	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 18753	A direction is a relation. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ (𝑅 ∈ DirRel → Rel 𝑅)
Theorem	dirdm 18754	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 18755	A direction is reflexive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ DirRel ∧ 𝐴 ∈ 𝑋) → 𝐴𝑅𝐴)
Theorem	dirtr 18756	A direction is transitive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ (((𝑅 ∈ DirRel ∧ 𝐶 ∈ 𝑉) ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐴𝑅𝐶)
Theorem	dirge 18757*	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 18758	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 18759	Extend class notation with the class of (finite) chains.
class ( < Chain 𝐴)
Definition	df-chn 18760*	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 18761*	Property of being a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝐶 ∈ ( < Chain 𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛)))
Theorem	chnwrd 18762	A chain is an ordered sequence, i.e. a word. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    ⇒   ⊢ (𝜑 → 𝐶 ∈ Word 𝐴)
Theorem	chnltm1 18763	Basic property of a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ (dom 𝐶 ∖ {0}))    ⇒   ⊢ (𝜑 → (𝐶‘(𝑁 − 1)) < (𝐶‘𝑁))
Theorem	pfxchn 18764	A prefix of a chain is still a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐿 ∈ (0...(♯‘𝐶)))    ⇒   ⊢ (𝜑 → (𝐶 prefix 𝐿) ∈ ( < Chain 𝐴))
Theorem	nfchnd 18765	Bound-variable hypothesis builder for chain collection constructor. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝜑 → Ⅎ𝑥 < )    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥( < Chain 𝐴))
Theorem	chneq1 18766	Equality theorem for chains. (Contributed by Ender Ting, 17-Jan-2026.)
⊢ ( < = 𝑅 → ( < Chain 𝐴) = (𝑅 Chain 𝐴))
Theorem	chneq2 18767	Equality theorem for chains. (Contributed by Ender Ting, 17-Jan-2026.)
⊢ (𝐴 = 𝐵 → ( < Chain 𝐴) = ( < Chain 𝐵))
Theorem	chneq12 18768	Equality theorem for chains. (Contributed by Ender Ting, 17-Jan-2026.)
⊢ (( < = 𝑅 ∧ 𝐴 = 𝐵) → ( < Chain 𝐴) = (𝑅 Chain 𝐵))
Theorem	chnrss 18769	Chains under a relation are also chains under any superset relation. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ ( < ⊆ 𝑅 → ( < Chain 𝐴) ⊆ (𝑅 Chain 𝐴))
Theorem	chndss 18770	Chains with an alphabet are also chains with any superset alphabet. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝐴 ⊆ 𝐵 → ( < Chain 𝐴) ⊆ ( < Chain 𝐵))
Theorem	chnrdss 18771	Subset theorem for chains. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (( < ⊆ 𝑅 ∧ 𝐴 ⊆ 𝐵) → ( < Chain 𝐴) ⊆ (𝑅 Chain 𝐵))
Theorem	chnexg 18772	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 18773	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 18774	A singleton word is always a chain. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ⟨“𝑋”⟩ ∈ ( < Chain 𝐴))
Theorem	chnind 18775*	Induction over a chain. See nnind 12334 for an explanation about the hypotheses. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝑐 = ∅ → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝑑 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑐 = 𝐶 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (((((𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	chnub 18776	In a chain, the last element is an upper bound. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → < Po 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^((♯‘𝐶) − 1)))    ⇒   ⊢ (𝜑 → (𝐶‘𝐼) < (lastS‘𝐶))
Theorem	chnlt 18777	Compare any two elements in a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → < Po 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶)))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^𝐽))    ⇒   ⊢ (𝜑 → (𝐶‘𝐼) < (𝐶‘𝐽))
Theorem	chnso 18778	A chain induces a total order. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → < Or ran 𝐶)
Theorem	chnccats1 18779	Extend a chain with a single element. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑇 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → (𝑇 = ∅ ∨ (lastS‘𝑇) < 𝑋))    ⇒   ⊢ (𝜑 → (𝑇 ++ ⟨“𝑋”⟩) ∈ ( < Chain 𝐴))
Theorem	chnccat 18780	Concatenate two chains. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝜑 → 𝑇 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝑈 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → (𝑇 = ∅ ∨ 𝑈 = ∅ ∨ (lastS‘𝑇) < (𝑈‘0)))    ⇒   ⊢ (𝜑 → (𝑇 ++ 𝑈) ∈ ( < Chain 𝐴))
Theorem	chnrev 18781	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 18782*	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 18783	A chain is a zero-based finite sequence with a recoverable upper limit. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝐵 ∈ ( < Chain 𝐴) → 𝐵:(0..^(♯‘𝐵))⟶𝐴)
Theorem	chnpof1 18784	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 18785	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 18786	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 18787	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 18788	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 18789	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 18790	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 18791	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 18792	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 7417, binary operations are defined by a rule, and with df-ov 7415, 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 7415 (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 7415). The definition of magmas (Mgm, see df-mgm 18796) 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 18793	Extend class notation with group addition as a function.
class +𝑓
Syntax	cmgm 18794	Extend class notation with class of all magmas.
class Mgm
Definition	df-plusf 18795*	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 18806), while +g only has closure (mgmcl 18799). (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ +𝑓 = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)𝑦)))
Definition	df-mgm 18796*	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 18797*	The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵))
Theorem	ismgmn0 18798*	The predicate "is a magma" for a structure with a nonempty base set. (Contributed by AV, 29-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝐴 ∈ 𝐵 → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵))
Theorem	mgmcl 18799	Closure of the operation of a magma. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 13-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⚬ 𝑌) ∈ 𝐵)
Theorem	isnmgm 18800	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)