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	latdisd 18501*	In a lattice, joins distribute over meets if and only if meets distribute over joins; the distributive property is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝐾 ∈ Lat → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∨ (𝑦 ∧ 𝑧)) = ((𝑥 ∨ 𝑦) ∧ (𝑥 ∨ 𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧))))
9.5.2  Complete lattices
Syntax	ccla 18502	Extend class notation with complete lattices.
class CLat
Definition	df-clat 18503	Define the class of all complete lattices, where every subset of the base set has an LUB and a GLB. (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.)
⊢ CLat = {𝑝 ∈ Poset ∣ (dom (lub‘𝑝) = 𝒫 (Base‘𝑝) ∧ dom (glb‘𝑝) = 𝒫 (Base‘𝑝))}
Theorem	isclat 18504	The predicate "is a complete lattice". (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ (𝐾 ∈ CLat ↔ (𝐾 ∈ Poset ∧ (dom 𝑈 = 𝒫 𝐵 ∧ dom 𝐺 = 𝒫 𝐵)))
Theorem	clatpos 18505	A complete lattice is a poset. (Contributed by NM, 8-Sep-2018.)
⊢ (𝐾 ∈ CLat → 𝐾 ∈ Poset)
Theorem	clatlem 18506	Lemma for properties of a complete lattice. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → ((𝑈‘𝑆) ∈ 𝐵 ∧ (𝐺‘𝑆) ∈ 𝐵))
Theorem	clatlubcl 18507	Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝑈‘𝑆) ∈ 𝐵)
Theorem	clatlubcl2 18508	Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → 𝑆 ∈ dom 𝑈)
Theorem	clatglbcl 18509	Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵)
Theorem	clatglbcl2 18510	Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → 𝑆 ∈ dom 𝐺)
Theorem	oduclatb 18511	Being a complete lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    ⇒   ⊢ (𝑂 ∈ CLat ↔ 𝐷 ∈ CLat)
Theorem	clatl 18512	A complete lattice is a lattice. (Contributed by NM, 18-Sep-2011.) TODO: use eqrelrdv2 5756 to shorten proof and eliminate joindmss 18381 and meetdmss 18395?
⊢ (𝐾 ∈ CLat → 𝐾 ∈ Lat)
Theorem	isglbd 18513*	Properties that determine the greatest lower bound of a complete lattice. (Contributed by Mario Carneiro, 19-Mar-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝐻 ≤ 𝑦)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → 𝑥 ≤ 𝐻)    &   ⊢ (𝜑 → 𝐾 ∈ CLat)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐻 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) = 𝐻)
Theorem	lublem 18514*	Lemma for the least upper bound properties in a complete lattice. (Contributed by NM, 19-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (∀𝑦 ∈ 𝑆 𝑦 ≤ (𝑈‘𝑆) ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → (𝑈‘𝑆) ≤ 𝑧)))
Theorem	lubub 18515	The LUB of a complete lattice subset is an upper bound. (Contributed by NM, 19-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆) → 𝑋 ≤ (𝑈‘𝑆))
Theorem	lubl 18516*	The LUB of a complete lattice subset is the least bound. (Contributed by NM, 19-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝐵) → (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 → (𝑈‘𝑆) ≤ 𝑋))
Theorem	lubss 18517	Subset law for least upper bounds. (chsupss 31480 analog.) (Contributed by NM, 20-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇) → (𝑈‘𝑆) ≤ (𝑈‘𝑇))
Theorem	lubel 18518	An element of a set is less than or equal to the least upper bound of the set. (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝑆 ∧ 𝑆 ⊆ 𝐵) → 𝑋 ≤ (𝑈‘𝑆))
Theorem	lubun 18519	The LUB of a union. (Contributed by NM, 5-Mar-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑈‘(𝑆 ∪ 𝑇)) = ((𝑈‘𝑆) ∨ (𝑈‘𝑇)))
Theorem	clatglb 18520*	Properties of greatest lower bound of a complete lattice. (Contributed by NM, 5-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (∀𝑦 ∈ 𝑆 (𝐺‘𝑆) ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ (𝐺‘𝑆))))
Theorem	clatglble 18521	The greatest lower bound is the least element. (Contributed by NM, 5-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑋)
Theorem	clatleglb 18522*	Two ways of expressing "less than or equal to the greatest lower bound." (Contributed by NM, 5-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → (𝑋 ≤ (𝐺‘𝑆) ↔ ∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦))
Theorem	clatglbss 18523	Subset law for greatest lower bound. (Contributed by Mario Carneiro, 16-Apr-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇) → (𝐺‘𝑇) ≤ (𝐺‘𝑆))
9.5.3  Distributive lattices
Syntax	cdlat 18524	The class of distributive lattices.
class DLat
Definition	df-dlat 18525*	A distributive lattice is a lattice in which meets distribute over joins, or equivalently (latdisd 18501) joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ DLat = {𝑘 ∈ Lat ∣ [(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))}
Theorem	isdlat 18526*	Property of being a distributive lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝐾 ∈ DLat ↔ (𝐾 ∈ Lat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧))))
Theorem	dlatmjdi 18527	In a distributive lattice, meets distribute over joins. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ DLat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍)))
Theorem	dlatl 18528	A distributive lattice is a lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ (𝐾 ∈ DLat → 𝐾 ∈ Lat)
Theorem	odudlatb 18529	The dual of a distributive lattice is a distributive lattice and conversely. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐷 = (ODual‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → (𝐾 ∈ DLat ↔ 𝐷 ∈ DLat))
Theorem	dlatjmdi 18530	In a distributive lattice, joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ DLat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ 𝑍)))
9.5.4  Subset order structures
Syntax	cipo 18531	Class function defining inclusion posets.
class toInc
Definition	df-ipo 18532*	For any family of sets, define the poset of that family ordered by inclusion. See ipobas 18535, ipolerval 18536, and ipole 18538 for its contract. EDITORIAL: I'm not thrilled with the name. Any suggestions? (Contributed by Stefan O'Rear, 30-Jan-2015.) (New usage is discouraged.)
⊢ toInc = (𝑓 ∈ V ↦ ⦋{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦)} / 𝑜⦌({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})⟩}))
Theorem	ipostr 18533	The structure of df-ipo 18532 is a structure defining indices up to 11. (Contributed by Mario Carneiro, 25-Oct-2015.)
⊢ ({⟨(Base‘ndx), 𝐵⟩, ⟨(TopSet‘ndx), 𝐽⟩} ∪ {⟨(le‘ndx), ≤ ⟩, ⟨(oc‘ndx), ⊥ ⟩}) Struct ⟨1, ;11⟩
Theorem	ipoval 18534*	Value of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ ≤ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦)}    ⇒   ⊢ (𝐹 ∈ 𝑉 → 𝐼 = ({⟨(Base‘ndx), 𝐹⟩, ⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩} ∪ {⟨(le‘ndx), ≤ ⟩, ⟨(oc‘ndx), (𝑥 ∈ 𝐹 ↦ ∪ {𝑦 ∈ 𝐹 ∣ (𝑦 ∩ 𝑥) = ∅})⟩}))
Theorem	ipobas 18535	Base set of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by Mario Carneiro, 25-Oct-2015.)
⊢ 𝐼 = (toInc‘𝐹)    ⇒   ⊢ (𝐹 ∈ 𝑉 → 𝐹 = (Base‘𝐼))
Theorem	ipolerval 18536*	Relation of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐼 = (toInc‘𝐹)    ⇒   ⊢ (𝐹 ∈ 𝑉 → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦)} = (le‘𝐼))
Theorem	ipotset 18537	Topology of the inclusion poset. (Contributed by Mario Carneiro, 24-Oct-2015.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ ≤ = (le‘𝐼)    ⇒   ⊢ (𝐹 ∈ 𝑉 → (ordTop‘ ≤ ) = (TopSet‘𝐼))
Theorem	ipole 18538	Weak order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ ≤ = (le‘𝐼)    ⇒   ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑋 ≤ 𝑌 ↔ 𝑋 ⊆ 𝑌))
Theorem	ipolt 18539	Strict order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐼 = (toInc‘𝐹)    &   ⊢ < = (lt‘𝐼)    ⇒   ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑋 < 𝑌 ↔ 𝑋 ⊊ 𝑌))
Theorem	ipopos 18540	The inclusion poset on a family of sets is actually a poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
⊢ 𝐼 = (toInc‘𝐹)    ⇒   ⊢ 𝐼 ∈ Poset
Theorem	isipodrs 18541*	Condition for a family of sets to be directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ((toInc‘𝐴) ∈ Dirset ↔ (𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧))
Theorem	ipodrscl 18542	Direction by inclusion as used here implies sethood. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ((toInc‘𝐴) ∈ Dirset → 𝐴 ∈ V)
Theorem	ipodrsfi 18543*	Finite upper bound property for directed collections of sets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ (((toInc‘𝐴) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → ∃𝑧 ∈ 𝐴 ∪ 𝑋 ⊆ 𝑧)
Theorem	fpwipodrs 18544	The finite subsets of any set are directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → (toInc‘(𝒫 𝐴 ∩ Fin)) ∈ Dirset)
Theorem	ipodrsima 18545*	The monotone image of a directed set. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ (𝜑 → 𝐹 Fn 𝒫 𝐴)    &   ⊢ ((𝜑 ∧ (𝑢 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝐴)) → (𝐹‘𝑢) ⊆ (𝐹‘𝑣))    &   ⊢ (𝜑 → (toInc‘𝐵) ∈ Dirset)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝒫 𝐴)    &   ⊢ (𝜑 → (𝐹 “ 𝐵) ∈ 𝑉)    ⇒   ⊢ (𝜑 → (toInc‘(𝐹 “ 𝐵)) ∈ Dirset)
Theorem	isacs3lem 18546*	An algebraic closure system satisfies isacs3 18554. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠 ∈ 𝐶)))
Theorem	acsdrsel 18547	An algebraic closure system contains all directed unions of closed sets. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑌 ⊆ 𝐶 ∧ (toInc‘𝑌) ∈ Dirset) → ∪ 𝑌 ∈ 𝐶)
Theorem	isacs4lem 18548*	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 18549*	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 18550	In an algebraic closure system, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.)
⊢ 𝐹 = (mrCls‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑌 ⊆ 𝒫 𝑋 ∧ (toInc‘𝑌) ∈ Dirset) → (𝐹‘∪ 𝑌) = ∪ (𝐹 “ 𝑌))
Theorem	acsficl 18551	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 18552*	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 18553*	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 18554*	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 18555	In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 18551. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑁‘𝑆) = ∪ (𝑁 “ (𝒫 𝑆 ∩ Fin)))
Theorem	acsficl2d 18556*	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 18551. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑌 ∈ (𝑁‘𝑆) ↔ ∃𝑥 ∈ (𝒫 𝑆 ∩ Fin)𝑌 ∈ (𝑁‘𝑥)))
Theorem	acsfiindd 18557	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 18558*	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 18556 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 18559*	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 18558 and observing that, since 𝑆 and 𝑇 have the same closure, the closure of ∪ ran 𝑓 must contain 𝑆. Since 𝑆 is independent, by mrissmrcd 17644, ∪ 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 18560	In an algebraic closure system, if 𝑆 and 𝑇 have the same closure and 𝑆 is infinite independent, then 𝑇 is infinite. This follows from applying unirnffid 9276 to the map given in acsmap2d 18559. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    &   ⊢ (𝜑 → ¬ 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → ¬ 𝑇 ∈ Fin)
Theorem	acsdomd 18561	In an algebraic closure system, if 𝑆 and 𝑇 have the same closure and 𝑆 is infinite independent, then 𝑇 dominates 𝑆. This follows from applying acsinfd 18560 and then applying unirnfdomd 10511 to the map given in acsmap2d 18559. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    &   ⊢ (𝜑 → ¬ 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑆 ≼ 𝑇)
Theorem	acsinfdimd 18562	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 18561 twice with acsinfd 18560. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))    &   ⊢ 𝑁 = (mrCls‘𝐴)    &   ⊢ 𝐼 = (mrInd‘𝐴)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐼)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐼)    &   ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))    &   ⊢ (𝜑 → ¬ 𝑆 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝑆 ≈ 𝑇)
Theorem	acsexdimd 18563*	In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 17654 for the finite case and acsinfdimd 18562 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 18564	Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015.) See mrelatglbALT 49555 for an alternate proof.
⊢ 𝐼 = (toInc‘𝐶)    &   ⊢ 𝐺 = (glb‘𝐼)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅) → (𝐺‘𝑈) = ∩ 𝑈)
Theorem	mrelatglb0 18565	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 18566	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 49554 for an alternate proof.
⊢ 𝐼 = (toInc‘𝐶)    &   ⊢ 𝐹 = (mrCls‘𝐶)    &   ⊢ 𝐿 = (lub‘𝐼)    ⇒   ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶) → (𝐿‘𝑈) = (𝐹‘∪ 𝑈))
Theorem	mreclatBAD 18567*	A Moore space is a complete lattice under inclusion. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 7338 update): Reprove using isclat 18504 instead of the isclatBAD. hypothesis. See commented-out mreclat above. See mreclat 49556 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 18568	Extend class notation with the class of all posets.
class PosetRel
Syntax	ctsr 18569	Extend class notation with the class of all totally ordered sets.
class TosetRel
Definition	df-ps 18570	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 18571	Define the class of all totally ordered sets. (Contributed by FL, 1-Nov-2009.)
⊢ TosetRel = {𝑟 ∈ PosetRel ∣ (dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)}
Theorem	isps 18572	The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation. (Contributed by NM, 11-May-2008.)
⊢ (𝑅 ∈ 𝐴 → (𝑅 ∈ PosetRel ↔ (Rel 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅))))
Theorem	psrel 18573	A poset is a relation. (Contributed by NM, 12-May-2008.)
⊢ (𝐴 ∈ PosetRel → Rel 𝐴)
Theorem	psref2 18574	A poset is antisymmetric and reflexive. (Contributed by FL, 3-Aug-2009.)
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅))
Theorem	pstr2 18575	A poset is transitive. (Contributed by FL, 3-Aug-2009.)
⊢ (𝑅 ∈ PosetRel → (𝑅 ∘ 𝑅) ⊆ 𝑅)
Theorem	pslem 18576	Lemma for psref 18578 and others. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝑅 ∈ PosetRel → (((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) ∧ (𝐴 ∈ ∪ ∪ 𝑅 → 𝐴𝑅𝐴) ∧ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵)))
Theorem	psdmrn 18577	The domain and range of a poset equal its field. (Contributed by NM, 13-May-2008.)
⊢ (𝑅 ∈ PosetRel → (dom 𝑅 = ∪ ∪ 𝑅 ∧ ran 𝑅 = ∪ ∪ 𝑅))
Theorem	psref 18578	A poset is reflexive. (Contributed by NM, 13-May-2008.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑋) → 𝐴𝑅𝐴)
Theorem	psrn 18579	The range of a poset equals it domain. (Contributed by NM, 7-Jul-2008.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ PosetRel → 𝑋 = ran 𝑅)
Theorem	psasym 18580	A poset is antisymmetric. (Contributed by NM, 12-May-2008.)
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵)
Theorem	pstr 18581	A poset is transitive. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Theorem	cnvps 18582	The converse of a poset is a poset. In the general case (◡𝑅 ∈ PosetRel → 𝑅 ∈ PosetRel) is not true. See cnvpsb 18583 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 18583	The converse of a poset is a poset. (Contributed by FL, 5-Jan-2009.)
⊢ (Rel 𝑅 → (𝑅 ∈ PosetRel ↔ ◡𝑅 ∈ PosetRel))
Theorem	psss 18584	Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010.)
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel)
Theorem	psssdm2 18585	Field of a subposet. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ PosetRel → dom (𝑅 ∩ (𝐴 × 𝐴)) = (𝑋 ∩ 𝐴))
Theorem	psssdm 18586	Field of a subposet. (Contributed by FL, 19-Sep-2011.) (Revised by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ⊆ 𝑋) → dom (𝑅 ∩ (𝐴 × 𝐴)) = 𝐴)
Theorem	istsr 18587	The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ TosetRel ↔ (𝑅 ∈ PosetRel ∧ (𝑋 × 𝑋) ⊆ (𝑅 ∪ ◡𝑅)))
Theorem	istsr2 18588*	The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ TosetRel ↔ (𝑅 ∈ PosetRel ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)))
Theorem	tsrlin 18589	A toset is a linear order. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ∨ 𝐵𝑅𝐴))
Theorem	tsrlemax 18590	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 18591	A toset is a poset. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ (𝑅 ∈ TosetRel → 𝑅 ∈ PosetRel)
Theorem	cnvtsr 18592	The converse of a toset is a toset. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝑅 ∈ TosetRel → ◡𝑅 ∈ TosetRel )
Theorem	tsrss 18593	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 18594	The domain of ≤ is ℝ*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.)
⊢ ℝ* = dom ≤
Theorem	lern 18595	The range of ≤ is ℝ*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
⊢ ℝ* = ran ≤
Theorem	lefld 18596	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 18597	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 18598	Extend class notation with the class of directed sets.
class DirRel
Syntax	ctail 18599	Extend class notation with the tail function for directed sets.
class tail
Definition	df-dir 18600	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 ↾ ∪ ∪ 𝑟) ⊆ 𝑟) ∧ ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)))}