P. 183 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18201-18300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	yonedalem22 18201	Lemma for yoneda 18206. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))    ⇒   ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) = (((𝑃(2nd ‘𝑌)𝑋)‘𝐾)(⟨((1st ‘𝑌)‘𝑋), 𝐹⟩(2nd ‘𝐻)⟨((1st ‘𝑌)‘𝑃), 𝐺⟩)𝐴))
Theorem	yonedalem3b 18202*	Lemma for yoneda 18206. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑆))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))    &   ⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))    &   ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))    ⇒   ⊢ (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1st ‘𝑍)𝑋), (𝐺(1st ‘𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1st ‘𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1st ‘𝑍)𝑋), (𝐹(1st ‘𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1st ‘𝐸)𝑃))(𝐹𝑀𝑋)))
Theorem	yonedalem3 18203*	Lemma for yoneda 18206. (Contributed by Mario Carneiro, 28-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))    ⇒   ⊢ (𝜑 → 𝑀 ∈ (𝑍((𝑄 ×c 𝑂) Nat 𝑇)𝐸))
Theorem	yonedainv 18204*	The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))    &   ⊢ 𝐼 = (Inv‘𝑅)    &   ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))))    ⇒   ⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)𝑁)
Theorem	yonffthlem 18205*	Lemma for yonffth 18207. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))    &   ⊢ 𝐼 = (Inv‘𝑅)    &   ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))))    ⇒   ⊢ (𝜑 → 𝑌 ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄)))
Theorem	yoneda 18206*	The Yoneda Lemma. There is a natural isomorphism between the functors 𝑍 and 𝐸, where 𝑍(𝐹, 𝑋) is the natural transformations from Yon(𝑋) = Hom ( − , 𝑋) to 𝐹, and 𝐸(𝐹, 𝑋) = 𝐹(𝑋) is the evaluation functor. Here we need two universes to state the claim: the smaller universe 𝑈 is used for forming the functor category 𝑄 = 𝐶 op → SetCat(𝑈), which itself does not (necessarily) live in 𝑈 but instead is an element of the larger universe 𝑉. (If 𝑈 is a Grothendieck universe, then it will be closed under this "presheaf" operation, and so we can set 𝑈 = 𝑉 in this case.) (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 1 = (Id‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑇 = (SetCat‘𝑉)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐻 = (HomF‘𝑄)    &   ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)    &   ⊢ 𝐸 = (𝑂 evalF 𝑆)    &   ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)    &   ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))    &   ⊢ 𝐼 = (Iso‘𝑅)    ⇒   ⊢ (𝜑 → 𝑀 ∈ (𝑍𝐼𝐸))
Theorem	yonffth 18207	The Yoneda Lemma. The Yoneda embedding, the curried Hom functor, is full and faithful, and hence is a representation of the category 𝐶 as a full subcategory of the category 𝑄 of presheaves on 𝐶. (Contributed by Mario Carneiro, 29-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ Cat)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    ⇒   ⊢ (𝜑 → 𝑌 ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄)))
Theorem	yoniso 18208*	If the codomain is recoverable from a hom-set, then the Yoneda embedding is injective on objects, and hence is an isomorphism from 𝐶 into a full subcategory of a presheaf category. (Contributed by Mario Carneiro, 30-Jan-2017.)
⊢ 𝑌 = (Yon‘𝐶)    &   ⊢ 𝑂 = (oppCat‘𝐶)    &   ⊢ 𝑆 = (SetCat‘𝑈)    &   ⊢ 𝐷 = (CatCat‘𝑉)    &   ⊢ 𝐵 = (Base‘𝐷)    &   ⊢ 𝐼 = (Iso‘𝐷)    &   ⊢ 𝑄 = (𝑂 FuncCat 𝑆)    &   ⊢ 𝐸 = (𝑄 ↾s ran (1st ‘𝑌))    &   ⊢ (𝜑 → 𝑉 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑊)    &   ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝐹‘(𝑥(Hom ‘𝐶)𝑦)) = 𝑦)    ⇒   ⊢ (𝜑 → 𝑌 ∈ (𝐶𝐼𝐸))
PART 9  BASIC ORDER THEORY
9.1  Dual of an order structure
Syntax	codu 18209	Class function defining dual orders.
class ODual
Definition	df-odu 18210	Define the dual of an ordered structure, which replaces the order component of the structure with its reverse. See odubas 18214, oduleval 18212, and oduleg 18213 for its principal properties. EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 18418. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ ODual = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(le‘ndx), ◡(le‘𝑤)⟩))
Theorem	oduval 18211	Value of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ ≤ = (le‘𝑂)    ⇒   ⊢ 𝐷 = (𝑂 sSet ⟨(le‘ndx), ◡ ≤ ⟩)
Theorem	oduleval 18212	Value of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ ≤ = (le‘𝑂)    ⇒   ⊢ ◡ ≤ = (le‘𝐷)
Theorem	oduleg 18213	Truth of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    &   ⊢ ≤ = (le‘𝑂)    &   ⊢ 𝐺 = (le‘𝐷)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝐺𝐵 ↔ 𝐵 ≤ 𝐴))
Theorem	odubas 18214	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 18215	Extend class notation with the class of all prosets.
class Proset
Syntax	cdrs 18216	Extend class notation with the class of all directed sets.
class Dirset
Definition	df-proset 18217*	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 18218*	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 18219*	Property of being a preordered set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Proset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))))
Theorem	prslem 18220	Lemma for prsref 18221 and prstr 18222. (Contributed by Mario Carneiro, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)))
Theorem	prsref 18221	"Less than or equal to" is reflexive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋)
Theorem	prstr 18222	"Less than or equal to" is transitive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → 𝑋 ≤ 𝑍)
Theorem	oduprs 18223	Being a proset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐷 = (ODual‘𝐾)    ⇒   ⊢ (𝐾 ∈ Proset → 𝐷 ∈ Proset )
Theorem	isdrs 18224*	Property of being a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧)))
Theorem	drsdir 18225*	Direction of a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Dirset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ∃𝑧 ∈ 𝐵 (𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧))
Theorem	drsprs 18226	A directed set is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐾 ∈ Dirset → 𝐾 ∈ Proset )
Theorem	drsbn0 18227	The base of a directed set is not empty. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ (𝐾 ∈ Dirset → 𝐵 ≠ ∅)
Theorem	drsdirfi 18228*	Any finite number of elements in a directed set have a common upper bound. Here is where the nonemptiness constraint in df-drs 18218 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 18229*	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 18230	Extend class notation with the class of posets.
class Poset
Syntax	cplt 18231	Extend class notation with less-than for posets.
class lt
Syntax	club 18232	Extend class notation with poset least upper bound.
class lub
Syntax	cglb 18233	Extend class notation with poset greatest lower bound.
class glb
Syntax	cjn 18234	Extend class notation with poset join.
class join
Syntax	cmee 18235	Extend class notation with poset meet.
class meet
Definition	df-poset 18236*	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 3494 and related theorems. (Contributed by NM, 18-Oct-2012.)
⊢ Poset = {𝑓 ∣ ∃𝑏∃𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))}
Theorem	ispos 18237*	The predicate "is a poset". (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 4-Nov-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))))
Theorem	ispos2 18238*	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 18239	A poset is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset )
Theorem	posi 18240	Lemma for poset properties. (Contributed by NM, 11-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)))
Theorem	posref 18241	A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋)
Theorem	posasymb 18242	A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌))
Theorem	postr 18243	A poset ordering is transitive. (Contributed by NM, 11-Sep-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))
Theorem	0pos 18244	Technical lemma to simplify the statement of ipopos 18459. The empty set is (rather pathologically) a poset under our definitions, since it has an empty base set (str0 17116) 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 18245*	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 18246*	Properties that determine a poset (implicit structure version). (Contributed by NM, 11-Sep-2011.)
⊢ 𝐾 ∈ V    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ (𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))    ⇒   ⊢ 𝐾 ∈ Poset
Theorem	isposix 18247*	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 18248*	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 18249	Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    ⇒   ⊢ (𝑂 ∈ Poset → 𝐷 ∈ Poset)
Theorem	oduposb 18250	Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ 𝐷 = (ODual‘𝑂)    ⇒   ⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ Poset ↔ 𝐷 ∈ Poset))
Definition	df-plt 18251	Define less-than ordering for posets and related structures. Unlike df-base 17137 and df-ple 17197, 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 18252	Value of the less-than relation. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → < = ( ≤ ∖ I ))
Theorem	pltval 18253	Less-than relation. (df-pss 3921 analog.) (Contributed by NM, 12-Oct-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌)))
Theorem	pltle 18254	"Less than" implies "less than or equal to". (pssss 4050 analog.) (Contributed by NM, 4-Dec-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≤ 𝑌))
Theorem	pltne 18255	The "less than" relation is not reflexive. (df-pss 3921 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≠ 𝑌))
Theorem	pltirr 18256	The "less than" relation is not reflexive. (pssirr 4055 analog.) (Contributed by NM, 7-Feb-2012.)
⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ¬ 𝑋 < 𝑋)
Theorem	pleval2i 18257	One direction of pleval2 18258. (Contributed by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 < 𝑌 ∨ 𝑋 = 𝑌)))
Theorem	pleval2 18258	"Less than or equal to" in terms of "less than". (sspss 4054 analog.) (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 < 𝑌 ∨ 𝑋 = 𝑌)))
Theorem	pltnle 18259	"Less than" implies not converse "less than or equal to". (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 ≤ 𝑋)
Theorem	pltval3 18260	Alternate expression for the "less than" relation. (dfpss3 4041 analog.) (Contributed by NM, 4-Nov-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋)))
Theorem	pltnlt 18261	The less-than relation implies the negation of its inverse. (Contributed by NM, 18-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 < 𝑋)
Theorem	pltn2lp 18262	The less-than relation has no 2-cycle loops. (pssn2lp 4056 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ¬ (𝑋 < 𝑌 ∧ 𝑌 < 𝑋))
Theorem	plttr 18263	The less-than relation is transitive. (psstr 4059 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍))
Theorem	pltletr 18264	Transitive law for chained "less than" and "less than or equal to". (psssstr 4061 analog.) (Contributed by NM, 2-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 < 𝑍))
Theorem	plelttr 18265	Transitive law for chained "less than or equal to" and "less than". (sspsstr 4060 analog.) (Contributed by NM, 2-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍))
Theorem	pospo 18266	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 18267*	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 18268*	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 18269*	Define poset join. (Contributed by NM, 12-Sep-2011.) (Revised by Mario Carneiro, 3-Nov-2015.)
⊢ join = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (lub‘𝑝)𝑧})
Definition	df-meet 18270*	Define poset meet. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 8-Sep-2018.)
⊢ meet = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧})
Theorem	lubfval 18271*	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 18272*	Domain of the least upper bound function of a poset. (Contributed by NM, 6-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝑈 = {𝑠 ∈ 𝒫 𝐵 ∣ ∃!𝑥 ∈ 𝐵 𝜓})
Theorem	lubfun 18273	The LUB is a function. (Contributed by NM, 9-Sep-2018.)
⊢ 𝑈 = (lub‘𝐾)    ⇒   ⊢ Fun 𝑈
Theorem	lubeldm 18274*	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 18275	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 18276*	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 18277*	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 18278	The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    ⇒   ⊢ (𝜑 → (𝑈‘𝑆) ∈ 𝐵)
Theorem	lubprop 18279*	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 18280	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 18281*	Lemma for lublecl 18282 and lubid 18283. (Contributed by NM, 8-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ Poset)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}𝑧 ≤ 𝑥 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤)) ↔ 𝑥 = 𝑋))
Theorem	lublecl 18282*	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 18283*	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 18284*	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 18285*	Domain of the greatest lower bound function of a poset. (Contributed by NM, 6-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝐺 = {𝑠 ∈ 𝒫 𝐵 ∣ ∃!𝑥 ∈ 𝐵 𝜓})
Theorem	glbfun 18286	The GLB is a function. (Contributed by NM, 9-Sep-2018.)
⊢ 𝐺 = (glb‘𝐾)    ⇒   ⊢ Fun 𝐺
Theorem	glbeldm 18287*	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 18288	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 18289*	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 18290*	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 18291	The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝐺)    ⇒   ⊢ (𝜑 → (𝐺‘𝑆) ∈ 𝐵)
Theorem	glbprop 18292*	Properties of greatest lower bound of a poset. (Contributed by NM, 7-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑈 = (glb‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ dom 𝑈)    ⇒   ⊢ (𝜑 → (∀𝑦 ∈ 𝑆 (𝑈‘𝑆) ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ (𝑈‘𝑆))))
Theorem	glble 18293	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 18294*	Value of join function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove joinfval2 18295 first to reduce net proof size (existence part)?
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → ∨ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦}𝑈𝑧})
Theorem	joinfval2 18295*	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 18296*	Domain of join function for a poset-type structure. (Contributed by NM, 16-Sep-2018.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → dom ∨ = {⟨𝑥, 𝑦⟩ ∣ {𝑥, 𝑦} ∈ dom 𝑈})
Theorem	joindef 18297	Two ways to say that a join is defined. (Contributed by NM, 9-Sep-2018.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ↔ {𝑋, 𝑌} ∈ dom 𝑈))
Theorem	joinval 18298	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 18299	Closure of join of elements in the domain. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )    ⇒   ⊢ (𝜑 → (𝑋 ∨ 𝑌) ∈ 𝐵)
Theorem	joindmss 18300	Subset property of domain of join. (Contributed by NM, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom ∨ ⊆ (𝐵 × 𝐵))