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	pltletr 18301	Transitive law for chained "less than" and "less than or equal to". (psssstr 4107 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 < 𝑍))
Theorem	plelttr 18302	Transitive law for chained "less than or equal to" and "less than". (sspsstr 4106 analog.) (Contributed by NM, 2-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍))
Theorem	pospo 18303	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 18304*	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 18305*	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 18306*	Define poset join. (Contributed by NM, 12-Sep-2011.) (Revised by Mario Carneiro, 3-Nov-2015.)
⊢ join = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (lub‘𝑝)𝑧})
Definition	df-meet 18307*	Define poset meet. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 8-Sep-2018.)
⊢ meet = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧})
Theorem	lubfval 18308*	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 18309*	Domain of the least upper bound function of a poset. (Contributed by NM, 6-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝑈 = {𝑠 ∈ 𝒫 𝐵 ∣ ∃!𝑥 ∈ 𝐵 𝜓})
Theorem	lubfun 18310	The LUB is a function. (Contributed by NM, 9-Sep-2018.)
⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ Fun 𝑈
Theorem	lubeldm 18311*	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 18312	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 18313*	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 18314*	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 18315	The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) ∈ 𝐵)
Theorem	lubprop 18316*	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 18317	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 18318*	Lemma for lublecl 18319 and lubid 18320. (Contributed by NM, 8-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}𝑧 ≤ 𝑥 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤)) ↔ 𝑥 = 𝑋))
Theorem	lublecl 18319*	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 18320*	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 18321*	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 18322*	Domain of the greatest lower bound function of a poset. (Contributed by NM, 6-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝐺 = {𝑠 ∈ 𝒫 𝐵 ∣ ∃!𝑥 ∈ 𝐵 𝜓})
Theorem	glbfun 18323	The GLB is a function. (Contributed by NM, 9-Sep-2018.)
⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ Fun 𝐺
Theorem	glbeldm 18324*	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 18325	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 18326*	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 18327*	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 18328	The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝐺)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) ∈ 𝐵)
Theorem	glbprop 18329*	Properties of greatest lower bound of a poset. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (glb‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    ⇒   ⊢ (𝜑 → (∀𝑦 ∈ 𝑆 (𝑈‘𝑆) ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ (𝑈‘𝑆))))
Theorem	glble 18330	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 18331*	Value of join function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove joinfval2 18332 first to reduce net proof size (existence part)?
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → ∨ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦}𝑈𝑧})
Theorem	joinfval2 18332*	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 18333*	Domain of join function for a poset-type structure. (Contributed by NM, 16-Sep-2018.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → dom ∨ = {⟨𝑥, 𝑦⟩ ∣ {𝑥, 𝑦} ∈ dom 𝑈})
Theorem	joindef 18334	Two ways to say that a join is defined. (Contributed by NM, 9-Sep-2018.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ↔ {𝑋, 𝑌} ∈ dom 𝑈))
Theorem	joinval 18335	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 18336	Closure of join of elements in the domain. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )    ⇒   ⊢ (𝜑 → (𝑋 ∨ 𝑌) ∈ 𝐵)
Theorem	joindmss 18337	Subset property of domain of join. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom ∨ ⊆ (𝐵 × 𝐵))
Theorem	joinval2lem 18338*	Lemma for joinval2 18339 and joineu 18340. (Contributed by NM, 12-Sep-2018.) TODO: combine this through joineu 18340 into joinlem 18341?
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((∀𝑦 ∈ {𝑋, 𝑌}𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ {𝑋, 𝑌}𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)) ↔ ((𝑋 ≤ 𝑥 ∧ 𝑌 ≤ 𝑥) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → 𝑥 ≤ 𝑧))))
Theorem	joinval2 18339*	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 18340*	Uniqueness of join of elements in the domain. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐵 ((𝑋 ≤ 𝑥 ∧ 𝑌 ≤ 𝑥) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → 𝑥 ≤ 𝑧)))
Theorem	joinlem 18341*	Lemma for join properties. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )    ⇒   ⊢ (𝜑 → ((𝑋 ≤ (𝑋 ∨ 𝑌) ∧ 𝑌 ≤ (𝑋 ∨ 𝑌)) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → (𝑋 ∨ 𝑌) ≤ 𝑧)))
Theorem	lejoin1 18342	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 18343	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 18344	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 18345*	Value of meet function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove meetfval2 18346 first to reduce net proof size (existence part)?
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → ∧ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦}𝐺𝑧})
Theorem	meetfval2 18346*	Value of meet function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → ∧ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ({𝑥, 𝑦} ∈ dom 𝐺 ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))})
Theorem	meetdm 18347*	Domain of meet function for a poset-type structure. (Contributed by NM, 16-Sep-2018.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → dom ∧ = {⟨𝑥, 𝑦⟩ ∣ {𝑥, 𝑦} ∈ dom 𝐺})
Theorem	meetdef 18348	Two ways to say that a meet is defined. (Contributed by NM, 9-Sep-2018.)
⊢ 𝐺 = (glb‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩ ∈ dom ∧ ↔ {𝑋, 𝑌} ∈ dom 𝐺))
Theorem	meetval 18349	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 18350	Closure of meet of elements in the domain. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )    ⇒   ⊢ (𝜑 → (𝑋 ∧ 𝑌) ∈ 𝐵)
Theorem	meetdmss 18351	Subset property of domain of meet. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom ∧ ⊆ (𝐵 × 𝐵))
Theorem	meetval2lem 18352*	Lemma for meetval2 18353 and meeteu 18354. (Contributed by NM, 12-Sep-2018.) TODO: combine this through meeteu 18354 into meetlem 18355?
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((∀𝑦 ∈ {𝑋, 𝑌}𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ {𝑋, 𝑌}𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)) ↔ ((𝑥 ≤ 𝑋 ∧ 𝑥 ≤ 𝑌) ∧ ∀𝑧 ∈ 𝐵 ((𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌) → 𝑧 ≤ 𝑥))))
Theorem	meetval2 18353*	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 18354*	Uniqueness of meet of elements in the domain. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝐵 ((𝑥 ≤ 𝑋 ∧ 𝑥 ≤ 𝑌) ∧ ∀𝑧 ∈ 𝐵 ((𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌) → 𝑧 ≤ 𝑥)))
Theorem	meetlem 18355*	Lemma for meet properties. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )    ⇒   ⊢ (𝜑 → (((𝑋 ∧ 𝑌) ≤ 𝑋 ∧ (𝑋 ∧ 𝑌) ≤ 𝑌) ∧ ∀𝑧 ∈ 𝐵 ((𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌) → 𝑧 ≤ (𝑋 ∧ 𝑌))))
Theorem	lemeet1 18356	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 18357	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 18358	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 18359	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 18360	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 18361	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 18362	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 18363	Lemma for odumeet 18368. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ (join‘∅) = ∅
Theorem	meet0 18364	Lemma for odujoin 18366. (Contributed by Stefan O'Rear, 29-Jan-2015.) TODO (df-riota 7368 update): This proof increased from 152 bytes to 547 bytes after the df-riota 7368 change. Any way to shorten it? join0 18363 also.
⊢ (meet‘∅) = ∅
Theorem	odulub 18365	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 18366	Joins in a dual order are meets in the original. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ ∧ = (meet‘𝑂)    ⇒   ⊢ ∧ = (join‘𝐷)
Theorem	oduglb 18367	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 18368	Meets in a dual order are joins in the original. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ ∨ = (join‘𝑂)    ⇒   ⊢ ∨ = (meet‘𝐷)
Theorem	poslubmo 18369*	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 18370*	Greatest lower bounds in a poset are unique if they exist. (Contributed by NM, 20-Sep-2018.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵) → ∃*𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))
Theorem	poslubd 18371*	Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ≤ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑥 ≤ 𝑦) → 𝑇 ≤ 𝑦)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇)
Theorem	poslubdg 18372*	Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ ≤ = (le‘𝐾)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝑈 = (lub‘𝐾))    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ≤ 𝑇)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑥 ≤ 𝑦) → 𝑇 ≤ 𝑦)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇)
Theorem	posglbdg 18373*	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 18374	Extend class notation with the class of all tosets.
class Toset
Definition	df-toset 18375*	Define the class of totally ordered sets (tosets). (Contributed by FL, 17-Nov-2014.)
⊢ Toset = {𝑓 ∈ Poset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑟𝑦 ∨ 𝑦𝑟𝑥)}
Theorem	istos 18376*	The predicate "is a toset". (Contributed by FL, 17-Nov-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Toset ↔ (𝐾 ∈ Poset ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥)))
Theorem	tosso 18377	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 18378	A Toset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ (𝐹 ∈ Toset → 𝐹 ∈ Poset)
Theorem	tleile 18379	In a Toset, any two elements are comparable. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋))
Theorem	tltnle 18380	In a Toset, "less than" is equivalent to the negation of the converse of "less than or equal to", see pltnle 18296. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ ¬ 𝑌 ≤ 𝑋))
Syntax	cp0 18381	Extend class notation with poset zero.
class 0.
Syntax	cp1 18382	Extend class notation with poset unit.
class 1.
Definition	df-p0 18383	Define poset zero. (Contributed by NM, 12-Oct-2011.)
⊢ 0. = (𝑝 ∈ V ↦ ((glb‘𝑝)‘(Base‘𝑝)))
Definition	df-p1 18384	Define poset unit. (Contributed by NM, 22-Oct-2011.)
⊢ 1. = (𝑝 ∈ V ↦ ((lub‘𝑝)‘(Base‘𝑝)))
Theorem	p0val 18385	Value of poset zero. (Contributed by NM, 12-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → 0 = (𝐺‘𝐵))
Theorem	p1val 18386	Value of poset zero. (Contributed by NM, 22-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → 1 = (𝑈‘𝐵))
Theorem	p0le 18387	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 18388	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 )
9.5  Lattices
9.5.1  Lattices
Syntax	clat 18389	Extend class notation with the class of all lattices.
class Lat
Definition	df-lat 18390	Define the class of all lattices. A lattice is a poset in which the join and meet of any two elements always exists. (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.)
⊢ Lat = {𝑝 ∈ Poset ∣ (dom (join‘𝑝) = ((Base‘𝑝) × (Base‘𝑝)) ∧ dom (meet‘𝑝) = ((Base‘𝑝) × (Base‘𝑝)))}
Theorem	islat 18391	The predicate "is a lattice". (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ (𝐾 ∈ Lat ↔ (𝐾 ∈ Poset ∧ (dom ∨ = (𝐵 × 𝐵) ∧ dom ∧ = (𝐵 × 𝐵))))
Theorem	odulatb 18392	Being a lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    ⇒   ⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ Lat ↔ 𝐷 ∈ Lat))
Theorem	odulat 18393	Being a lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    ⇒   ⊢ (𝑂 ∈ Lat → 𝐷 ∈ Lat)
Theorem	latcl2 18394	The join and meet of any two elements exist. (Contributed by NM, 14-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Lat)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom ∧ ))
Theorem	latlem 18395	Lemma for lattice properties. (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∨ 𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ∈ 𝐵))
Theorem	latpos 18396	A lattice is a poset. (Contributed by NM, 17-Sep-2011.)
⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
Theorem	latjcl 18397	Closure of join operation in a lattice. (chjcom 31023 analog.) (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)
Theorem	latmcl 18398	Closure of meet operation in a lattice. (incom 4202 analog.) (Contributed by NM, 14-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)
Theorem	latref 18399	A lattice ordering is reflexive. (ssid 4005 analog.) (Contributed by NM, 8-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋)
Theorem	latasymb 18400	A lattice ordering is asymmetric. (eqss 3998 analog.) (Contributed by NM, 22-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌))