Home | Metamath
Proof Explorer Theorem List (p. 178 of 450) | < 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: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | latmlej12 17701 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ 𝑌) ≤ (𝑍 ∨ 𝑋)) | ||
Theorem | latmlej21 17702 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∧ 𝑋) ≤ (𝑋 ∨ 𝑍)) | ||
Theorem | latmlej22 17703 | Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∧ 𝑋) ≤ (𝑍 ∨ 𝑋)) | ||
Theorem | lubsn 17704 | The least upper bound of a singleton. (chsupsn 29190 analog.) (Contributed by NM, 20-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑈‘{𝑋}) = 𝑋) | ||
Theorem | latjass 17705 | Lattice join is associative. Lemma 2.2 in [MegPav2002] p. 362. (chjass 29310 analog.) (Contributed by NM, 17-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = (𝑋 ∨ (𝑌 ∨ 𝑍))) | ||
Theorem | latj12 17706 | Swap 1st and 2nd members of lattice join. (chj12 29311 analog.) (Contributed by NM, 4-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍)) = (𝑌 ∨ (𝑋 ∨ 𝑍))) | ||
Theorem | latj32 17707 | Swap 2nd and 3rd members of lattice join. Lemma 2.2 in [MegPav2002] p. 362. (Contributed by NM, 2-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑋 ∨ 𝑍) ∨ 𝑌)) | ||
Theorem | latj13 17708 | Swap 1st and 3rd members of lattice join. (Contributed by NM, 4-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍)) = (𝑍 ∨ (𝑌 ∨ 𝑋))) | ||
Theorem | latj31 17709 | Swap 2nd and 3rd members of lattice join. Lemma 2.2 in [MegPav2002] p. 362. (Contributed by NM, 23-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑍 ∨ 𝑌) ∨ 𝑋)) | ||
Theorem | latjrot 17710 | Rotate lattice join of 3 classes. (Contributed by NM, 23-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑍 ∨ 𝑋) ∨ 𝑌)) | ||
Theorem | latj4 17711 | Rearrangement of lattice join of 4 classes. (chj4 29312 analog.) (Contributed by NM, 14-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ (𝑍 ∨ 𝑊)) = ((𝑋 ∨ 𝑍) ∨ (𝑌 ∨ 𝑊))) | ||
Theorem | latj4rot 17712 | Rotate lattice join of 4 classes. (Contributed by NM, 11-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ (𝑍 ∨ 𝑊)) = ((𝑊 ∨ 𝑋) ∨ (𝑌 ∨ 𝑍))) | ||
Theorem | latjjdi 17713 | Lattice join distributes over itself. (Contributed by NM, 30-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍)) = ((𝑋 ∨ 𝑌) ∨ (𝑋 ∨ 𝑍))) | ||
Theorem | latjjdir 17714 | Lattice join distributes over itself. (Contributed by NM, 2-Aug-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = ((𝑋 ∨ 𝑍) ∨ (𝑌 ∨ 𝑍))) | ||
Theorem | mod1ile 17715 | The weak direction of the modular law (e.g., pmod1i 36999, atmod1i1 37008) that holds in any lattice. (Contributed by NM, 11-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ≤ 𝑍 → (𝑋 ∨ (𝑌 ∧ 𝑍)) ≤ ((𝑋 ∨ 𝑌) ∧ 𝑍))) | ||
Theorem | mod2ile 17716 | The weak direction of the modular law (e.g., pmod2iN 37000) that holds in any lattice. (Contributed by NM, 11-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑍 ≤ 𝑋 → ((𝑋 ∧ 𝑌) ∨ 𝑍) ≤ (𝑋 ∧ (𝑌 ∨ 𝑍)))) | ||
Syntax | ccla 17717 | Extend class notation with complete lattices. |
class CLat | ||
Definition | df-clat 17718 | Define the class of all complete lattices, where every subset of the base set has an LUB and a GLB. (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.) |
⊢ CLat = {𝑝 ∈ Poset ∣ (dom (lub‘𝑝) = 𝒫 (Base‘𝑝) ∧ dom (glb‘𝑝) = 𝒫 (Base‘𝑝))} | ||
Theorem | isclat 17719 | The predicate "is a complete lattice." (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ (𝐾 ∈ CLat ↔ (𝐾 ∈ Poset ∧ (dom 𝑈 = 𝒫 𝐵 ∧ dom 𝐺 = 𝒫 𝐵))) | ||
Theorem | clatpos 17720 | A complete lattice is a poset. (Contributed by NM, 8-Sep-2018.) |
⊢ (𝐾 ∈ CLat → 𝐾 ∈ Poset) | ||
Theorem | clatlem 17721 | Lemma for properties of a complete lattice. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → ((𝑈‘𝑆) ∈ 𝐵 ∧ (𝐺‘𝑆) ∈ 𝐵)) | ||
Theorem | clatlubcl 17722 | Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝑈‘𝑆) ∈ 𝐵) | ||
Theorem | clatlubcl2 17723 | Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 13-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → 𝑆 ∈ dom 𝑈) | ||
Theorem | clatglbcl 17724 | Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵) | ||
Theorem | clatglbcl2 17725 | 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 17726 | A complete lattice is a lattice. (Contributed by NM, 18-Sep-2011.) TODO: use eqrelrdv2 5668 to shorten proof and eliminate joindmss 17617 and meetdmss 17631? |
⊢ (𝐾 ∈ CLat → 𝐾 ∈ Lat) | ||
Theorem | isglbd 17727* | Properties that determine the greatest lower bound of a complete lattice. (Contributed by Mario Carneiro, 19-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝐻 ≤ 𝑦) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) → 𝑥 ≤ 𝐻) & ⊢ (𝜑 → 𝐾 ∈ CLat) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐻 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺‘𝑆) = 𝐻) | ||
Theorem | lublem 17728* | Lemma for the least upper bound properties in a complete lattice. (Contributed by NM, 19-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (∀𝑦 ∈ 𝑆 𝑦 ≤ (𝑈‘𝑆) ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → (𝑈‘𝑆) ≤ 𝑧))) | ||
Theorem | lubub 17729 | The LUB of a complete lattice subset is an upper bound. (Contributed by NM, 19-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆) → 𝑋 ≤ (𝑈‘𝑆)) | ||
Theorem | lubl 17730* | The LUB of a complete lattice subset is the least bound. (Contributed by NM, 19-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝐵) → (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 → (𝑈‘𝑆) ≤ 𝑋)) | ||
Theorem | lubss 17731 | Subset law for least upper bounds. (chsupss 29119 analog.) (Contributed by NM, 20-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇) → (𝑈‘𝑆) ≤ (𝑈‘𝑇)) | ||
Theorem | lubel 17732 | 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 17733 | The LUB of a union. (Contributed by NM, 5-Mar-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑈‘(𝑆 ∪ 𝑇)) = ((𝑈‘𝑆) ∨ (𝑈‘𝑇))) | ||
Theorem | clatglb 17734* | Properties of greatest lower bound of a complete lattice. (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (∀𝑦 ∈ 𝑆 (𝐺‘𝑆) ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ (𝐺‘𝑆)))) | ||
Theorem | clatglble 17735 | The greatest lower bound is the least element. (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑋) | ||
Theorem | clatleglb 17736* | 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 17737 | Subset law for greatest lower bound. (Contributed by Mario Carneiro, 16-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇) → (𝐺‘𝑇) ≤ (𝐺‘𝑆)) | ||
Syntax | codu 17738 | Class function defining dual orders. |
class ODual | ||
Definition | df-odu 17739 |
Define the dual of an ordered structure, which replaces the order
component of the structure with its reverse. See odubas 17743, oduleval 17741,
and oduleg 17742 for its principal properties.
EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 17798. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ ODual = (𝑤 ∈ V ↦ (𝑤 sSet 〈(le‘ndx), ◡(le‘𝑤)〉)) | ||
Theorem | oduval 17740 | Value of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ 𝐷 = (𝑂 sSet 〈(le‘ndx), ◡ ≤ 〉) | ||
Theorem | oduleval 17741 | Value of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) & ⊢ ≤ = (le‘𝑂) ⇒ ⊢ ◡ ≤ = (le‘𝐷) | ||
Theorem | oduleg 17742 | Truth of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) & ⊢ ≤ = (le‘𝑂) & ⊢ 𝐺 = (le‘𝐷) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝐺𝐵 ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | odubas 17743 | Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) & ⊢ 𝐵 = (Base‘𝑂) ⇒ ⊢ 𝐵 = (Base‘𝐷) | ||
Theorem | pospropd 17744* | 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 17745 | Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) ⇒ ⊢ (𝑂 ∈ Poset → 𝐷 ∈ Poset) | ||
Theorem | oduposb 17746 | Being a poset is a self-dual property. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) ⇒ ⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ Poset ↔ 𝐷 ∈ Poset)) | ||
Theorem | meet0 17747 | Lemma for odujoin 17752. (Contributed by Stefan O'Rear, 29-Jan-2015.) TODO (df-riota 7114 update): This proof increased from 152 bytes to 547 bytes after the df-riota 7114 change. Any way to shorten it? join0 17748 also. |
⊢ (meet‘∅) = ∅ | ||
Theorem | join0 17748 | Lemma for odumeet 17750. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ (join‘∅) = ∅ | ||
Theorem | oduglb 17749 | 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 17750 | Meets in a dual order are joins in the original. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) & ⊢ ∨ = (join‘𝑂) ⇒ ⊢ ∨ = (meet‘𝐷) | ||
Theorem | odulub 17751 | 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 17752 | Joins in a dual order are meets in the original. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) & ⊢ ∧ = (meet‘𝑂) ⇒ ⊢ ∧ = (join‘𝐷) | ||
Theorem | odulatb 17753 | Being a lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) ⇒ ⊢ (𝑂 ∈ 𝑉 → (𝑂 ∈ Lat ↔ 𝐷 ∈ Lat)) | ||
Theorem | oduclatb 17754 | Being a complete lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) ⇒ ⊢ (𝑂 ∈ CLat ↔ 𝐷 ∈ CLat) | ||
Theorem | odulat 17755 | Being a lattice is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ 𝐷 = (ODual‘𝑂) ⇒ ⊢ (𝑂 ∈ Lat → 𝐷 ∈ Lat) | ||
Theorem | poslubmo 17756* | 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 17757* | Greatest lower bounds in a poset are unique if they exist. (Contributed by NM, 20-Sep-2018.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐵 = (Base‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ 𝑆 ⊆ 𝐵) → ∃*𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥))) | ||
Theorem | poslubd 17758* | Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ≤ 𝑇) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑥 ≤ 𝑦) → 𝑇 ≤ 𝑦) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇) | ||
Theorem | poslubdg 17759* | Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ ≤ = (le‘𝐾) & ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝑈 = (lub‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ≤ 𝑇) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑥 ≤ 𝑦) → 𝑇 ≤ 𝑦) ⇒ ⊢ (𝜑 → (𝑈‘𝑆) = 𝑇) | ||
Theorem | posglbd 17760* | Properties which determine the greatest lower bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ ≤ = (le‘𝐾) & ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐺 = (glb‘𝐾)) & ⊢ (𝜑 → 𝐾 ∈ Poset) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑇 ≤ 𝑥) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑦 ≤ 𝑥) → 𝑦 ≤ 𝑇) ⇒ ⊢ (𝜑 → (𝐺‘𝑆) = 𝑇) | ||
Syntax | cipo 17761 | Class function defining inclusion posets. |
class toInc | ||
Definition | df-ipo 17762* |
For any family of sets, define the poset of that family ordered by
inclusion. See ipobas 17765, ipolerval 17766, and ipole 17768 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 17763 | The structure of df-ipo 17762 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 17764* | 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 17765 | 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 17766* | Relation of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐹) ⇒ ⊢ (𝐹 ∈ 𝑉 → {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦)} = (le‘𝐼)) | ||
Theorem | ipotset 17767 | Topology of the inclusion poset. (Contributed by Mario Carneiro, 24-Oct-2015.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ (𝐹 ∈ 𝑉 → (ordTop‘ ≤ ) = (TopSet‘𝐼)) | ||
Theorem | ipole 17768 | Weak order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ ≤ = (le‘𝐼) ⇒ ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑋 ≤ 𝑌 ↔ 𝑋 ⊆ 𝑌)) | ||
Theorem | ipolt 17769 | Strict order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐹) & ⊢ < = (lt‘𝐼) ⇒ ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝐹 ∧ 𝑌 ∈ 𝐹) → (𝑋 < 𝑌 ↔ 𝑋 ⊊ 𝑌)) | ||
Theorem | ipopos 17770 | The inclusion poset on a family of sets is actually a poset. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐹) ⇒ ⊢ 𝐼 ∈ Poset | ||
Theorem | isipodrs 17771* | Condition for a family of sets to be directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ ((toInc‘𝐴) ∈ Dirset ↔ (𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∪ 𝑦) ⊆ 𝑧)) | ||
Theorem | ipodrscl 17772 | Direction by inclusion as used here implies sethood. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ ((toInc‘𝐴) ∈ Dirset → 𝐴 ∈ V) | ||
Theorem | ipodrsfi 17773* | Finite upper bound property for directed collections of sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (((toInc‘𝐴) ∈ Dirset ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → ∃𝑧 ∈ 𝐴 ∪ 𝑋 ⊆ 𝑧) | ||
Theorem | fpwipodrs 17774 | The finite subsets of any set are directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (toInc‘(𝒫 𝐴 ∩ Fin)) ∈ Dirset) | ||
Theorem | ipodrsima 17775* | The monotone image of a directed set. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (𝜑 → 𝐹 Fn 𝒫 𝐴) & ⊢ ((𝜑 ∧ (𝑢 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝐴)) → (𝐹‘𝑢) ⊆ (𝐹‘𝑣)) & ⊢ (𝜑 → (toInc‘𝐵) ∈ Dirset) & ⊢ (𝜑 → 𝐵 ⊆ 𝒫 𝐴) & ⊢ (𝜑 → (𝐹 “ 𝐵) ∈ 𝑉) ⇒ ⊢ (𝜑 → (toInc‘(𝐹 “ 𝐵)) ∈ Dirset) | ||
Theorem | isacs3lem 17776* | An algebraic closure system satisfies isacs3 17784. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ (𝐶 ∈ (ACS‘𝑋) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠 ∈ 𝐶))) | ||
Theorem | acsdrsel 17777 | An algebraic closure system contains all directed unions of closed sets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑌 ⊆ 𝐶 ∧ (toInc‘𝑌) ∈ Dirset) → ∪ 𝑌 ∈ 𝐶) | ||
Theorem | isacs4lem 17778* | 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 17779* | 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 17780 | In an algebraic closure system, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑌 ⊆ 𝒫 𝑋 ∧ (toInc‘𝑌) ∈ Dirset) → (𝐹‘∪ 𝑌) = ∪ (𝐹 “ 𝑌)) | ||
Theorem | acsficl 17781 | 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 17782* | 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 17783* | 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 17784* | 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 17785 | In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 17781. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑁‘𝑆) = ∪ (𝑁 “ (𝒫 𝑆 ∩ Fin))) | ||
Theorem | acsficl2d 17786* | 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 17781. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑌 ∈ (𝑁‘𝑆) ↔ ∃𝑥 ∈ (𝒫 𝑆 ∩ Fin)𝑌 ∈ (𝑁‘𝑥))) | ||
Theorem | acsfiindd 17787 | 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 17788* | 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 17786 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 17789* | 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 17788 and observing that, since 𝑆 and 𝑇 have the same closure, the closure of ∪ ran 𝑓 must contain 𝑆. Since 𝑆 is independent, by mrissmrcd 16911, ∪ 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 17790 | In an algebraic closure system, if 𝑆 and 𝑇 have the same closure and 𝑆 is infinite independent, then 𝑇 is infinite. This follows from applying unirnffid 8816 to the map given in acsmap2d 17789. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑇 ⊆ 𝑋) & ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇)) & ⊢ (𝜑 → ¬ 𝑆 ∈ Fin) ⇒ ⊢ (𝜑 → ¬ 𝑇 ∈ Fin) | ||
Theorem | acsdomd 17791 | In an algebraic closure system, if 𝑆 and 𝑇 have the same closure and 𝑆 is infinite independent, then 𝑇 dominates 𝑆. This follows from applying acsinfd 17790 and then applying unirnfdomd 9989 to the map given in acsmap2d 17789. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑇 ⊆ 𝑋) & ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇)) & ⊢ (𝜑 → ¬ 𝑆 ∈ Fin) ⇒ ⊢ (𝜑 → 𝑆 ≼ 𝑇) | ||
Theorem | acsinfdimd 17792 | 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 17791 twice with acsinfd 17790. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑇 ∈ 𝐼) & ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇)) & ⊢ (𝜑 → ¬ 𝑆 ∈ Fin) ⇒ ⊢ (𝜑 → 𝑆 ≈ 𝑇) | ||
Theorem | acsexdimd 17793* | In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 16921 for the finite case and acsinfdimd 17792 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 17794 | Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐼 = (toInc‘𝐶) & ⊢ 𝐺 = (glb‘𝐼) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅) → (𝐺‘𝑈) = ∩ 𝑈) | ||
Theorem | mrelatglb0 17795 | 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 17796 | 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 17797* | A Moore space is a complete lattice under inclusion. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 7114 update): Reprove using isclat 17719 instead of the isclatBAD. hypothesis. See commented-out mreclat above. |
⊢ 𝐼 = (toInc‘𝐶) & ⊢ (𝐼 ∈ CLat ↔ (𝐼 ∈ Poset ∧ ∀𝑥(𝑥 ⊆ (Base‘𝐼) → (((lub‘𝐼)‘𝑥) ∈ (Base‘𝐼) ∧ ((glb‘𝐼)‘𝑥) ∈ (Base‘𝐼))))) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐼 ∈ CLat) | ||
Theorem | latmass 17798 | Lattice meet is associative. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = (𝑋 ∧ (𝑌 ∧ 𝑍))) | ||
Theorem | latdisdlem 17799* | Lemma for latdisd 17800. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (𝐾 ∈ Lat → (∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑢 ∨ (𝑣 ∧ 𝑤)) = ((𝑢 ∨ 𝑣) ∧ (𝑢 ∨ 𝑤)) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | ||
Theorem | latdisd 17800* | 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 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∨ (𝑦 ∧ 𝑧)) = ((𝑥 ∨ 𝑦) ∧ (𝑥 ∨ 𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |