P. 184 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18301-18400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	odubas 18301	Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Proof shortened by AV, 12-Nov-2024.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ 𝐵 = (Base‘𝑂)    ⇒   ⊢ 𝐵 = (Base‘𝐷)
9.2  Preordered sets and directed sets
Syntax	cproset 18302	Extend class notation with the class of all prosets.
class Proset
Syntax	cdrs 18303	Extend class notation with the class of all directed sets.
class Dirset
Definition	df-proset 18304*	Define the class of preordered sets, or prosets. A proset is a set equipped with a preorder, that is, a transitive and reflexive relation. Preorders are a natural generalization of partial orders which need not be antisymmetric: there may be pairs of elements such that each is "less than or equal to" the other, so that both elements have the same order-theoretic properties (in some sense, there is a "tie" among them). If a preorder is required to be antisymmetric, that is, there is no such "tie", then one obtains a partial order. If a preorder is required to be symmetric, that is, all comparable elements are tied, then one obtains an equivalence relation. Every preorder naturally factors into these two notions: the "tie" relation on a proset is an equivalence relation, and the quotient under that equivalence relation is a partial order. (Contributed by FL, 17-Nov-2014.) (Revised by Stefan O'Rear, 31-Jan-2015.)
⊢ Proset = {𝑓 ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))}
Definition	df-drs 18305*	Define the class of directed sets. A directed set is a nonempty preordered set where every pair of elements have some upper bound. Note that it is not required that there exist a least upper bound. There is no consensus in the literature over whether directed sets are allowed to be empty. It is slightly more convenient for us if they are not. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ Dirset = {𝑓 ∈ Proset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))}
Theorem	isprs 18306*	Property of being a preordered set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Proset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))))
Theorem	prslem 18307	Lemma for prsref 18308 and prstr 18309. (Contributed by Mario Carneiro, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)))
Theorem	prsref 18308	"Less than or equal to" is reflexive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋)
Theorem	prstr 18309	"Less than or equal to" is transitive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → 𝑋 ≤ 𝑍)
Theorem	oduprs 18310	Being a proset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐷 = (ODual‘𝐾)    ⇒   ⊢ (𝐾 ∈ Proset → 𝐷 ∈ Proset )
Theorem	isdrs 18311*	Property of being a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧)))
Theorem	drsdir 18312*	Direction of a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Dirset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ∃𝑧 ∈ 𝐵 (𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧))
Theorem	drsprs 18313	A directed set is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐾 ∈ Dirset → 𝐾 ∈ Proset )
Theorem	drsbn0 18314	The base of a directed set is not empty. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ (𝐾 ∈ Dirset → 𝐵 ≠ ∅)
Theorem	drsdirfi 18315*	Any finite number of elements in a directed set have a common upper bound. Here is where the nonemptiness constraint in df-drs 18305 first comes into play; without it we would need an additional constraint that 𝑋 not be empty. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Dirset ∧ 𝑋 ⊆ 𝐵 ∧ 𝑋 ∈ Fin) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑦)
Theorem	isdrs2 18316*	Directed sets may be defined in terms of finite subsets. Again, without nonemptiness we would need to restrict to nonempty subsets here. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Proset ∧ ∀𝑥 ∈ (𝒫 𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦))
9.3  Partially ordered sets (posets)
Syntax	cpo 18317	Extend class notation with the class of posets.
class Poset
Syntax	cplt 18318	Extend class notation with less-than for posets.
class lt
Syntax	club 18319	Extend class notation with poset least upper bound.
class lub
Syntax	cglb 18320	Extend class notation with poset greatest lower bound.
class glb
Syntax	cjn 18321	Extend class notation with poset join.
class join
Syntax	cmee 18322	Extend class notation with poset meet.
class meet
Definition	df-poset 18323*	Define the class of partially ordered sets (posets). A poset is a set equipped with a partial order, that is, a binary relation which is reflexive, antisymmetric, and transitive. Unlike a total order, in a partial order there may be pairs of elements where neither precedes the other. Definition of poset in [Crawley] p. 1. Note that Crawley-Dilworth require that a poset base set be nonempty, but we follow the convention of most authors who don't make this a requirement. In our formalism of extensible structures, the base set of a poset 𝑓 is denoted by (Base‘𝑓) and its partial order by (le‘𝑓) (for "less than or equal to"). The quantifiers ∃𝑏∃𝑟 provide a notational shorthand to allow to refer to the base and ordering relation as 𝑏 and 𝑟 in the definition rather than having to repeat (Base‘𝑓) and (le‘𝑓) throughout. These quantifiers can be eliminated with ceqsex2v 3515 and related theorems. (Contributed by NM, 18-Oct-2012.)
⊢ Poset = {𝑓 ∣ ∃𝑏∃𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))}
Theorem	ispos 18324*	The predicate "is a poset". (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 4-Nov-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))))
Theorem	ispos2 18325*	A poset is an antisymmetric proset. EDITORIAL: could become the definition of poset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ Proset ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)))
Theorem	posprs 18326	A poset is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset )
Theorem	posi 18327	Lemma for poset properties. (Contributed by NM, 11-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)))
Theorem	posref 18328	A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋)
Theorem	posasymb 18329	A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌))
Theorem	postr 18330	A poset ordering is transitive. (Contributed by NM, 11-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))
Theorem	0pos 18331	Technical lemma to simplify the statement of ipopos 18544. The empty set is (rather pathologically) a poset under our definitions, since it has an empty base set (str0 17206) and any relation partially orders an empty set. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Proof shortened by AV, 13-Oct-2024.)
⊢ ∅ ∈ Poset
Theorem	isposd 18332*	Properties that determine a poset (implicit structure version). (Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by AV, 26-Apr-2024.)
⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → ≤ = (le‘𝐾))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ≤ 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))    ⇒   ⊢ (𝜑 → 𝐾 ∈ Poset)
Theorem	isposi 18333*	Properties that determine a poset (implicit structure version). (Contributed by NM, 11-Sep-2011.)
⊢ 𝐾 ∈ V    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))    ⇒   ⊢ 𝐾 ∈ Poset
Theorem	isposix 18334*	Properties that determine a poset (explicit structure version). Note that the numeric indices of the structure components are not mentioned explicitly in either the theorem or its proof. (Contributed by NM, 9-Nov-2012.) (Proof shortened by AV, 30-Oct-2024.)
⊢ 𝐵 ∈ V    &   ⊢ ≤ ∈ V    &   ⊢ 𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ≤ ⟩}    &   ⊢ (𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))    ⇒   ⊢ 𝐾 ∈ Poset
Theorem	pospropd 18335*	Posethood is determined only by structure components and only by the value of the relation within the base set. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(le‘𝐾)𝑦 ↔ 𝑥(le‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ Poset ↔ 𝐿 ∈ Poset))
Theorem	odupos 18336	Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    ⇒   ⊢ (𝑂 ∈ Poset → 𝐷 ∈ Poset)
Theorem	oduposb 18337	Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    ⇒   ⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ Poset ↔ 𝐷 ∈ Poset))
Definition	df-plt 18338	Define less-than ordering for posets and related structures. Unlike df-base 17227 and df-ple 17289, this is a derived component extractor and not an extensible structure component extractor that defines the poset. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.)
⊢ lt = (𝑝 ∈ V ↦ ((le‘𝑝) ∖ I ))
Theorem	pltfval 18339	Value of the less-than relation. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → < = ( ≤ ∖ I ))
Theorem	pltval 18340	Less-than relation. (df-pss 3946 analog.) (Contributed by NM, 12-Oct-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌)))
Theorem	pltle 18341	"Less than" implies "less than or equal to". (pssss 4073 analog.) (Contributed by NM, 4-Dec-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≤ 𝑌))
Theorem	pltne 18342	The "less than" relation is not reflexive. (df-pss 3946 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≠ 𝑌))
Theorem	pltirr 18343	The "less than" relation is not reflexive. (pssirr 4078 analog.) (Contributed by NM, 7-Feb-2012.)
⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ¬ 𝑋 < 𝑋)
Theorem	pleval2i 18344	One direction of pleval2 18345. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 < 𝑌 ∨ 𝑋 = 𝑌)))
Theorem	pleval2 18345	"Less than or equal to" in terms of "less than". (sspss 4077 analog.) (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 < 𝑌 ∨ 𝑋 = 𝑌)))
Theorem	pltnle 18346	"Less than" implies not converse "less than or equal to". (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 ≤ 𝑋)
Theorem	pltval3 18347	Alternate expression for the "less than" relation. (dfpss3 4064 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋)))
Theorem	pltnlt 18348	The less-than relation implies the negation of its inverse. (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 < 𝑋)
Theorem	pltn2lp 18349	The less-than relation has no 2-cycle loops. (pssn2lp 4079 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ¬ (𝑋 < 𝑌 ∧ 𝑌 < 𝑋))
Theorem	plttr 18350	The less-than relation is transitive. (psstr 4082 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍))
Theorem	pltletr 18351	Transitive law for chained "less than" and "less than or equal to". (psssstr 4084 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 < 𝑍))
Theorem	plelttr 18352	Transitive law for chained "less than or equal to" and "less than". (sspsstr 4083 analog.) (Contributed by NM, 2-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍))
Theorem	pospo 18353	Write a poset structure in terms of the proper-class poset predicate (strict less than version). (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → (𝐾 ∈ Poset ↔ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )))
Definition	df-lub 18354*	Define the least upper bound (LUB) of a set of (poset) elements. The domain is restricted to exclude sets 𝑠 for which the LUB doesn't exist uniquely. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.)
⊢ lub = (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))}))
Definition	df-glb 18355*	Define the greatest lower bound (GLB) of a set of (poset) elements. The domain is restricted to exclude sets 𝑠 for which the GLB doesn't exist uniquely. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.)
⊢ glb = (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑧(le‘𝑝)𝑦 → 𝑧(le‘𝑝)𝑥)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑧(le‘𝑝)𝑦 → 𝑧(le‘𝑝)𝑥))}))
Definition	df-join 18356*	Define poset join. (Contributed by NM, 12-Sep-2011.) (Revised by Mario Carneiro, 3-Nov-2015.)
⊢ join = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (lub‘𝑝)𝑧})
Definition	df-meet 18357*	Define poset meet. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 8-Sep-2018.)
⊢ meet = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧})
Theorem	lubfval 18358*	Value of the least upper bound function of a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑈 = ((𝑠 ∈ 𝒫 𝐵 ↦ (℩𝑥 ∈ 𝐵 𝜓)) ↾ {𝑠 ∣ ∃!𝑥 ∈ 𝐵 𝜓}))
Theorem	lubdm 18359*	Domain of the least upper bound function of a poset. (Contributed by NM, 6-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝑈 = {𝑠 ∈ 𝒫 𝐵 ∣ ∃!𝑥 ∈ 𝐵 𝜓})
Theorem	lubfun 18360	The LUB is a function. (Contributed by NM, 9-Sep-2018.)
⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ Fun 𝑈
Theorem	lubeldm 18361*	Member of the domain of the least upper bound function of a poset. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ↔ (𝑆 ⊆ 𝐵 ∧ ∃!𝑥 ∈ 𝐵 𝜓)))
Theorem	lubelss 18362	A member of the domain of the least upper bound function is a subset of the base set. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
Theorem	lubeu 18363*	Unique existence proper of a member of the domain of the least upper bound function of a poset. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐵 𝜓)
Theorem	lubval 18364*	Value of the least upper bound function of a poset. Out-of-domain arguments (those not satisfying 𝑆 ∈ dom 𝑈) are allowed for convenience, evaluating to the empty set. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) = (℩𝑥 ∈ 𝐵 𝜓))
Theorem	lubcl 18365	The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) ∈ 𝐵)
Theorem	lubprop 18366*	Properties of greatest lower bound of a poset. (Contributed by NM, 22-Oct-2011.) (Revised by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    ⇒   ⊢ (𝜑 → (∀𝑦 ∈ 𝑆 𝑦 ≤ (𝑈‘𝑆) ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → (𝑈‘𝑆) ≤ 𝑧)))
Theorem	luble 18367	The greatest lower bound is the least element. (Contributed by NM, 22-Oct-2011.) (Revised by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑋 ≤ (𝑈‘𝑆))
Theorem	lublecllem 18368*	Lemma for lublecl 18369 and lubid 18370. (Contributed by NM, 8-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}𝑧 ≤ 𝑥 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤)) ↔ 𝑥 = 𝑋))
Theorem	lublecl 18369*	The set of all elements less than a given element has an LUB. (Contributed by NM, 8-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋} ∈ dom 𝑈)
Theorem	lubid 18370*	The LUB of elements less than or equal to a fixed value equals that value. (Contributed by NM, 19-Oct-2011.) (Revised by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑈‘{𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}) = 𝑋)
Theorem	glbfval 18371*	Value of the greatest lower function of a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐺 = ((𝑠 ∈ 𝒫 𝐵 ↦ (℩𝑥 ∈ 𝐵 𝜓)) ↾ {𝑠 ∣ ∃!𝑥 ∈ 𝐵 𝜓}))
Theorem	glbdm 18372*	Domain of the greatest lower bound function of a poset. (Contributed by NM, 6-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝐺 = {𝑠 ∈ 𝒫 𝐵 ∣ ∃!𝑥 ∈ 𝐵 𝜓})
Theorem	glbfun 18373	The GLB is a function. (Contributed by NM, 9-Sep-2018.)
⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ Fun 𝐺
Theorem	glbeldm 18374*	Member of the domain of the greatest lower bound function of a poset. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ (𝑆 ⊆ 𝐵 ∧ ∃!𝑥 ∈ 𝐵 𝜓)))
Theorem	glbelss 18375	A member of the domain of the greatest lower bound function is a subset of the base set. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝐺)    ⇒   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)
Theorem	glbeu 18376*	Unique existence proper of a member of the domain of the greatest lower bound function of a poset. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝐺)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐵 𝜓)
Theorem	glbval 18377*	Value of the greatest lower bound function of a poset. Out-of-domain arguments (those not satisfying 𝑆 ∈ dom 𝑈) are allowed for convenience, evaluating to the empty set on both sides of the equality. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) = (℩𝑥 ∈ 𝐵 𝜓))
Theorem	glbcl 18378	The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝐺)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) ∈ 𝐵)
Theorem	glbprop 18379*	Properties of greatest lower bound of a poset. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (glb‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    ⇒   ⊢ (𝜑 → (∀𝑦 ∈ 𝑆 (𝑈‘𝑆) ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ (𝑈‘𝑆))))
Theorem	glble 18380	The greatest lower bound is the least element. (Contributed by NM, 22-Oct-2011.) (Revised by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (glb‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) ≤ 𝑋)
Theorem	joinfval 18381*	Value of join function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove joinfval2 18382 first to reduce net proof size (existence part)?
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → ∨ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦}𝑈𝑧})
Theorem	joinfval2 18382*	Value of join function for a poset-type structure. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → ∨ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ({𝑥, 𝑦} ∈ dom 𝑈 ∧ 𝑧 = (𝑈‘{𝑥, 𝑦}))})
Theorem	joindm 18383*	Domain of join function for a poset-type structure. (Contributed by NM, 16-Sep-2018.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → dom ∨ = {⟨𝑥, 𝑦⟩ ∣ {𝑥, 𝑦} ∈ dom 𝑈})
Theorem	joindef 18384	Two ways to say that a join is defined. (Contributed by NM, 9-Sep-2018.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ↔ {𝑋, 𝑌} ∈ dom 𝑈))
Theorem	joinval 18385	Join value. Since both sides evaluate to ∅ when they don't exist, for convenience we drop the {𝑋, 𝑌} ∈ dom 𝑈 requirement. (Contributed by NM, 9-Sep-2018.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (𝑋 ∨ 𝑌) = (𝑈‘{𝑋, 𝑌}))
Theorem	joincl 18386	Closure of join of elements in the domain. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )    ⇒   ⊢ (𝜑 → (𝑋 ∨ 𝑌) ∈ 𝐵)
Theorem	joindmss 18387	Subset property of domain of join. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom ∨ ⊆ (𝐵 × 𝐵))
Theorem	joinval2lem 18388*	Lemma for joinval2 18389 and joineu 18390. (Contributed by NM, 12-Sep-2018.) TODO: combine this through joineu 18390 into joinlem 18391?
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((∀𝑦 ∈ {𝑋, 𝑌}𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ {𝑋, 𝑌}𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)) ↔ ((𝑋 ≤ 𝑥 ∧ 𝑌 ≤ 𝑥) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → 𝑥 ≤ 𝑧))))
Theorem	joinval2 18389*	Value of join for a poset with LUB expanded. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 11-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∨ 𝑌) = (℩𝑥 ∈ 𝐵 ((𝑋 ≤ 𝑥 ∧ 𝑌 ≤ 𝑥) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → 𝑥 ≤ 𝑧))))
Theorem	joineu 18390*	Uniqueness of join of elements in the domain. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐵 ((𝑋 ≤ 𝑥 ∧ 𝑌 ≤ 𝑥) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → 𝑥 ≤ 𝑧)))
Theorem	joinlem 18391*	Lemma for join properties. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )    ⇒   ⊢ (𝜑 → ((𝑋 ≤ (𝑋 ∨ 𝑌) ∧ 𝑌 ≤ (𝑋 ∨ 𝑌)) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → (𝑋 ∨ 𝑌) ≤ 𝑧)))
Theorem	lejoin1 18392	A join's first argument is less than or equal to the join. (Contributed by NM, 16-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )    ⇒   ⊢ (𝜑 → 𝑋 ≤ (𝑋 ∨ 𝑌))
Theorem	lejoin2 18393	A join's second argument is less than or equal to the join. (Contributed by NM, 16-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )    ⇒   ⊢ (𝜑 → 𝑌 ≤ (𝑋 ∨ 𝑌))
Theorem	joinle 18394	A join is less than or equal to a third value iff each argument is less than or equal to the third value. (Contributed by NM, 16-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )    ⇒   ⊢ (𝜑 → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))
Theorem	meetfval 18395*	Value of meet function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove meetfval2 18396 first to reduce net proof size (existence part)?
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → ∧ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦}𝐺𝑧})
Theorem	meetfval2 18396*	Value of meet function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → ∧ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ({𝑥, 𝑦} ∈ dom 𝐺 ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))})
Theorem	meetdm 18397*	Domain of meet function for a poset-type structure. (Contributed by NM, 16-Sep-2018.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → dom ∧ = {⟨𝑥, 𝑦⟩ ∣ {𝑥, 𝑦} ∈ dom 𝐺})
Theorem	meetdef 18398	Two ways to say that a meet is defined. (Contributed by NM, 9-Sep-2018.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩ ∈ dom ∧ ↔ {𝑋, 𝑌} ∈ dom 𝐺))
Theorem	meetval 18399	Meet value. Since both sides evaluate to ∅ when they don't exist, for convenience we drop the {𝑋, 𝑌} ∈ dom 𝐺 requirement. (Contributed by NM, 9-Sep-2018.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (𝑋 ∧ 𝑌) = (𝐺‘{𝑋, 𝑌}))
Theorem	meetcl 18400	Closure of meet of elements in the domain. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )    ⇒   ⊢ (𝜑 → (𝑋 ∧ 𝑌) ∈ 𝐵)