P. 185 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18401-18500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pltfval 18401	Value of the less-than relation. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → < = ( ≤ ∖ I ))
Theorem	pltval 18402	Less-than relation. (df-pss 3996 analog.) (Contributed by NM, 12-Oct-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌)))
Theorem	pltle 18403	"Less than" implies "less than or equal to". (pssss 4121 analog.) (Contributed by NM, 4-Dec-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≤ 𝑌))
Theorem	pltne 18404	The "less than" relation is not reflexive. (df-pss 3996 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≠ 𝑌))
Theorem	pltirr 18405	The "less than" relation is not reflexive. (pssirr 4126 analog.) (Contributed by NM, 7-Feb-2012.)
⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ¬ 𝑋 < 𝑋)
Theorem	pleval2i 18406	One direction of pleval2 18407. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 < 𝑌 ∨ 𝑋 = 𝑌)))
Theorem	pleval2 18407	"Less than or equal to" in terms of "less than". (sspss 4125 analog.) (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 < 𝑌 ∨ 𝑋 = 𝑌)))
Theorem	pltnle 18408	"Less than" implies not converse "less than or equal to". (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 ≤ 𝑋)
Theorem	pltval3 18409	Alternate expression for the "less than" relation. (dfpss3 4112 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋)))
Theorem	pltnlt 18410	The less-than relation implies the negation of its inverse. (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 < 𝑋)
Theorem	pltn2lp 18411	The less-than relation has no 2-cycle loops. (pssn2lp 4127 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ¬ (𝑋 < 𝑌 ∧ 𝑌 < 𝑋))
Theorem	plttr 18412	The less-than relation is transitive. (psstr 4130 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍))
Theorem	pltletr 18413	Transitive law for chained "less than" and "less than or equal to". (psssstr 4132 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 < 𝑍))
Theorem	plelttr 18414	Transitive law for chained "less than or equal to" and "less than". (sspsstr 4131 analog.) (Contributed by NM, 2-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍))
Theorem	pospo 18415	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 18416*	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 18417*	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 18418*	Define poset join. (Contributed by NM, 12-Sep-2011.) (Revised by Mario Carneiro, 3-Nov-2015.)
⊢ join = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (lub‘𝑝)𝑧})
Definition	df-meet 18419*	Define poset meet. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 8-Sep-2018.)
⊢ meet = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧})
Theorem	lubfval 18420*	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 18421*	Domain of the least upper bound function of a poset. (Contributed by NM, 6-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝑈 = {𝑠 ∈ 𝒫 𝐵 ∣ ∃!𝑥 ∈ 𝐵 𝜓})
Theorem	lubfun 18422	The LUB is a function. (Contributed by NM, 9-Sep-2018.)
⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ Fun 𝑈
Theorem	lubeldm 18423*	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 18424	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 18425*	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 18426*	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 18427	The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) ∈ 𝐵)
Theorem	lubprop 18428*	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 18429	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 18430*	Lemma for lublecl 18431 and lubid 18432. (Contributed by NM, 8-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}𝑧 ≤ 𝑥 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤)) ↔ 𝑥 = 𝑋))
Theorem	lublecl 18431*	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 18432*	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 18433*	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 18434*	Domain of the greatest lower bound function of a poset. (Contributed by NM, 6-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝐺 = {𝑠 ∈ 𝒫 𝐵 ∣ ∃!𝑥 ∈ 𝐵 𝜓})
Theorem	glbfun 18435	The GLB is a function. (Contributed by NM, 9-Sep-2018.)
⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ Fun 𝐺
Theorem	glbeldm 18436*	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 18437	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 18438*	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 18439*	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 18440	The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝐺)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) ∈ 𝐵)
Theorem	glbprop 18441*	Properties of greatest lower bound of a poset. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (glb‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    ⇒   ⊢ (𝜑 → (∀𝑦 ∈ 𝑆 (𝑈‘𝑆) ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ (𝑈‘𝑆))))
Theorem	glble 18442	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 18443*	Value of join function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove joinfval2 18444 first to reduce net proof size (existence part)?
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → ∨ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦}𝑈𝑧})
Theorem	joinfval2 18444*	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 18445*	Domain of join function for a poset-type structure. (Contributed by NM, 16-Sep-2018.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → dom ∨ = {⟨𝑥, 𝑦⟩ ∣ {𝑥, 𝑦} ∈ dom 𝑈})
Theorem	joindef 18446	Two ways to say that a join is defined. (Contributed by NM, 9-Sep-2018.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ↔ {𝑋, 𝑌} ∈ dom 𝑈))
Theorem	joinval 18447	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 18448	Closure of join of elements in the domain. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )    ⇒   ⊢ (𝜑 → (𝑋 ∨ 𝑌) ∈ 𝐵)
Theorem	joindmss 18449	Subset property of domain of join. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom ∨ ⊆ (𝐵 × 𝐵))
Theorem	joinval2lem 18450*	Lemma for joinval2 18451 and joineu 18452. (Contributed by NM, 12-Sep-2018.) TODO: combine this through joineu 18452 into joinlem 18453?
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((∀𝑦 ∈ {𝑋, 𝑌}𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ {𝑋, 𝑌}𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)) ↔ ((𝑋 ≤ 𝑥 ∧ 𝑌 ≤ 𝑥) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → 𝑥 ≤ 𝑧))))
Theorem	joinval2 18451*	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 18452*	Uniqueness of join of elements in the domain. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐵 ((𝑋 ≤ 𝑥 ∧ 𝑌 ≤ 𝑥) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → 𝑥 ≤ 𝑧)))
Theorem	joinlem 18453*	Lemma for join properties. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )    ⇒   ⊢ (𝜑 → ((𝑋 ≤ (𝑋 ∨ 𝑌) ∧ 𝑌 ≤ (𝑋 ∨ 𝑌)) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → (𝑋 ∨ 𝑌) ≤ 𝑧)))
Theorem	lejoin1 18454	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 18455	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 18456	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 18457*	Value of meet function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove meetfval2 18458 first to reduce net proof size (existence part)?
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → ∧ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦}𝐺𝑧})
Theorem	meetfval2 18458*	Value of meet function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → ∧ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ({𝑥, 𝑦} ∈ dom 𝐺 ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))})
Theorem	meetdm 18459*	Domain of meet function for a poset-type structure. (Contributed by NM, 16-Sep-2018.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → dom ∧ = {⟨𝑥, 𝑦⟩ ∣ {𝑥, 𝑦} ∈ dom 𝐺})
Theorem	meetdef 18460	Two ways to say that a meet is defined. (Contributed by NM, 9-Sep-2018.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩ ∈ dom ∧ ↔ {𝑋, 𝑌} ∈ dom 𝐺))
Theorem	meetval 18461	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 18462	Closure of meet of elements in the domain. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )    ⇒   ⊢ (𝜑 → (𝑋 ∧ 𝑌) ∈ 𝐵)
Theorem	meetdmss 18463	Subset property of domain of meet. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom ∧ ⊆ (𝐵 × 𝐵))
Theorem	meetval2lem 18464*	Lemma for meetval2 18465 and meeteu 18466. (Contributed by NM, 12-Sep-2018.) TODO: combine this through meeteu 18466 into meetlem 18467?
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((∀𝑦 ∈ {𝑋, 𝑌}𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ {𝑋, 𝑌}𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)) ↔ ((𝑥 ≤ 𝑋 ∧ 𝑥 ≤ 𝑌) ∧ ∀𝑧 ∈ 𝐵 ((𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌) → 𝑧 ≤ 𝑥))))
Theorem	meetval2 18465*	Value of meet for a poset with LUB expanded. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 11-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 ∧ 𝑌) = (℩𝑥 ∈ 𝐵 ((𝑥 ≤ 𝑋 ∧ 𝑥 ≤ 𝑌) ∧ ∀𝑧 ∈ 𝐵 ((𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌) → 𝑧 ≤ 𝑥))))
Theorem	meeteu 18466*	Uniqueness of meet of elements in the domain. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐵 ((𝑥 ≤ 𝑋 ∧ 𝑥 ≤ 𝑌) ∧ ∀𝑧 ∈ 𝐵 ((𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌) → 𝑧 ≤ 𝑥)))
Theorem	meetlem 18467*	Lemma for meet properties. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )    ⇒   ⊢ (𝜑 → (((𝑋 ∧ 𝑌) ≤ 𝑋 ∧ (𝑋 ∧ 𝑌) ≤ 𝑌) ∧ ∀𝑧 ∈ 𝐵 ((𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌) → 𝑧 ≤ (𝑋 ∧ 𝑌))))
Theorem	lemeet1 18468	A meet's first argument is less than or equal to the meet. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )    ⇒   ⊢ (𝜑 → (𝑋 ∧ 𝑌) ≤ 𝑋)
Theorem	lemeet2 18469	A meet's second argument is less than or equal to the meet. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )    ⇒   ⊢ (𝜑 → (𝑋 ∧ 𝑌) ≤ 𝑌)
Theorem	meetle 18470	A meet 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.) (Revised by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )    ⇒   ⊢ (𝜑 → ((𝑍 ≤ 𝑋 ∧ 𝑍 ≤ 𝑌) ↔ 𝑍 ≤ (𝑋 ∧ 𝑌)))
Theorem	joincomALT 18471	The join of a poset is commutative. (This may not be a theorem under other definitions of meet.) (Contributed by NM, 16-Sep-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))
Theorem	joincom 18472	The join of a poset is commutative. (The antecedent ⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑌, 𝑋⟩ ∈ dom ∨ i.e., "the joins exist" could be omitted as an artifact of our particular join definition, but other definitions may require it.) (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑌, 𝑋⟩ ∈ dom ∨ )) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋))
Theorem	meetcomALT 18473	The meet of a poset is commutative. (This may not be a theorem under other definitions of meet.) (Contributed by NM, 17-Sep-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋))
Theorem	meetcom 18474	The meet of a poset is commutative. (The antecedent ⟨𝑋, 𝑌⟩ ∈ dom ∧ ∧ ⟨𝑌, 𝑋⟩ ∈ dom ∧ i.e., "the meets exist" could be omitted as an artifact of our particular join definition, but other definitions may require it.) (Contributed by NM, 17-Sep-2011.) (Revised by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (⟨𝑋, 𝑌⟩ ∈ dom ∧ ∧ ⟨𝑌, 𝑋⟩ ∈ dom ∧ )) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋))
Theorem	join0 18475	Lemma for odumeet 18480. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ (join‘∅) = ∅
Theorem	meet0 18476	Lemma for odujoin 18478. (Contributed by Stefan O'Rear, 29-Jan-2015.) TODO (df-riota 7404 update): This proof increased from 152 bytes to 547 bytes after the df-riota 7404 change. Any way to shorten it? join0 18475 also.
⊢ (meet‘∅) = ∅
Theorem	odulub 18477	Least upper bounds in a dual order are greatest lower bounds in the original order. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ 𝐿 = (glb‘𝑂)    ⇒   ⊢ (𝑂 ∈ 𝑉 → 𝐿 = (lub‘𝐷))
Theorem	odujoin 18478	Joins in a dual order are meets in the original. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ ∧ = (meet‘𝑂)    ⇒   ⊢ ∧ = (join‘𝐷)
Theorem	oduglb 18479	Greatest lower bounds in a dual order are least upper bounds in the original order. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ 𝑈 = (lub‘𝑂)    ⇒   ⊢ (𝑂 ∈ 𝑉 → 𝑈 = (glb‘𝐷))
Theorem	odumeet 18480	Meets in a dual order are joins in the original. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ ∨ = (join‘𝑂)    ⇒   ⊢ ∨ = (meet‘𝐷)
Theorem	poslubmo 18481*	Least upper bounds in a poset are unique if they exist. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by NM, 16-Jun-2017.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵) → ∃*𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)))
Theorem	posglbmo 18482*	Greatest lower bounds in a poset are unique if they exist. (Contributed by NM, 20-Sep-2018.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵) → ∃*𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))
Theorem	poslubd 18483*	Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ≤ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑥 ≤ 𝑦) → 𝑇 ≤ 𝑦)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇)
Theorem	poslubdg 18484*	Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ≤ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑥 ≤ 𝑦) → 𝑇 ≤ 𝑦)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇)
Theorem	posglbdg 18485*	Properties which determine the greatest lower bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐺 = (glb‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑇 ≤ 𝑥)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑦 ≤ 𝑥) → 𝑦 ≤ 𝑇)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) = 𝑇)
9.4  Totally ordered sets (tosets)
Syntax	ctos 18486	Extend class notation with the class of all tosets.
class Toset
Definition	df-toset 18487*	Define the class of totally ordered sets (tosets). (Contributed by FL, 17-Nov-2014.)
⊢ Toset = {𝑓 ∈ Poset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)}
Theorem	istos 18488*	The predicate "is a toset". (Contributed by FL, 17-Nov-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Toset ↔ (𝐾 ∈ Poset ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥)))
Theorem	tosso 18489	Write the totally ordered set structure predicate in terms of the proper class strict order predicate. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → (𝐾 ∈ Toset ↔ ( < Or 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )))
Theorem	tospos 18490	A Toset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ (𝐹 ∈ Toset → 𝐹 ∈ Poset)
Theorem	tleile 18491	In a Toset, any two elements are comparable. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋))
Theorem	tltnle 18492	In a Toset, "less than" is equivalent to the negation of the converse of "less than or equal to", see pltnle 18408. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ ¬ 𝑌 ≤ 𝑋))
Syntax	cp0 18493	Extend class notation with poset zero.
class 0.
Syntax	cp1 18494	Extend class notation with poset unit.
class 1.
Definition	df-p0 18495	Define poset zero. (Contributed by NM, 12-Oct-2011.)
⊢ 0. = (𝑝 ∈ V ↦ ((glb‘𝑝)‘(Base‘𝑝)))
Definition	df-p1 18496	Define poset unit. (Contributed by NM, 22-Oct-2011.)
⊢ 1. = (𝑝 ∈ V ↦ ((lub‘𝑝)‘(Base‘𝑝)))
Theorem	p0val 18497	Value of poset zero. (Contributed by NM, 12-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → 0 = (𝐺‘𝐵))
Theorem	p1val 18498	Value of poset zero. (Contributed by NM, 22-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → 1 = (𝑈‘𝐵))
Theorem	p0le 18499	Any element is less than or equal to a poset's upper bound (if defined). (Contributed by NM, 22-Oct-2011.) (Revised by NM, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝐺)    ⇒   ⊢ (𝜑 → 0 ≤ 𝑋)
Theorem	ple1 18500	Any element is less than or equal to a poset's upper bound (if defined). (Contributed by NM, 22-Oct-2011.) (Revised by NM, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑈)    ⇒   ⊢ (𝜑 → 𝑋 ≤ 1 )