![]() |
Metamath
Proof Explorer Theorem List (p. 176 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | clatglbcl2 17501 | Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 13-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → 𝑆 ∈ dom 𝐺) | ||
Theorem | clatl 17502 | A complete lattice is a lattice. (Contributed by NM, 18-Sep-2011.) TODO: use eqrelrdv2 5466 to shorten proof and eliminate joindmss 17393 and meetdmss 17407? |
⊢ (𝐾 ∈ CLat → 𝐾 ∈ Lat) | ||
Theorem | isglbd 17503* | Properties that determine the greatest lower bound of a complete lattice. (Contributed by Mario Carneiro, 19-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝐻 ≤ 𝑦) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → 𝑥 ≤ 𝐻) & ⊢ (𝜑 → 𝐾 ∈ CLat) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐻 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺‘𝑆) = 𝐻) | ||
Theorem | lublem 17504* | Lemma for the least upper bound properties in a complete lattice. (Contributed by NM, 19-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (∀𝑦 ∈ 𝑆 𝑦 ≤ (𝑈‘𝑆) ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → (𝑈‘𝑆) ≤ 𝑧))) | ||
Theorem | lubub 17505 | The LUB of a complete lattice subset is an upper bound. (Contributed by NM, 19-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆) → 𝑋 ≤ (𝑈‘𝑆)) | ||
Theorem | lubl 17506* | The LUB of a complete lattice subset is the least bound. (Contributed by NM, 19-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝐵) → (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 → (𝑈‘𝑆) ≤ 𝑋)) | ||
Theorem | lubss 17507 | Subset law for least upper bounds. (chsupss 28773 analog.) (Contributed by NM, 20-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇) → (𝑈‘𝑆) ≤ (𝑈‘𝑇)) | ||
Theorem | lubel 17508 | An element of a set is less than or equal to the least upper bound of the set. (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝑆 ∧ 𝑆 ⊆ 𝐵) → 𝑋 ≤ (𝑈‘𝑆)) | ||
Theorem | lubun 17509 | The LUB of a union. (Contributed by NM, 5-Mar-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑈‘(𝑆 ∪ 𝑇)) = ((𝑈‘𝑆) ∨ (𝑈‘𝑇))) | ||
Theorem | clatglb 17510* | Properties of greatest lower bound of a complete lattice. (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (∀𝑦 ∈ 𝑆 (𝐺‘𝑆) ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ (𝐺‘𝑆)))) | ||
Theorem | clatglble 17511 | The greatest lower bound is the least element. (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑋) | ||
Theorem | clatleglb 17512* | Two ways of expressing "less than or equal to the greatest lower bound." (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → (𝑋 ≤ (𝐺‘𝑆) ↔ ∀𝑦 ∈ 𝑆 𝑋 ≤ 𝑦)) | ||
Theorem | clatglbss 17513 | Subset law for greatest lower bound. (Contributed by Mario Carneiro, 16-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇) → (𝐺‘𝑇) ≤ (𝐺‘𝑆)) | ||
Syntax | codu 17514 | Class function defining dual orders. |
class ODual | ||
Definition | df-odu 17515 |
Define the dual of an ordered structure, which replaces the order
component of the structure with its reverse. See odubas 17519, oduleval 17517,
and oduleg 17518 for its principal properties.
EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 17574. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ ODual = (𝑤 ∈ V ↦ (𝑤 sSet 〈(le‘ndx), ◡(le‘𝑤)〉)) | ||
Theorem | oduval 17516 | Value of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ 𝐷 = (𝑂 sSet 〈(le‘ndx), ◡ ≤ 〉) | ||
Theorem | oduleval 17517 | Value of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ ◡ ≤ = (le‘𝐷) | ||
Theorem | oduleg 17518 | Truth of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) & ⊢ ≤ = (le‘𝑂) & ⊢ 𝐺 = (le‘𝐷) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝐺𝐵 ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | odubas 17519 | Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) & ⊢ 𝐵 = (Base‘𝑂) ⇒ ⊢ 𝐵 = (Base‘𝐷) | ||
Theorem | pospropd 17520* | 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 17521 | Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) ⇒ ⊢ (𝑂 ∈ Poset → 𝐷 ∈ Poset) | ||
Theorem | oduposb 17522 | Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) ⇒ ⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ Poset ↔ 𝐷 ∈ Poset)) | ||
Theorem | meet0 17523 | Lemma for odujoin 17528. (Contributed by Stefan O'Rear, 29-Jan-2015.) TODO (df-riota 6883 update): This proof increased from 152 bytes to 547 bytes after the df-riota 6883 change. Any way to shorten it? join0 17524 also. |
⊢ (meet‘∅) = ∅ | ||
Theorem | join0 17524 | Lemma for odumeet 17526. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ (join‘∅) = ∅ | ||
Theorem | oduglb 17525 | 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 17526 | Meets in a dual order are joins in the original. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) & ⊢ ∨ = (join‘𝑂) ⇒ ⊢ ∨ = (meet‘𝐷) | ||
Theorem | odulub 17527 | 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 17528 | Joins in a dual order are meets in the original. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) & ⊢ ∧ = (meet‘𝑂) ⇒ ⊢ ∧ = (join‘𝐷) | ||
Theorem | odulatb 17529 | Being a lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) ⇒ ⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ Lat ↔ 𝐷 ∈ Lat)) | ||
Theorem | oduclatb 17530 | Being a complete lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) ⇒ ⊢ (𝑂 ∈ CLat ↔ 𝐷 ∈ CLat) | ||
Theorem | odulat 17531 | Being a lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) ⇒ ⊢ (𝑂 ∈ Lat → 𝐷 ∈ Lat) | ||
Theorem | poslubmo 17532* | 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 17533* | Greatest lower bounds in a poset are unique if they exist. (Contributed by NM, 20-Sep-2018.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐵 = (Base‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵) → ∃*𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥))) | ||
Theorem | poslubd 17534* | Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ≤ 𝑇) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑥 ≤ 𝑦) → 𝑇 ≤ 𝑦) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇) | ||
Theorem | poslubdg 17535* | Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ ≤ = (le‘𝐾) & ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝑈 = (lub‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ≤ 𝑇) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑥 ≤ 𝑦) → 𝑇 ≤ 𝑦) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇) | ||
Theorem | posglbd 17536* | Properties which determine the greatest lower bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ ≤ = (le‘𝐾) & ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐺 = (glb‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑇 ≤ 𝑥) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑦 ≤ 𝑥) → 𝑦 ≤ 𝑇) ⇒ ⊢ (𝜑 → (𝐺‘𝑆) = 𝑇) | ||
Syntax | cipo 17537 | Class function defining inclusion posets. |
class toInc | ||
Definition | df-ipo 17538* |
For any family of sets, define the poset of that family ordered by
inclusion. See ipobas 17541, ipolerval 17542, and ipole 17544 for its contract.
EDITORIAL: I'm not thrilled with the name. Any suggestions? (Contributed by Stefan O'Rear, 30-Jan-2015.) (New usage is discouraged.) |
⊢ toInc = (𝑓 ∈ V ↦ ⦋{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦)} / 𝑜⦌({〈(Base‘ndx), 𝑓〉, 〈(TopSet‘ndx), (ordTop‘𝑜)〉} ∪ {〈(le‘ndx), 𝑜〉, 〈(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})〉})) | ||
Theorem | ipostr 17539 | The structure of df-ipo 17538 is a structure defining indices up to 11. (Contributed by Mario Carneiro, 25-Oct-2015.) |
⊢ ({〈(Base‘ndx), 𝐵〉, 〈(TopSet‘ndx), 𝐽〉} ∪ {〈(le‘ndx), ≤ 〉, 〈(oc‘ndx), ⊥ 〉}) Struct 〈1, ;11〉 | ||
Theorem | ipoval 17540* | Value of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ ≤ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦)} ⇒ ⊢ (𝐹 ∈ 𝑉 → 𝐼 = ({〈(Base‘ndx), 𝐹〉, 〈(TopSet‘ndx), (ordTop‘ ≤ )〉} ∪ {〈(le‘ndx), ≤ 〉, 〈(oc‘ndx), (𝑥 ∈ 𝐹 ↦ ∪ {𝑦 ∈ 𝐹 ∣ (𝑦 ∩ 𝑥) = ∅})〉})) | ||
Theorem | ipobas 17541 | Base set of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by Mario Carneiro, 25-Oct-2015.) |
⊢ 𝐼 = (toInc‘𝐹) ⇒ ⊢ (𝐹 ∈ 𝑉 → 𝐹 = (Base‘𝐼)) | ||
Theorem | ipolerval 17542* | Relation of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐹) ⇒ ⊢ (𝐹 ∈ 𝑉 → {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦)} = (le‘𝐼)) | ||
Theorem | ipotset 17543 | Topology of the inclusion poset. (Contributed by Mario Carneiro, 24-Oct-2015.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ (𝐹 ∈ 𝑉 → (ordTop‘ ≤ ) = (TopSet‘𝐼)) | ||
Theorem | ipole 17544 | Weak order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑋 ≤ 𝑌 ↔ 𝑋 ⊆ 𝑌)) | ||
Theorem | ipolt 17545 | Strict order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ < = (lt‘𝐼) ⇒ ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑋 < 𝑌 ↔ 𝑋 ⊊ 𝑌)) | ||
Theorem | ipopos 17546 | The inclusion poset on a family of sets is actually a poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐹) ⇒ ⊢ 𝐼 ∈ Poset | ||
Theorem | isipodrs 17547* | Condition for a family of sets to be directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ ((toInc‘𝐴) ∈ Dirset ↔ (𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧)) | ||
Theorem | ipodrscl 17548 | Direction by inclusion as used here implies sethood. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ ((toInc‘𝐴) ∈ Dirset → 𝐴 ∈ V) | ||
Theorem | ipodrsfi 17549* | Finite upper bound property for directed collections of sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (((toInc‘𝐴) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → ∃𝑧 ∈ 𝐴 ∪ 𝑋 ⊆ 𝑧) | ||
Theorem | fpwipodrs 17550 | The finite subsets of any set are directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (toInc‘(𝒫 𝐴 ∩ Fin)) ∈ Dirset) | ||
Theorem | ipodrsima 17551* | The monotone image of a directed set. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (𝜑 → 𝐹 Fn 𝒫 𝐴) & ⊢ ((𝜑 ∧ (𝑢 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝐴)) → (𝐹‘𝑢) ⊆ (𝐹‘𝑣)) & ⊢ (𝜑 → (toInc‘𝐵) ∈ Dirset) & ⊢ (𝜑 → 𝐵 ⊆ 𝒫 𝐴) & ⊢ (𝜑 → (𝐹 “ 𝐵) ∈ 𝑉) ⇒ ⊢ (𝜑 → (toInc‘(𝐹 “ 𝐵)) ∈ Dirset) | ||
Theorem | isacs3lem 17552* | An algebraic closure system satisfies isacs3 17560. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠 ∈ 𝐶))) | ||
Theorem | acsdrsel 17553 | An algebraic closure system contains all directed unions of closed sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑌 ⊆ 𝐶 ∧ (toInc‘𝑌) ∈ Dirset) → ∪ 𝑌 ∈ 𝐶) | ||
Theorem | isacs4lem 17554* | In a closure system in which directed unions of closed sets are closed, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠 ∈ 𝐶)) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫 𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) = ∪ (𝐹 “ 𝑡)))) | ||
Theorem | isacs5lem 17555* | If closure commutes with directed unions, then the closure of a set is the closure of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫 𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) = ∪ (𝐹 “ 𝑡))) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝐹‘𝑠) = ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)))) | ||
Theorem | acsdrscl 17556 | In an algebraic closure system, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑌 ⊆ 𝒫 𝑋 ∧ (toInc‘𝑌) ∈ Dirset) → (𝐹‘∪ 𝑌) = ∪ (𝐹 “ 𝑌)) | ||
Theorem | acsficl 17557 | A closure in an algebraic closure system is the union of the closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝐹‘𝑆) = ∪ (𝐹 “ (𝒫 𝑆 ∩ Fin))) | ||
Theorem | isacs5 17558* | A closure system is algebraic iff the closure of a generating set is the union of the closures of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝐹‘𝑠) = ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)))) | ||
Theorem | isacs4 17559* | A closure system is algebraic iff closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝒫 𝑋((toInc‘𝑠) ∈ Dirset → (𝐹‘∪ 𝑠) = ∪ (𝐹 “ 𝑠)))) | ||
Theorem | isacs3 17560* | A closure system is algebraic iff directed unions of closed sets are closed. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠 ∈ 𝐶))) | ||
Theorem | acsficld 17561 | In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 17557. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑁‘𝑆) = ∪ (𝑁 “ (𝒫 𝑆 ∩ Fin))) | ||
Theorem | acsficl2d 17562* | In an algebraic closure system, an element is in the closure of a set if and only if it is in the closure of a finite subset. Alternate form of acsficl 17557. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑌 ∈ (𝑁‘𝑆) ↔ ∃𝑥 ∈ (𝒫 𝑆 ∩ Fin)𝑌 ∈ (𝑁‘𝑥))) | ||
Theorem | acsfiindd 17563 | In an algebraic closure system, a set is independent if and only if all its finite subsets are independent. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ (𝒫 𝑆 ∩ Fin) ⊆ 𝐼)) | ||
Theorem | acsmapd 17564* | In an algebraic closure system, if 𝑇 is contained in the closure of 𝑆, there is a map 𝑓 from 𝑇 into the set of finite subsets of 𝑆 such that the closure of ∪ ran 𝑓 contains 𝑇. This is proven by applying acsficl2d 17562 to each element of 𝑇. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → 𝑇 ⊆ (𝑁‘𝑆)) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ 𝑇 ⊆ (𝑁‘∪ ran 𝑓))) | ||
Theorem | acsmap2d 17565* | In an algebraic closure system, if 𝑆 and 𝑇 have the same closure and 𝑆 is independent, then there is a map 𝑓 from 𝑇 into the set of finite subsets of 𝑆 such that 𝑆 equals the union of ran 𝑓. This is proven by taking the map 𝑓 from acsmapd 17564 and observing that, since 𝑆 and 𝑇 have the same closure, the closure of ∪ ran 𝑓 must contain 𝑆. Since 𝑆 is independent, by mrissmrcd 16686, ∪ ran 𝑓 must equal 𝑆. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑇 ⊆ 𝑋) & ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇)) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ 𝑆 = ∪ ran 𝑓)) | ||
Theorem | acsinfd 17566 | In an algebraic closure system, if 𝑆 and 𝑇 have the same closure and 𝑆 is infinite independent, then 𝑇 is infinite. This follows from applying unirnffid 8546 to the map given in acsmap2d 17565. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑇 ⊆ 𝑋) & ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇)) & ⊢ (𝜑 → ¬ 𝑆 ∈ Fin) ⇒ ⊢ (𝜑 → ¬ 𝑇 ∈ Fin) | ||
Theorem | acsdomd 17567 | In an algebraic closure system, if 𝑆 and 𝑇 have the same closure and 𝑆 is infinite independent, then 𝑇 dominates 𝑆. This follows from applying acsinfd 17566 and then applying unirnfdomd 9724 to the map given in acsmap2d 17565. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑇 ⊆ 𝑋) & ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇)) & ⊢ (𝜑 → ¬ 𝑆 ∈ Fin) ⇒ ⊢ (𝜑 → 𝑆 ≼ 𝑇) | ||
Theorem | acsinfdimd 17568 | In an algebraic closure system, if two independent sets have equal closure and one is infinite, then they are equinumerous. This is proven by using acsdomd 17567 twice with acsinfd 17566. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑇 ∈ 𝐼) & ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇)) & ⊢ (𝜑 → ¬ 𝑆 ∈ Fin) ⇒ ⊢ (𝜑 → 𝑆 ≈ 𝑇) | ||
Theorem | acsexdimd 17569* | In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 16696 for the finite case and acsinfdimd 17568 for the infinite case. This is a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑇 ∈ 𝐼) & ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇)) ⇒ ⊢ (𝜑 → 𝑆 ≈ 𝑇) | ||
Theorem | mrelatglb 17570 | Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐶) & ⊢ 𝐺 = (glb‘𝐼) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅) → (𝐺‘𝑈) = ∩ 𝑈) | ||
Theorem | mrelatglb0 17571 | The empty intersection in a Moore space is realized by the base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐶) & ⊢ 𝐺 = (glb‘𝐼) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐺‘∅) = 𝑋) | ||
Theorem | mrelatlub 17572 | Least upper bounds in a Moore space are realized by the closure of the union. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐶) & ⊢ 𝐹 = (mrCls‘𝐶) & ⊢ 𝐿 = (lub‘𝐼) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶) → (𝐿‘𝑈) = (𝐹‘∪ 𝑈)) | ||
Theorem | mreclatBAD 17573* | A Moore space is a complete lattice under inclusion. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 6883 update): Reprove using isclat 17495 instead of the isclatBAD. hypothesis. See commented-out mreclat above. |
⊢ 𝐼 = (toInc‘𝐶) & ⊢ (𝐼 ∈ CLat ↔ (𝐼 ∈ Poset ∧ ∀𝑥(𝑥 ⊆ (Base‘𝐼) → (((lub‘𝐼)‘𝑥) ∈ (Base‘𝐼) ∧ ((glb‘𝐼)‘𝑥) ∈ (Base‘𝐼))))) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ CLat) | ||
Theorem | latmass 17574 | Lattice meet is associative. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = (𝑋 ∧ (𝑌 ∧ 𝑍))) | ||
Theorem | latdisdlem 17575* | Lemma for latdisd 17576. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ Lat → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑢 ∨ (𝑣 ∧ 𝑤)) = ((𝑢 ∨ 𝑣) ∧ (𝑢 ∨ 𝑤)) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | ||
Theorem | latdisd 17576* | In a lattice, joins distribute over meets if and only if meets distribute over joins; the distributive property is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ Lat → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∨ (𝑦 ∧ 𝑧)) = ((𝑥 ∨ 𝑦) ∧ (𝑥 ∨ 𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | ||
Syntax | cdlat 17577 | The class of distributive lattices. |
class DLat | ||
Definition | df-dlat 17578* | A distributive lattice is a lattice in which meets distribute over joins, or equivalently (latdisd 17576) joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ DLat = {𝑘 ∈ Lat ∣ [(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))} | ||
Theorem | isdlat 17579* | Property of being a distributive lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ DLat ↔ (𝐾 ∈ Lat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | ||
Theorem | dlatmjdi 17580 | In a distributive lattice, meets distribute over joins. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ DLat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))) | ||
Theorem | dlatl 17581 | A distributive lattice is a lattice. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ (𝐾 ∈ DLat → 𝐾 ∈ Lat) | ||
Theorem | odudlatb 17582 | The dual of a distributive lattice is a distributive lattice and conversely. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (𝐾 ∈ DLat ↔ 𝐷 ∈ DLat)) | ||
Theorem | dlatjmdi 17583 | In a distributive lattice, joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ DLat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ 𝑍))) | ||
Syntax | cps 17584 | Extend class notation with the class of all posets. |
class PosetRel | ||
Syntax | ctsr 17585 | Extend class notation with the class of all totally ordered sets. |
class TosetRel | ||
Definition | df-ps 17586 | Define the class of all posets (partially ordered sets) with weak ordering (e.g., "less than or equal to" instead of "less than"). A poset is a relation which is transitive, reflexive, and antisymmetric. (Contributed by NM, 11-May-2008.) |
⊢ PosetRel = {𝑟 ∣ (Rel 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (𝑟 ∩ ◡𝑟) = ( I ↾ ∪ ∪ 𝑟))} | ||
Definition | df-tsr 17587 | Define the class of all totally ordered sets. (Contributed by FL, 1-Nov-2009.) |
⊢ TosetRel = {𝑟 ∈ PosetRel ∣ (dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)} | ||
Theorem | isps 17588 | The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation. (Contributed by NM, 11-May-2008.) |
⊢ (𝑅 ∈ 𝐴 → (𝑅 ∈ PosetRel ↔ (Rel 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅)))) | ||
Theorem | psrel 17589 | A poset is a relation. (Contributed by NM, 12-May-2008.) |
⊢ (𝐴 ∈ PosetRel → Rel 𝐴) | ||
Theorem | psref2 17590 | A poset is antisymmetric and reflexive. (Contributed by FL, 3-Aug-2009.) |
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅)) | ||
Theorem | pstr2 17591 | A poset is transitive. (Contributed by FL, 3-Aug-2009.) |
⊢ (𝑅 ∈ PosetRel → (𝑅 ∘ 𝑅) ⊆ 𝑅) | ||
Theorem | pslem 17592 | Lemma for psref 17594 and others. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ (𝑅 ∈ PosetRel → (((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) ∧ (𝐴 ∈ ∪ ∪ 𝑅 → 𝐴𝑅𝐴) ∧ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵))) | ||
Theorem | psdmrn 17593 | The domain and range of a poset equal its field. (Contributed by NM, 13-May-2008.) |
⊢ (𝑅 ∈ PosetRel → (dom 𝑅 = ∪ ∪ 𝑅 ∧ ran 𝑅 = ∪ ∪ 𝑅)) | ||
Theorem | psref 17594 | A poset is reflexive. (Contributed by NM, 13-May-2008.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑋) → 𝐴𝑅𝐴) | ||
Theorem | psrn 17595 | The range of a poset equals it domain. (Contributed by NM, 7-Jul-2008.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ (𝑅 ∈ PosetRel → 𝑋 = ran 𝑅) | ||
Theorem | psasym 17596 | A poset is antisymmetric. (Contributed by NM, 12-May-2008.) |
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵) | ||
Theorem | pstr 17597 | A poset is transitive. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) | ||
Theorem | cnvps 17598 | The converse of a poset is a poset. In the general case (◡𝑅 ∈ PosetRel → 𝑅 ∈ PosetRel) is not true. See cnvpsb 17599 for a special case where the property holds. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝑅 ∈ PosetRel → ◡𝑅 ∈ PosetRel) | ||
Theorem | cnvpsb 17599 | The converse of a poset is a poset. (Contributed by FL, 5-Jan-2009.) |
⊢ (Rel 𝑅 → (𝑅 ∈ PosetRel ↔ ◡𝑅 ∈ PosetRel)) | ||
Theorem | psss 17600 | Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010.) |
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |