| Metamath
Proof Explorer Theorem List (p. 177 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | qusmulf 17601* | The multiplication in a quotient structure as a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
| ⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞))) & ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉) & ⊢ · = (.r‘𝑅) & ⊢ ∙ = (.r‘𝑈) ⇒ ⊢ (𝜑 → ∙ :((𝑉 / ∼ ) × (𝑉 / ∼ ))⟶(𝑉 / ∼ )) | ||
| Theorem | fnpr2o 17602 | Function with a domain of 2o. (Contributed by Jim Kingdon, 25-Sep-2023.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {〈∅, 𝐴〉, 〈1o, 𝐵〉} Fn 2o) | ||
| Theorem | fnpr2ob 17603 | Biconditional version of fnpr2o 17602. (Contributed by Jim Kingdon, 27-Sep-2023.) |
| ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ {〈∅, 𝐴〉, 〈1o, 𝐵〉} Fn 2o) | ||
| Theorem | fvpr0o 17604 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) |
| ⊢ (𝐴 ∈ 𝑉 → ({〈∅, 𝐴〉, 〈1o, 𝐵〉}‘∅) = 𝐴) | ||
| Theorem | fvpr1o 17605 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) |
| ⊢ (𝐵 ∈ 𝑉 → ({〈∅, 𝐴〉, 〈1o, 𝐵〉}‘1o) = 𝐵) | ||
| Theorem | fvprif 17606 | The value of the pair function at an element of 2o. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) → ({〈∅, 𝐴〉, 〈1o, 𝐵〉}‘𝐶) = if(𝐶 = ∅, 𝐴, 𝐵)) | ||
| Theorem | xpsfrnel 17607* | Elementhood in the target space of the function 𝐹 appearing in xpsval 17615. (Contributed by Mario Carneiro, 14-Aug-2015.) |
| ⊢ (𝐺 ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) | ||
| Theorem | xpsfeq 17608 | A function on 2o is determined by its values at zero and one. (Contributed by Mario Carneiro, 27-Aug-2015.) |
| ⊢ (𝐺 Fn 2o → {〈∅, (𝐺‘∅)〉, 〈1o, (𝐺‘1o)〉} = 𝐺) | ||
| Theorem | xpsfrnel2 17609* | Elementhood in the target space of the function 𝐹 appearing in xpsval 17615. (Contributed by Mario Carneiro, 15-Aug-2015.) |
| ⊢ ({〈∅, 𝑋〉, 〈1o, 𝑌〉} ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | xpscf 17610 | Equivalent condition for the pair function to be a proper function on 𝐴. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ ({〈∅, 𝑋〉, 〈1o, 𝑌〉}:2o⟶𝐴 ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) | ||
| Theorem | xpsfval 17611* | The value of the function appearing in xpsval 17615. (Contributed by Mario Carneiro, 15-Aug-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ⇒ ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐹𝑌) = {〈∅, 𝑋〉, 〈1o, 𝑌〉}) | ||
| Theorem | xpsff1o 17612* | The function appearing in xpsval 17615 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = {∅, 1o}. (Contributed by Mario Carneiro, 15-Aug-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ⇒ ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) | ||
| Theorem | xpsfrn 17613* | A short expression for the indexed cartesian product on two indices. (Contributed by Mario Carneiro, 15-Aug-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ⇒ ⊢ ran 𝐹 = X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) | ||
| Theorem | xpsff1o2 17614* | The function appearing in xpsval 17615 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = {∅, 1o}. (Contributed by Mario Carneiro, 24-Jan-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ⇒ ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→ran 𝐹 | ||
| Theorem | xpsval 17615* | Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) & ⊢ 𝐺 = (Scalar‘𝑅) & ⊢ 𝑈 = (𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) ⇒ ⊢ (𝜑 → 𝑇 = (◡𝐹 “s 𝑈)) | ||
| Theorem | xpsrnbas 17616* | The indexed structure product that appears in xpsval 17615 has the same base as the target of the function 𝐹. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) & ⊢ 𝐺 = (Scalar‘𝑅) & ⊢ 𝑈 = (𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) ⇒ ⊢ (𝜑 → ran 𝐹 = (Base‘𝑈)) | ||
| Theorem | xpsbas 17617 | The base set of the binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑋 × 𝑌) = (Base‘𝑇)) | ||
| Theorem | xpsaddlem 17618* | Lemma for xpsadd 17619 and xpsmul 17620. (Contributed by Mario Carneiro, 15-Aug-2015.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → (𝐴 · 𝐶) ∈ 𝑋) & ⊢ (𝜑 → (𝐵 × 𝐷) ∈ 𝑌) & ⊢ · = (𝐸‘𝑅) & ⊢ × = (𝐸‘𝑆) & ⊢ ∙ = (𝐸‘𝑇) & ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) & ⊢ 𝑈 = ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) & ⊢ ((𝜑 ∧ {〈∅, 𝐴〉, 〈1o, 𝐵〉} ∈ ran 𝐹 ∧ {〈∅, 𝐶〉, 〈1o, 𝐷〉} ∈ ran 𝐹) → ((◡𝐹‘{〈∅, 𝐴〉, 〈1o, 𝐵〉}) ∙ (◡𝐹‘{〈∅, 𝐶〉, 〈1o, 𝐷〉})) = (◡𝐹‘({〈∅, 𝐴〉, 〈1o, 𝐵〉} (𝐸‘𝑈){〈∅, 𝐶〉, 〈1o, 𝐷〉}))) & ⊢ (({〈∅, 𝑅〉, 〈1o, 𝑆〉} Fn 2o ∧ {〈∅, 𝐴〉, 〈1o, 𝐵〉} ∈ (Base‘𝑈) ∧ {〈∅, 𝐶〉, 〈1o, 𝐷〉} ∈ (Base‘𝑈)) → ({〈∅, 𝐴〉, 〈1o, 𝐵〉} (𝐸‘𝑈){〈∅, 𝐶〉, 〈1o, 𝐷〉}) = (𝑘 ∈ 2o ↦ (({〈∅, 𝐴〉, 〈1o, 𝐵〉}‘𝑘)(𝐸‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘))({〈∅, 𝐶〉, 〈1o, 𝐷〉}‘𝑘)))) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ∙ 〈𝐶, 𝐷〉) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) | ||
| Theorem | xpsadd 17619 | Value of the addition operation in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → (𝐴 · 𝐶) ∈ 𝑋) & ⊢ (𝜑 → (𝐵 × 𝐷) ∈ 𝑌) & ⊢ · = (+g‘𝑅) & ⊢ × = (+g‘𝑆) & ⊢ ∙ = (+g‘𝑇) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ∙ 〈𝐶, 𝐷〉) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) | ||
| Theorem | xpsmul 17620 | Value of the multiplication operation in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → (𝐴 · 𝐶) ∈ 𝑋) & ⊢ (𝜑 → (𝐵 × 𝐷) ∈ 𝑌) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) & ⊢ ∙ = (.r‘𝑇) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ∙ 〈𝐶, 𝐷〉) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) | ||
| Theorem | xpssca 17621 | Value of the scalar field of a binary structure product. For concreteness, we choose the scalar field to match the left argument, but in most cases where this slot is meaningful both factors will have the same scalar field, so that it doesn't matter which factor is chosen. (Contributed by Mario Carneiro, 15-Aug-2015.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝐺 = (Scalar‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐺 = (Scalar‘𝑇)) | ||
| Theorem | xpsvsca 17622 | Value of the scalar multiplication function in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝐺 = (Scalar‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ 𝐾 = (Base‘𝐺) & ⊢ · = ( ·𝑠 ‘𝑅) & ⊢ × = ( ·𝑠 ‘𝑆) & ⊢ ∙ = ( ·𝑠 ‘𝑇) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑌) & ⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑋) & ⊢ (𝜑 → (𝐴 × 𝐶) ∈ 𝑌) ⇒ ⊢ (𝜑 → (𝐴 ∙ 〈𝐵, 𝐶〉) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) | ||
| Theorem | xpsless 17623 | Closure of the ordering in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ ≤ = (le‘𝑇) ⇒ ⊢ (𝜑 → ≤ ⊆ ((𝑋 × 𝑌) × (𝑋 × 𝑌))) | ||
| Theorem | xpsle 17624 | Value of the ordering in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ ≤ = (le‘𝑇) & ⊢ 𝑀 = (le‘𝑅) & ⊢ 𝑁 = (le‘𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ≤ 〈𝐶, 𝐷〉 ↔ (𝐴𝑀𝐶 ∧ 𝐵𝑁𝐷))) | ||
| Syntax | cmre 17625 | The class of Moore systems. |
| class Moore | ||
| Syntax | cmrc 17626 | The class function generating Moore closures. |
| class mrCls | ||
| Syntax | cmri 17627 | mrInd is a class function which takes a Moore system to its set of independent sets. |
| class mrInd | ||
| Syntax | cacs 17628 | The class of algebraic closure (Moore) systems. |
| class ACS | ||
| Definition | df-mre 17629* |
Define a Moore collection, which is a family of subsets of a base set
which preserve arbitrary intersection. Elements of a Moore collection
are termed closed; Moore collections generalize the notion of
closedness from topologies (cldmre 23086) and vector spaces (lssmre 20964)
to the most general setting in which such concepts make sense.
Definition of Moore collection of sets in [Schechter] p. 78. A Moore
collection may also be called a closure system (Section 0.6 in
[Gratzer] p. 23.) The name Moore
collection is after Eliakim Hastings
Moore, who discussed these systems in Part I of [Moore] p. 53 to 76.
See ismre 17633, mresspw 17635, mre1cl 17637 and mreintcl 17638 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 17643); as such the disjoint union of all Moore collections is sometimes considered as ∪ ran Moore, justified by mreunirn 17644. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by David Moews, 1-May-2017.) |
| ⊢ Moore = (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))}) | ||
| Definition | df-mrc 17630* |
Define the Moore closure of a generating set, which is the smallest
closed set containing all generating elements. Definition of Moore
closure in [Schechter] p. 79. This
generalizes topological closure
(mrccls 23087) and linear span (mrclsp 20987).
A Moore closure operation 𝑁 is (1) extensive, i.e., 𝑥 ⊆ (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcssid 17660), (2) isotone, i.e., 𝑥 ⊆ 𝑦 implies that (𝑁‘𝑥) ⊆ (𝑁‘𝑦) for all subsets 𝑥 and 𝑦 of the base set (mrcss 17659), and (3) idempotent, i.e., (𝑁‘(𝑁‘𝑥)) = (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcidm 17662.) Operators satisfying these three properties are in bijective correspondence with Moore collections, so these properties may be used to give an alternate characterization of a Moore collection by providing a closure operation 𝑁 on the set of subsets of a given base set which satisfies (1), (2), and (3); the closed sets can be recovered as those sets which equal their closures (Section 4.5 in [Schechter] p. 82.) (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by David Moews, 1-May-2017.) |
| ⊢ mrCls = (𝑐 ∈ ∪ ran Moore ↦ (𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠})) | ||
| Definition | df-mri 17631* | In a Moore system, a set is independent if no element of the set is in the closure of the set with the element removed (Section 0.6 in [Gratzer] p. 27; Definition 4.1.1 in [FaureFrolicher] p. 83.) mrInd is a class function which takes a Moore system to its set of independent sets. (Contributed by David Moews, 1-May-2017.) |
| ⊢ mrInd = (𝑐 ∈ ∪ ran Moore ↦ {𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))}) | ||
| Definition | df-acs 17632* | An important subclass of Moore systems are those which can be interpreted as closure under some collection of operators of finite arity (the collection itself is not required to be finite). These are termed algebraic closure systems; similar to definition (A) of an algebraic closure system in [Schechter] p. 84, but to avoid the complexity of an arbitrary mixed collection of functions of various arities (especially if the axiom of infinity omex 9683 is to be avoided), we consider a single function defined on finite sets instead. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ ACS = (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))}) | ||
| Theorem | ismre 17633* | Property of being a Moore collection on some base set. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ (𝐶 ∈ (Moore‘𝑋) ↔ (𝐶 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐶 ∧ ∀𝑠 ∈ 𝒫 𝐶(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶))) | ||
| Theorem | fnmre 17634 | The Moore collection generator is a well-behaved function. Analogue for Moore collections of fntopon 22930 for topologies. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ Moore Fn V | ||
| Theorem | mresspw 17635 | A Moore collection is a subset of the power of the base set; each closed subset of the system is actually a subset of the base. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐶 ⊆ 𝒫 𝑋) | ||
| Theorem | mress 17636 | A Moore-closed subset is a subset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐶) → 𝑆 ⊆ 𝑋) | ||
| Theorem | mre1cl 17637 | In any Moore collection the base set is closed. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝑋 ∈ 𝐶) | ||
| Theorem | mreintcl 17638 | A nonempty collection of closed sets has a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ 𝐶) | ||
| Theorem | mreiincl 17639* | A nonempty indexed intersection of closed sets is closed. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐼 ≠ ∅ ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → ∩ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) | ||
| Theorem | mrerintcl 17640 | The relative intersection of a set of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
| ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶) → (𝑋 ∩ ∩ 𝑆) ∈ 𝐶) | ||
| Theorem | mreriincl 17641* | The relative intersection of a family of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
| ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → (𝑋 ∩ ∩ 𝑦 ∈ 𝐼 𝑆) ∈ 𝐶) | ||
| Theorem | mreincl 17642 | Two closed sets have a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∩ 𝐵) ∈ 𝐶) | ||
| Theorem | mreuni 17643 | Since the entire base set of a Moore collection is the greatest element of it, the base set can be recovered from a Moore collection by set union. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ (𝐶 ∈ (Moore‘𝑋) → ∪ 𝐶 = 𝑋) | ||
| Theorem | mreunirn 17644 | Two ways to express the notion of being a Moore collection on an unspecified base. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ (𝐶 ∈ ∪ ran Moore ↔ 𝐶 ∈ (Moore‘∪ 𝐶)) | ||
| Theorem | ismred 17645* | Properties that determine a Moore collection. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ (𝜑 → 𝐶 ⊆ 𝒫 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐶 ∧ 𝑠 ≠ ∅) → ∩ 𝑠 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐶 ∈ (Moore‘𝑋)) | ||
| Theorem | ismred2 17646* | Properties that determine a Moore collection, using restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
| ⊢ (𝜑 → 𝐶 ⊆ 𝒫 𝑋) & ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐶) → (𝑋 ∩ ∩ 𝑠) ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐶 ∈ (Moore‘𝑋)) | ||
| Theorem | mremre 17647 | The Moore collections of subsets of a space, viewed as a kind of subset of the power set, form a Moore collection in their own right on the power set. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
| ⊢ (𝑋 ∈ 𝑉 → (Moore‘𝑋) ∈ (Moore‘𝒫 𝑋)) | ||
| Theorem | submre 17648 | The subcollection of a closed set system below a given closed set is itself a closed set system. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
| ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) → (𝐶 ∩ 𝒫 𝐴) ∈ (Moore‘𝐴)) | ||
| Theorem | mrcflem 17649* | The domain and codomain of the function expression for Moore closures. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠}):𝒫 𝑋⟶𝐶) | ||
| Theorem | fnmrc 17650 | Moore-closure is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
| ⊢ mrCls Fn ∪ ran Moore | ||
| Theorem | mrcfval 17651* | Value of the function expression for the Moore closure. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹 = (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠})) | ||
| Theorem | mrcf 17652 | The Moore closure is a function mapping arbitrary subsets to closed sets. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝐶) | ||
| Theorem | mrcval 17653* | Evaluation of the Moore closure of a set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Proof shortened by Fan Zheng, 6-Jun-2016.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘𝑈) = ∩ {𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠}) | ||
| Theorem | mrccl 17654 | The Moore closure of a set is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘𝑈) ∈ 𝐶) | ||
| Theorem | mrcsncl 17655 | The Moore closure of a singleton is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ∈ 𝑋) → (𝐹‘{𝑈}) ∈ 𝐶) | ||
| Theorem | mrcid 17656 | The closure of a closed set is itself. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ∈ 𝐶) → (𝐹‘𝑈) = 𝑈) | ||
| Theorem | mrcssv 17657 | The closure of a set is a subset of the base. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐹‘𝑈) ⊆ 𝑋) | ||
| Theorem | mrcidb 17658 | A set is closed iff it is equal to its closure. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑈 ∈ 𝐶 ↔ (𝐹‘𝑈) = 𝑈)) | ||
| Theorem | mrcss 17659 | Closure preserves subset ordering. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘𝑈) ⊆ (𝐹‘𝑉)) | ||
| Theorem | mrcssid 17660 | The closure of a set is a superset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → 𝑈 ⊆ (𝐹‘𝑈)) | ||
| Theorem | mrcidb2 17661 | A set is closed iff it contains its closure. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝑈 ∈ 𝐶 ↔ (𝐹‘𝑈) ⊆ 𝑈)) | ||
| Theorem | mrcidm 17662 | The closure operation is idempotent. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘(𝐹‘𝑈)) = (𝐹‘𝑈)) | ||
| Theorem | mrcsscl 17663 | The closure is the minimal closed set; any closed set which contains the generators is a superset of the closure. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ∈ 𝐶) → (𝐹‘𝑈) ⊆ 𝑉) | ||
| Theorem | mrcuni 17664 | Idempotence of closure under a general union. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (𝐹‘∪ 𝑈) = (𝐹‘∪ (𝐹 “ 𝑈))) | ||
| Theorem | mrcun 17665 | Idempotence of closure under a pair union. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘(𝑈 ∪ 𝑉)) = (𝐹‘((𝐹‘𝑈) ∪ (𝐹‘𝑉)))) | ||
| Theorem | mrcssvd 17666 | The Moore closure of a set is a subset of the base. Deduction form of mrcssv 17657. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) ⇒ ⊢ (𝜑 → (𝑁‘𝐵) ⊆ 𝑋) | ||
| Theorem | mrcssd 17667 | Moore closure preserves subset ordering. Deduction form of mrcss 17659. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑈 ⊆ 𝑉) & ⊢ (𝜑 → 𝑉 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑁‘𝑈) ⊆ (𝑁‘𝑉)) | ||
| Theorem | mrcssidd 17668 | A set is contained in its Moore closure. Deduction form of mrcssid 17660. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑈 ⊆ 𝑋) ⇒ ⊢ (𝜑 → 𝑈 ⊆ (𝑁‘𝑈)) | ||
| Theorem | mrcidmd 17669 | Moore closure is idempotent. Deduction form of mrcidm 17662. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑈 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑁‘(𝑁‘𝑈)) = (𝑁‘𝑈)) | ||
| Theorem | mressmrcd 17670 | In a Moore system, if a set is between another set and its closure, the two sets have the same closure. Deduction form. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑇)) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇)) | ||
| Theorem | submrc 17671 | In a closure system which is cut off above some level, closures below that level act as normal. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) & ⊢ 𝐺 = (mrCls‘(𝐶 ∩ 𝒫 𝐷)) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐷 ∈ 𝐶 ∧ 𝑈 ⊆ 𝐷) → (𝐺‘𝑈) = (𝐹‘𝑈)) | ||
| Theorem | mrieqvlemd 17672 | In a Moore system, if 𝑌 is a member of 𝑆, (𝑆 ∖ {𝑌}) and 𝑆 have the same closure if and only if 𝑌 is in the closure of (𝑆 ∖ {𝑌}). Used in the proof of mrieqvd 17681 and mrieqv2d 17682. Deduction form. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑌 ∈ (𝑁‘(𝑆 ∖ {𝑌})) ↔ (𝑁‘(𝑆 ∖ {𝑌})) = (𝑁‘𝑆))) | ||
| Theorem | mrisval 17673* | Value of the set of independent sets of a Moore system. (Contributed by David Moews, 1-May-2017.) |
| ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) ⇒ ⊢ (𝐴 ∈ (Moore‘𝑋) → 𝐼 = {𝑠 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))}) | ||
| Theorem | ismri 17674* | Criterion for a set to be an independent set of a Moore system. (Contributed by David Moews, 1-May-2017.) |
| ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) ⇒ ⊢ (𝐴 ∈ (Moore‘𝑋) → (𝑆 ∈ 𝐼 ↔ (𝑆 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))))) | ||
| Theorem | ismri2 17675* | Criterion for a subset of the base set in a Moore system to be independent. (Contributed by David Moews, 1-May-2017.) |
| ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) ⇒ ⊢ ((𝐴 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐼 ↔ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))) | ||
| Theorem | ismri2d 17676* | Criterion for a subset of the base set in a Moore system to be independent. Deduction form. (Contributed by David Moews, 1-May-2017.) |
| ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))) | ||
| Theorem | ismri2dd 17677* | Definition of independence of a subset of the base set in a Moore system. One-way deduction form. (Contributed by David Moews, 1-May-2017.) |
| ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) ⇒ ⊢ (𝜑 → 𝑆 ∈ 𝐼) | ||
| Theorem | mriss 17678 | An independent set of a Moore system is a subset of the base set. (Contributed by David Moews, 1-May-2017.) |
| ⊢ 𝐼 = (mrInd‘𝐴) ⇒ ⊢ ((𝐴 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐼) → 𝑆 ⊆ 𝑋) | ||
| Theorem | mrissd 17679 | An independent set of a Moore system is a subset of the base set. Deduction form. (Contributed by David Moews, 1-May-2017.) |
| ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) ⇒ ⊢ (𝜑 → 𝑆 ⊆ 𝑋) | ||
| Theorem | ismri2dad 17680 | Consequence of a set in a Moore system being independent. Deduction form. (Contributed by David Moews, 1-May-2017.) |
| ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘(𝑆 ∖ {𝑌}))) | ||
| Theorem | mrieqvd 17681* | In a Moore system, a set is independent if and only if, for all elements of the set, the closure of the set with the element removed is unequal to the closure of the original set. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑥 ∈ 𝑆 (𝑁‘(𝑆 ∖ {𝑥})) ≠ (𝑁‘𝑆))) | ||
| Theorem | mrieqv2d 17682* | In a Moore system, a set is independent if and only if all its proper subsets have closure properly contained in the closure of the set. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑠(𝑠 ⊊ 𝑆 → (𝑁‘𝑠) ⊊ (𝑁‘𝑆)))) | ||
| Theorem | mrissmrcd 17683 | In a Moore system, if an independent set is between a set and its closure, the two sets are equal (since the two sets must have equal closures by mressmrcd 17670, and so are equal by mrieqv2d 17682.) (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑇)) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) ⇒ ⊢ (𝜑 → 𝑆 = 𝑇) | ||
| Theorem | mrissmrid 17684 | In a Moore system, subsets of independent sets are independent. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → 𝑇 ∈ 𝐼) | ||
| Theorem | mreexd 17685* | In a Moore system, the closure operator is said to have the exchange property if, for all elements 𝑦 and 𝑧 of the base set and subsets 𝑆 of the base set such that 𝑧 is in the closure of (𝑆 ∪ {𝑦}) but not in the closure of 𝑆, 𝑦 is in the closure of (𝑆 ∪ {𝑧}) (Definition 3.1.9 in [FaureFrolicher] p. 57 to 58.) This theorem allows to construct substitution instances of this definition. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝑍 ∈ (𝑁‘(𝑆 ∪ {𝑌}))) & ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘𝑆)) ⇒ ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))) | ||
| Theorem | mreexmrid 17686* | In a Moore system whose closure operator has the exchange property, if a set is independent and an element is not in its closure, then adding the element to the set gives another independent set. Lemma 4.1.5 in [FaureFrolicher] p. 84. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘𝑆)) ⇒ ⊢ (𝜑 → (𝑆 ∪ {𝑌}) ∈ 𝐼) | ||
| Theorem | mreexexlemd 17687* | This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 17691. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝐽) & ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻))) & ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼) & ⊢ (𝜑 → (𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾)) & ⊢ (𝜑 → ∀𝑡∀𝑢 ∈ 𝒫 (𝑋 ∖ 𝑡)∀𝑣 ∈ 𝒫 (𝑋 ∖ 𝑡)(((𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣 ∪ 𝑡)) ∧ (𝑢 ∪ 𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢 ≈ 𝑖 ∧ (𝑖 ∪ 𝑡) ∈ 𝐼))) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼)) | ||
| Theorem | mreexexlem2d 17688* | Used in mreexexlem4d 17690 to prove the induction step in mreexexd 17691. See the proof of Proposition 4.2.1 in [FaureFrolicher] p. 86 to 87. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻))) & ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼) & ⊢ (𝜑 → 𝑌 ∈ 𝐹) ⇒ ⊢ (𝜑 → ∃𝑔 ∈ 𝐺 (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼)) | ||
| Theorem | mreexexlem3d 17689* | Base case of the induction in mreexexd 17691. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻))) & ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼) & ⊢ (𝜑 → (𝐹 = ∅ ∨ 𝐺 = ∅)) ⇒ ⊢ (𝜑 → ∃𝑖 ∈ 𝒫 𝐺(𝐹 ≈ 𝑖 ∧ (𝑖 ∪ 𝐻) ∈ 𝐼)) | ||
| Theorem | mreexexlem4d 17690* | Induction step of the induction in mreexexd 17691. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻))) & ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼) & ⊢ (𝜑 → 𝐿 ∈ ω) & ⊢ (𝜑 → ∀ℎ∀𝑓 ∈ 𝒫 (𝑋 ∖ ℎ)∀𝑔 ∈ 𝒫 (𝑋 ∖ ℎ)(((𝑓 ≈ 𝐿 ∨ 𝑔 ≈ 𝐿) ∧ 𝑓 ⊆ (𝑁‘(𝑔 ∪ ℎ)) ∧ (𝑓 ∪ ℎ) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓 ≈ 𝑗 ∧ (𝑗 ∪ ℎ) ∈ 𝐼))) & ⊢ (𝜑 → (𝐹 ≈ suc 𝐿 ∨ 𝐺 ≈ suc 𝐿)) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹 ≈ 𝑗 ∧ (𝑗 ∪ 𝐻) ∈ 𝐼)) | ||
| Theorem | mreexexd 17691* | Exchange-type theorem. In a Moore system whose closure operator has the exchange property, if 𝐹 and 𝐺 are disjoint from 𝐻, (𝐹 ∪ 𝐻) is independent, 𝐹 is contained in the closure of (𝐺 ∪ 𝐻), and either 𝐹 or 𝐺 is finite, then there is a subset 𝑞 of 𝐺 equinumerous to 𝐹 such that (𝑞 ∪ 𝐻) is independent. This implies the case of Proposition 4.2.1 in [FaureFrolicher] p. 86 where either (𝐴 ∖ 𝐵) or (𝐵 ∖ 𝐴) is finite. The theorem is proven by induction using mreexexlem3d 17689 for the base case and mreexexlem4d 17690 for the induction step. (Contributed by David Moews, 1-May-2017.) Remove dependencies on ax-rep 5279 and ax-ac2 10503. (Revised by Brendan Leahy, 2-Jun-2021.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻)) & ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻))) & ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼) & ⊢ (𝜑 → (𝐹 ∈ Fin ∨ 𝐺 ∈ Fin)) ⇒ ⊢ (𝜑 → ∃𝑞 ∈ 𝒫 𝐺(𝐹 ≈ 𝑞 ∧ (𝑞 ∪ 𝐻) ∈ 𝐼)) | ||
| Theorem | mreexdomd 17692* | In a Moore system whose closure operator has the exchange property, if 𝑆 is independent and contained in the closure of 𝑇, and either 𝑆 or 𝑇 is finite, then 𝑇 dominates 𝑆. This is an immediate consequence of mreexexd 17691. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑇)) & ⊢ (𝜑 → 𝑇 ⊆ 𝑋) & ⊢ (𝜑 → (𝑆 ∈ Fin ∨ 𝑇 ∈ Fin)) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) ⇒ ⊢ (𝜑 → 𝑆 ≼ 𝑇) | ||
| Theorem | mreexfidimd 17693* | In a Moore system whose closure operator has the exchange property, if two independent sets have equal closure and one is finite, then they are equinumerous. Proven by using mreexdomd 17692 twice. This implies a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧}))) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑇 ∈ 𝐼) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇)) ⇒ ⊢ (𝜑 → 𝑆 ≈ 𝑇) | ||
| Theorem | isacs 17694* | A set is an algebraic closure system iff it is specified by some function of the finite subsets, such that a set is closed iff it does not expand under the operation. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠)))) | ||
| Theorem | acsmre 17695 | Algebraic closure systems are closure systems. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ (𝐶 ∈ (ACS‘𝑋) → 𝐶 ∈ (Moore‘𝑋)) | ||
| Theorem | isacs2 17696* | In the definition of an algebraic closure system, we may always take the operation being closed over as the Moore closure. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (ACS‘𝑋) ↔ (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝑠 ∈ 𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑠 ∩ Fin)(𝐹‘𝑦) ⊆ 𝑠))) | ||
| Theorem | acsfiel 17697* | A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (ACS‘𝑋) → (𝑆 ∈ 𝐶 ↔ (𝑆 ⊆ 𝑋 ∧ ∀𝑦 ∈ (𝒫 𝑆 ∩ Fin)(𝐹‘𝑦) ⊆ 𝑆))) | ||
| Theorem | acsfiel2 17698* | A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
| ⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (ACS‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐶 ↔ ∀𝑦 ∈ (𝒫 𝑆 ∩ Fin)(𝐹‘𝑦) ⊆ 𝑆)) | ||
| Theorem | acsmred 17699 | An algebraic closure system is also a Moore system. Deduction form of acsmre 17695. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) ⇒ ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) | ||
| Theorem | isacs1i 17700* | A closure system determined by a function is a closure system and algebraic. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
| ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∈ (ACS‘𝑋)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |