![]() |
Metamath
Proof Explorer Theorem List (p. 175 of 443) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28474) |
![]() (28475-29999) |
![]() (30000-44279) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | prstr 17401 | "Less than or equal to" is transitive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Proset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍)) → 𝑋 ≤ 𝑍) | ||
Theorem | isdrs 17402* | Property of being a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧))) | ||
Theorem | drsdir 17403* | Direction of a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Dirset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ∃𝑧 ∈ 𝐵 (𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧)) | ||
Theorem | drsprs 17404 | A directed set is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐾 ∈ Dirset → 𝐾 ∈ Proset ) | ||
Theorem | drsbn0 17405 | The base of a directed set is not empty. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) ⇒ ⊢ (𝐾 ∈ Dirset → 𝐵 ≠ ∅) | ||
Theorem | drsdirfi 17406* | Any finite number of elements in a directed set have a common upper bound. Here is where the nonemptiness constraint in df-drs 17397 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 17407* | 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)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦)) | ||
Syntax | cpo 17408 | Extend class notation with the class of posets. |
class Poset | ||
Syntax | cplt 17409 | Extend class notation with less-than for posets. |
class lt | ||
Syntax | club 17410 | Extend class notation with poset least upper bound. |
class lub | ||
Syntax | cglb 17411 | Extend class notation with poset greatest lower bound. |
class glb | ||
Syntax | cjn 17412 | Extend class notation with poset join. |
class join | ||
Syntax | cmee 17413 | Extend class notation with poset meet. |
class meet | ||
Definition | df-poset 17414* |
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 us 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 3465 and related theorems. (Contributed by NM, 18-Oct-2012.) |
⊢ Poset = {𝑓 ∣ ∃𝑏∃𝑟(𝑏 = (Base‘𝑓) ∧ 𝑟 = (le‘𝑓) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))} | ||
Theorem | ispos 17415* | The predicate "is a poset." (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 4-Nov-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) | ||
Theorem | ispos2 17416* |
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 17417 | A poset is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset ) | ||
Theorem | posi 17418 | Lemma for poset properties. (Contributed by NM, 11-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑋 ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍))) | ||
Theorem | posref 17419 | A poset ordering is reflexive. (Contributed by NM, 11-Sep-2011.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 𝑋) | ||
Theorem | posasymb 17420 | A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌)) | ||
Theorem | postr 17421 | A poset ordering is transitive. (Contributed by NM, 11-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 ≤ 𝑍)) | ||
Theorem | 0pos 17422 | Technical lemma to simplify the statement of ipopos 17628. The empty set is (rather pathologically) a poset under our definitions, since it has an empty base set (str0 16391) and any relation partially orders an empty set. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ ∅ ∈ Poset | ||
Theorem | isposd 17423* | Properties that determine a poset (implicit structure version). (Contributed by Mario Carneiro, 29-Apr-2014.) |
⊢ (𝜑 → 𝐾 ∈ V) & ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → ≤ = (le‘𝐾)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ≤ 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ⇒ ⊢ (𝜑 → 𝐾 ∈ Poset) | ||
Theorem | isposi 17424* | Properties that determine a poset (implicit structure version). (Contributed by NM, 11-Sep-2011.) |
⊢ 𝐾 ∈ V & ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ (𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ⇒ ⊢ 𝐾 ∈ Poset | ||
Theorem | isposix 17425* | 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.) |
⊢ 𝐵 ∈ V & ⊢ ≤ ∈ V & ⊢ 𝐾 = {〈(Base‘ndx), 𝐵〉, 〈(le‘ndx), ≤ 〉} & ⊢ (𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ⇒ ⊢ 𝐾 ∈ Poset | ||
Definition | df-plt 17426 | Define less-than ordering for posets and related structures. Unlike df-base 16345 and df-ple 16441, 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 17427 | Value of the less-than relation. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → < = ( ≤ ∖ I )) | ||
Theorem | pltval 17428 | Less-than relation. (df-pss 3845 analog.) (Contributed by NM, 12-Oct-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌))) | ||
Theorem | pltle 17429 | "Less than" implies "less than or equal to". (pssss 3962 analog.) (Contributed by NM, 4-Dec-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≤ 𝑌)) | ||
Theorem | pltne 17430 | The "less than" relation is not reflexive. (df-pss 3845 analog.) (Contributed by NM, 2-Dec-2011.) |
⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶) → (𝑋 < 𝑌 → 𝑋 ≠ 𝑌)) | ||
Theorem | pltirr 17431 | The "less than" relation is not reflexive. (pssirr 3967 analog.) (Contributed by NM, 7-Feb-2012.) |
⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ¬ 𝑋 < 𝑋) | ||
Theorem | pleval2i 17432 | One direction of pleval2 17433. (Contributed by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 < 𝑌 ∨ 𝑋 = 𝑌))) | ||
Theorem | pleval2 17433 | "Less than or equal to" in terms of "less than". (sspss 3966 analog.) (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 8-Feb-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑋 < 𝑌 ∨ 𝑋 = 𝑌))) | ||
Theorem | pltnle 17434 | "Less than" implies not converse "less than or equal to". (Contributed by NM, 18-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 ≤ 𝑋) | ||
Theorem | pltval3 17435 | Alternate expression for the "less than" relation. (dfpss3 3953 analog.) (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋))) | ||
Theorem | pltnlt 17436 | The less-than relation implies the negation of its inverse. (Contributed by NM, 18-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ¬ 𝑌 < 𝑋) | ||
Theorem | pltn2lp 17437 | The less-than relation has no 2-cycle loops. (pssn2lp 3968 analog.) (Contributed by NM, 2-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ¬ (𝑋 < 𝑌 ∧ 𝑌 < 𝑋)) | ||
Theorem | plttr 17438 | The less-than relation is transitive. (psstr 3971 analog.) (Contributed by NM, 2-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍)) | ||
Theorem | pltletr 17439 | Transitive law for chained "less than" and "less than or equal to". (psssstr 3973 analog.) (Contributed by NM, 2-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 < 𝑍)) | ||
Theorem | plelttr 17440 | Transitive law for chained "less than or equal to" and "less than". (sspsstr 3972 analog.) (Contributed by NM, 2-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑌 < 𝑍) → 𝑋 < 𝑍)) | ||
Theorem | pospo 17441 | 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 17442* | 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 17443* | 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 17444* | Define poset join. (Contributed by NM, 12-Sep-2011.) (Revised by Mario Carneiro, 3-Nov-2015.) |
⊢ join = (𝑝 ∈ V ↦ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (lub‘𝑝)𝑧}) | ||
Definition | df-meet 17445* | Define poset join. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 8-Sep-2018.) |
⊢ meet = (𝑝 ∈ V ↦ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧}) | ||
Theorem | lubfval 17446* | 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 17447* | Domain of the least upper bound function of a poset. (Contributed by NM, 6-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧))) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝑈 = {𝑠 ∈ 𝒫 𝐵 ∣ ∃!𝑥 ∈ 𝐵 𝜓}) | ||
Theorem | lubfun 17448 | The LUB is a function. (Contributed by NM, 9-Sep-2018.) |
⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ Fun 𝑈 | ||
Theorem | lubeldm 17449* | 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 17450 | 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 17451* | 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 17452* | 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 17453 | The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ dom 𝑈) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) ∈ 𝐵) | ||
Theorem | lubprop 17454* | 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 17455 | 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 17456* | Lemma for lublecl 17457 and lubid 17458. (Contributed by NM, 8-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}𝑧 ≤ 𝑥 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋}𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤)) ↔ 𝑥 = 𝑋)) | ||
Theorem | lublecl 17457* | 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 17458* | 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 17459* | 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 17460* | Domain of the greatest lower bound function of a poset. (Contributed by NM, 6-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ (𝜓 ↔ (∀𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥))) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom 𝐺 = {𝑠 ∈ 𝒫 𝐵 ∣ ∃!𝑥 ∈ 𝐵 𝜓}) | ||
Theorem | glbfun 17461 | The GLB is a function. (Contributed by NM, 9-Sep-2018.) |
⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ Fun 𝐺 | ||
Theorem | glbeldm 17462* | 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 17463 | 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 17464* | 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 17465* | 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 17466 | The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ dom 𝐺) ⇒ ⊢ (𝜑 → (𝐺‘𝑆) ∈ 𝐵) | ||
Theorem | glbprop 17467* | Properties of greatest lower bound of a poset. (Contributed by NM, 7-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (glb‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ dom 𝑈) ⇒ ⊢ (𝜑 → (∀𝑦 ∈ 𝑆 (𝑈‘𝑆) ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ (𝑈‘𝑆)))) | ||
Theorem | glble 17468 | 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 17469* | Value of join function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove joinfval2 17470 first to reduce net proof size (existence part)? |
⊢ 𝑈 = (lub‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → ∨ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝑈𝑧}) | ||
Theorem | joinfval2 17470* | 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 17471* | Domain of join function for a poset-type structure. (Contributed by NM, 16-Sep-2018.) |
⊢ 𝑈 = (lub‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → dom ∨ = {〈𝑥, 𝑦〉 ∣ {𝑥, 𝑦} ∈ dom 𝑈}) | ||
Theorem | joindef 17472 | Two ways to say that a join is defined. (Contributed by NM, 9-Sep-2018.) |
⊢ 𝑈 = (lub‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → 𝑌 ∈ 𝑍) ⇒ ⊢ (𝜑 → (〈𝑋, 𝑌〉 ∈ dom ∨ ↔ {𝑋, 𝑌} ∈ dom 𝑈)) | ||
Theorem | joinval 17473 | 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 17474 | Closure of join of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∨ ) ⇒ ⊢ (𝜑 → (𝑋 ∨ 𝑌) ∈ 𝐵) | ||
Theorem | joindmss 17475 | Subset property of domain of join. (Contributed by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom ∨ ⊆ (𝐵 × 𝐵)) | ||
Theorem | joinval2lem 17476* | Lemma for joinval2 17477 and joineu 17478. (Contributed by NM, 12-Sep-2018.) TODO: combine this through joineu 17478 into joinlem 17479? |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((∀𝑦 ∈ {𝑋, 𝑌}𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ {𝑋, 𝑌}𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)) ↔ ((𝑋 ≤ 𝑥 ∧ 𝑌 ≤ 𝑥) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) | ||
Theorem | joinval2 17477* | 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 17478* | Uniqueness of join of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∨ ) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝐵 ((𝑋 ≤ 𝑥 ∧ 𝑌 ≤ 𝑥) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → 𝑥 ≤ 𝑧))) | ||
Theorem | joinlem 17479* | Lemma for join properties. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∨ ) ⇒ ⊢ (𝜑 → ((𝑋 ≤ (𝑋 ∨ 𝑌) ∧ 𝑌 ≤ (𝑋 ∨ 𝑌)) ∧ ∀𝑧 ∈ 𝐵 ((𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧) → (𝑋 ∨ 𝑌) ≤ 𝑧))) | ||
Theorem | lejoin1 17480 | 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 17481 | 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 17482 | 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 17483* | Value of meet function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) TODO: prove meetfval2 17484 first to reduce net proof size (existence part)? |
⊢ 𝐺 = (glb‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → ∧ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ {𝑥, 𝑦}𝐺𝑧}) | ||
Theorem | meetfval2 17484* | Value of meet function for a poset. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 9-Sep-2018.) |
⊢ 𝐺 = (glb‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → ∧ = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ({𝑥, 𝑦} ∈ dom 𝐺 ∧ 𝑧 = (𝐺‘{𝑥, 𝑦}))}) | ||
Theorem | meetdm 17485* | Domain of meet function for a poset-type structure. (Contributed by NM, 16-Sep-2018.) |
⊢ 𝐺 = (glb‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → dom ∧ = {〈𝑥, 𝑦〉 ∣ {𝑥, 𝑦} ∈ dom 𝐺}) | ||
Theorem | meetdef 17486 | Two ways to say that a meet is defined. (Contributed by NM, 9-Sep-2018.) |
⊢ 𝐺 = (glb‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → 𝑌 ∈ 𝑍) ⇒ ⊢ (𝜑 → (〈𝑋, 𝑌〉 ∈ dom ∧ ↔ {𝑋, 𝑌} ∈ dom 𝐺)) | ||
Theorem | meetval 17487 | 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 17488 | Closure of meet of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∧ ) ⇒ ⊢ (𝜑 → (𝑋 ∧ 𝑌) ∈ 𝐵) | ||
Theorem | meetdmss 17489 | Subset property of domain of meet. (Contributed by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) ⇒ ⊢ (𝜑 → dom ∧ ⊆ (𝐵 × 𝐵)) | ||
Theorem | meetval2lem 17490* | Lemma for meetval2 17491 and meeteu 17492. (Contributed by NM, 12-Sep-2018.) TODO: combine this through meeteu 17492 into meetlem 17493? |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((∀𝑦 ∈ {𝑋, 𝑌}𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ {𝑋, 𝑌}𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)) ↔ ((𝑥 ≤ 𝑋 ∧ 𝑥 ≤ 𝑌) ∧ ∀𝑧 ∈ 𝐵 ((𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌) → 𝑧 ≤ 𝑥)))) | ||
Theorem | meetval2 17491* | 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 17492* | Uniqueness of meet of elements in the domain. (Contributed by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∧ ) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝐵 ((𝑥 ≤ 𝑋 ∧ 𝑥 ≤ 𝑌) ∧ ∀𝑧 ∈ 𝐵 ((𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌) → 𝑧 ≤ 𝑥))) | ||
Theorem | meetlem 17493* | Lemma for meet properties. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ dom ∧ ) ⇒ ⊢ (𝜑 → (((𝑋 ∧ 𝑌) ≤ 𝑋 ∧ (𝑋 ∧ 𝑌) ≤ 𝑌) ∧ ∀𝑧 ∈ 𝐵 ((𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌) → 𝑧 ≤ (𝑋 ∧ 𝑌)))) | ||
Theorem | lemeet1 17494 | 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 17495 | 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 17496 | 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 17497 | The join of a poset commutes. (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 17498 | The join of a poset commutes. (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 17499 | The meet of a poset commutes. (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 17500 | The meet of a poset commutes. (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 ∧ )) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |