P. 186 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18501-18600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isipodrs 18501*	Condition for a family of sets to be directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ((toInc‘𝐴) ∈ Dirset ↔ (𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧))
Theorem	ipodrscl 18502	Direction by inclusion as used here implies sethood. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ((toInc‘𝐴) ∈ Dirset → 𝐴 ∈ V)
Theorem	ipodrsfi 18503*	Finite upper bound property for directed collections of sets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ (((toInc‘𝐴) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → ∃𝑧 ∈ 𝐴 ∪ 𝑋 ⊆ 𝑧)
Theorem	fpwipodrs 18504	The finite subsets of any set are directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → (toInc‘(𝒫 𝐴 ∩ Fin)) ∈ Dirset)
Theorem	ipodrsima 18505*	The monotone image of a directed set. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ (𝜑 → 𝐹 Fn 𝒫 𝐴)    &   ⊢ ((𝜑 ∧ (𝑢 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝐴)) → (𝐹‘𝑢) ⊆ (𝐹‘𝑣))    &   ⊢ (𝜑 → (toInc‘𝐵) ∈ Dirset)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝒫 𝐴)    &   ⊢ (𝜑 → (𝐹 “ 𝐵) ∈ 𝑉)    ⇒   ⊢ (𝜑 → (toInc‘(𝐹 “ 𝐵)) ∈ Dirset)
Theorem	isacs3lem 18506*	An algebraic closure system satisfies isacs3 18514. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠 ∈ 𝐶)))
Theorem	acsdrsel 18507	An algebraic closure system contains all directed unions of closed sets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑌 ⊆ 𝐶 ∧ (toInc‘𝑌) ∈ Dirset) → ∪ 𝑌 ∈ 𝐶)
Theorem	isacs4lem 18508*	In a closure system in which directed unions of closed sets are closed, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠 ∈ 𝐶)) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫 𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) = ∪ (𝐹 “ 𝑡))))
Theorem	isacs5lem 18509*	If closure commutes with directed unions, then the closure of a set is the closure of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫 𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) = ∪ (𝐹 “ 𝑡))) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝐹‘𝑠) = ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin))))
Theorem	acsdrscl 18510	In an algebraic closure system, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑌 ⊆ 𝒫 𝑋 ∧ (toInc‘𝑌) ∈ Dirset) → (𝐹‘∪ 𝑌) = ∪ (𝐹 “ 𝑌))
Theorem	acsficl 18511	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 18512*	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 18513*	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 18514*	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 18515	In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 18511. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑁‘𝑆) = ∪ (𝑁 “ (𝒫 𝑆 ∩ Fin)))
Theorem	acsficl2d 18516*	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 18511. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑌 ∈ (𝑁‘𝑆) ↔ ∃𝑥 ∈ (𝒫 𝑆 ∩ Fin)𝑌 ∈ (𝑁‘𝑥)))
Theorem	acsfiindd 18517	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 18518*	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 18516 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 18519*	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 18518 and observing that, since 𝑆 and 𝑇 have the same closure, the closure of ∪ ran 𝑓 must contain 𝑆. Since 𝑆 is independent, by mrissmrcd 17604, ∪ 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 18520	In an algebraic closure system, if 𝑆 and 𝑇 have the same closure and 𝑆 is infinite independent, then 𝑇 is infinite. This follows from applying unirnffid 9254 to the map given in acsmap2d 18519. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    &   ⊢ (𝜑 → ¬ 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → ¬ 𝑇 ∈ Fin)
Theorem	acsdomd 18521	In an algebraic closure system, if 𝑆 and 𝑇 have the same closure and 𝑆 is infinite independent, then 𝑇 dominates 𝑆. This follows from applying acsinfd 18520 and then applying unirnfdomd 10488 to the map given in acsmap2d 18519. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    &   ⊢ (𝜑 → ¬ 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑆 ≼ 𝑇)
Theorem	acsinfdimd 18522	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 18521 twice with acsinfd 18520. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐼)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    &   ⊢ (𝜑 → ¬ 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑆 ≈ 𝑇)
Theorem	acsexdimd 18523*	In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 17614 for the finite case and acsinfdimd 18522 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 18524	Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015.) See mrelatglbALT 49487 for an alternate proof.
⊢ 𝐼 = (toInc‘𝐶)    &   ⊢ 𝐺 = (glb‘𝐼)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅) → (𝐺‘𝑈) = ∩ 𝑈)
Theorem	mrelatglb0 18525	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 18526	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 49486 for an alternate proof.
⊢ 𝐼 = (toInc‘𝐶)    &   ⊢ 𝐹 = (mrCls‘𝐶)    &   ⊢ 𝐿 = (lub‘𝐼)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶) → (𝐿‘𝑈) = (𝐹‘∪ 𝑈))
Theorem	mreclatBAD 18527*	A Moore space is a complete lattice under inclusion. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 7320 update): Reprove using isclat 18464 instead of the isclatBAD. hypothesis. See commented-out mreclat above. See mreclat 49488 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 18528	Extend class notation with the class of all posets.
class PosetRel
Syntax	ctsr 18529	Extend class notation with the class of all totally ordered sets.
class TosetRel
Definition	df-ps 18530	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 18531	Define the class of all totally ordered sets. (Contributed by FL, 1-Nov-2009.)
⊢ TosetRel = {𝑟 ∈ PosetRel ∣ (dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)}
Theorem	isps 18532	The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation. (Contributed by NM, 11-May-2008.)
⊢ (𝑅 ∈ 𝐴 → (𝑅 ∈ PosetRel ↔ (Rel 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅))))
Theorem	psrel 18533	A poset is a relation. (Contributed by NM, 12-May-2008.)
⊢ (𝐴 ∈ PosetRel → Rel 𝐴)
Theorem	psref2 18534	A poset is antisymmetric and reflexive. (Contributed by FL, 3-Aug-2009.)
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅))
Theorem	pstr2 18535	A poset is transitive. (Contributed by FL, 3-Aug-2009.)
⊢ (𝑅 ∈ PosetRel → (𝑅 ∘ 𝑅) ⊆ 𝑅)
Theorem	pslem 18536	Lemma for psref 18538 and others. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝑅 ∈ PosetRel → (((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) ∧ (𝐴 ∈ ∪ ∪ 𝑅 → 𝐴𝑅𝐴) ∧ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵)))
Theorem	psdmrn 18537	The domain and range of a poset equal its field. (Contributed by NM, 13-May-2008.)
⊢ (𝑅 ∈ PosetRel → (dom 𝑅 = ∪ ∪ 𝑅 ∧ ran 𝑅 = ∪ ∪ 𝑅))
Theorem	psref 18538	A poset is reflexive. (Contributed by NM, 13-May-2008.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑋) → 𝐴𝑅𝐴)
Theorem	psrn 18539	The range of a poset equals it domain. (Contributed by NM, 7-Jul-2008.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ PosetRel → 𝑋 = ran 𝑅)
Theorem	psasym 18540	A poset is antisymmetric. (Contributed by NM, 12-May-2008.)
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵)
Theorem	pstr 18541	A poset is transitive. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Theorem	cnvps 18542	The converse of a poset is a poset. In the general case (◡𝑅 ∈ PosetRel → 𝑅 ∈ PosetRel) is not true. See cnvpsb 18543 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 18543	The converse of a poset is a poset. (Contributed by FL, 5-Jan-2009.)
⊢ (Rel 𝑅 → (𝑅 ∈ PosetRel ↔ ◡𝑅 ∈ PosetRel))
Theorem	psss 18544	Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010.)
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel)
Theorem	psssdm2 18545	Field of a subposet. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ PosetRel → dom (𝑅 ∩ (𝐴 × 𝐴)) = (𝑋 ∩ 𝐴))
Theorem	psssdm 18546	Field of a subposet. (Contributed by FL, 19-Sep-2011.) (Revised by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ⊆ 𝑋) → dom (𝑅 ∩ (𝐴 × 𝐴)) = 𝐴)
Theorem	istsr 18547	The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ TosetRel ↔ (𝑅 ∈ PosetRel ∧ (𝑋 × 𝑋) ⊆ (𝑅 ∪ ◡𝑅)))
Theorem	istsr2 18548*	The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ TosetRel ↔ (𝑅 ∈ PosetRel ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)))
Theorem	tsrlin 18549	A toset is a linear order. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ∨ 𝐵𝑅𝐴))
Theorem	tsrlemax 18550	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 18551	A toset is a poset. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (𝑅 ∈ TosetRel → 𝑅 ∈ PosetRel)
Theorem	cnvtsr 18552	The converse of a toset is a toset. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝑅 ∈ TosetRel → ◡𝑅 ∈ TosetRel )
Theorem	tsrss 18553	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 18554	The domain of ≤ is ℝ*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.)
⊢ ℝ* = dom ≤
Theorem	lern 18555	The range of ≤ is ℝ*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
⊢ ℝ* = ran ≤
Theorem	lefld 18556	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 18557	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 18558	Extend class notation with the class of directed sets.
class DirRel
Syntax	ctail 18559	Extend class notation with the tail function for directed sets.
class tail
Definition	df-dir 18560	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 18561*	Define the tail function for directed sets. (Contributed by Jeff Hankins, 25-Nov-2009.)
⊢ tail = (𝑟 ∈ DirRel ↦ (𝑥 ∈ ∪ ∪ 𝑟 ↦ (𝑟 “ {𝑥})))
Theorem	isdir 18562	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 18563	A direction is a relation. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ (𝑅 ∈ DirRel → Rel 𝑅)
Theorem	dirdm 18564	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 18565	A direction is reflexive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ DirRel ∧ 𝐴 ∈ 𝑋) → 𝐴𝑅𝐴)
Theorem	dirtr 18566	A direction is transitive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ (((𝑅 ∈ DirRel ∧ 𝐶 ∈ 𝑉) ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐴𝑅𝐶)
Theorem	dirge 18567*	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 18568	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 18569	Extend class notation with the class of (finite) chains.
class ( < Chain 𝐴)
Definition	df-chn 18570*	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 18571*	Property of being a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝐶 ∈ ( < Chain 𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛)))
Theorem	chnwrd 18572	A chain is an ordered sequence, i.e. a word. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    ⇒   ⊢ (𝜑 → 𝐶 ∈ Word 𝐴)
Theorem	chnltm1 18573	Basic property of a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ (dom 𝐶 ∖ {0}))    ⇒   ⊢ (𝜑 → (𝐶‘(𝑁 − 1)) < (𝐶‘𝑁))
Theorem	pfxchn 18574	A prefix of a chain is still a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐿 ∈ (0...(♯‘𝐶)))    ⇒   ⊢ (𝜑 → (𝐶 prefix 𝐿) ∈ ( < Chain 𝐴))
Theorem	nfchnd 18575	Bound-variable hypothesis builder for chain collection constructor. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝜑 → Ⅎ𝑥 < )    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    ⇒   ⊢ (𝜑 → Ⅎ𝑥( < Chain 𝐴))
Theorem	chneq1 18576	Equality theorem for chains. (Contributed by Ender Ting, 17-Jan-2026.)
⊢ ( < = 𝑅 → ( < Chain 𝐴) = (𝑅 Chain 𝐴))
Theorem	chneq2 18577	Equality theorem for chains. (Contributed by Ender Ting, 17-Jan-2026.)
⊢ (𝐴 = 𝐵 → ( < Chain 𝐴) = ( < Chain 𝐵))
Theorem	chneq12 18578	Equality theorem for chains. (Contributed by Ender Ting, 17-Jan-2026.)
⊢ (( < = 𝑅 ∧ 𝐴 = 𝐵) → ( < Chain 𝐴) = (𝑅 Chain 𝐵))
Theorem	chnrss 18579	Chains under a relation are also chains under any superset relation. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ ( < ⊆ 𝑅 → ( < Chain 𝐴) ⊆ (𝑅 Chain 𝐴))
Theorem	chndss 18580	Chains with an alphabet are also chains with any superset alphabet. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝐴 ⊆ 𝐵 → ( < Chain 𝐴) ⊆ ( < Chain 𝐵))
Theorem	chnrdss 18581	Subset theorem for chains. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (( < ⊆ 𝑅 ∧ 𝐴 ⊆ 𝐵) → ( < Chain 𝐴) ⊆ (𝑅 Chain 𝐵))
Theorem	chnexg 18582	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 18583	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 18584	A singleton word is always a chain. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ⟨“𝑋”⟩ ∈ ( < Chain 𝐴))
Theorem	chnind 18585*	Induction over a chain. See nnind 12190 for an explanation about the hypotheses. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝑐 = ∅ → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝑑 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑐 = 𝐶 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (((((𝜑 ∧ 𝑑 ∈ ( < Chain 𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	chnub 18586	In a chain, the last element is an upper bound. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → < Po 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^((♯‘𝐶) − 1)))    ⇒   ⊢ (𝜑 → (𝐶‘𝐼) < (lastS‘𝐶))
Theorem	chnlt 18587	Compare any two elements in a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (𝜑 → < Po 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶)))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^𝐽))    ⇒   ⊢ (𝜑 → (𝐶‘𝐼) < (𝐶‘𝐽))
Theorem	chnso 18588	A chain induces a total order. (Contributed by Thierry Arnoux, 19-Jun-2025.)
⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain 𝐴)) → < Or ran 𝐶)
Theorem	chnccats1 18589	Extend a chain with a single element. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑇 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → (𝑇 = ∅ ∨ (lastS‘𝑇) < 𝑋))    ⇒   ⊢ (𝜑 → (𝑇 ++ ⟨“𝑋”⟩) ∈ ( < Chain 𝐴))
Theorem	chnccat 18590	Concatenate two chains. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝜑 → 𝑇 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝑈 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → (𝑇 = ∅ ∨ 𝑈 = ∅ ∨ (lastS‘𝑇) < (𝑈‘0)))    ⇒   ⊢ (𝜑 → (𝑇 ++ 𝑈) ∈ ( < Chain 𝐴))
Theorem	chnrev 18591	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 18592*	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 18593	A chain is a zero-based finite sequence with a recoverable upper limit. (Contributed by Ender Ting, 20-Jan-2026.)
⊢ (𝐵 ∈ ( < Chain 𝐴) → 𝐵:(0..^(♯‘𝐵))⟶𝐴)
Theorem	chnpof1 18594	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 18595	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 18596	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 18597	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 18598	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 18599	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 18600	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))