![]() |
Metamath
Proof Explorer Theorem List (p. 173 of 489) | < 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-30950) |
![]() (30951-32473) |
![]() (32474-48899) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | structfung 17201 | The converse of the converse of a structure is a function. Closed form of structfun 17202. (Contributed by AV, 12-Nov-2021.) |
⊢ (𝐹 Struct 𝑋 → Fun ◡◡𝐹) | ||
Theorem | structfun 17202 | Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Proof shortened by AV, 12-Nov-2021.) |
⊢ 𝐹 Struct 𝑋 ⇒ ⊢ Fun ◡◡𝐹 | ||
Theorem | structfn 17203 | Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐹 Struct 〈𝑀, 𝑁〉 ⇒ ⊢ (Fun ◡◡𝐹 ∧ dom 𝐹 ⊆ (1...𝑁)) | ||
Theorem | strleun 17204 | Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐹 Struct 〈𝐴, 𝐵〉 & ⊢ 𝐺 Struct 〈𝐶, 𝐷〉 & ⊢ 𝐵 < 𝐶 ⇒ ⊢ (𝐹 ∪ 𝐺) Struct 〈𝐴, 𝐷〉 | ||
Theorem | strle1 17205 | Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐼 ∈ ℕ & ⊢ 𝐴 = 𝐼 ⇒ ⊢ {〈𝐴, 𝑋〉} Struct 〈𝐼, 𝐼〉 | ||
Theorem | strle2 17206 | Make a structure from a pair. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐼 ∈ ℕ & ⊢ 𝐴 = 𝐼 & ⊢ 𝐼 < 𝐽 & ⊢ 𝐽 ∈ ℕ & ⊢ 𝐵 = 𝐽 ⇒ ⊢ {〈𝐴, 𝑋〉, 〈𝐵, 𝑌〉} Struct 〈𝐼, 𝐽〉 | ||
Theorem | strle3 17207 | Make a structure from a triple. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐼 ∈ ℕ & ⊢ 𝐴 = 𝐼 & ⊢ 𝐼 < 𝐽 & ⊢ 𝐽 ∈ ℕ & ⊢ 𝐵 = 𝐽 & ⊢ 𝐽 < 𝐾 & ⊢ 𝐾 ∈ ℕ & ⊢ 𝐶 = 𝐾 ⇒ ⊢ {〈𝐴, 𝑋〉, 〈𝐵, 𝑌〉, 〈𝐶, 𝑍〉} Struct 〈𝐼, 𝐾〉 | ||
Theorem | sbcie2s 17208* | A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 14-Mar-2019.) (Revised by SN, 2-Mar-2025.) |
⊢ 𝐴 = (𝐸‘𝑊) & ⊢ 𝐵 = (𝐹‘𝑊) & ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝑤 = 𝑊 → ([(𝐸‘𝑤) / 𝑎][(𝐹‘𝑤) / 𝑏]𝜑 ↔ 𝜓)) | ||
Theorem | sbcie3s 17209* | A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 15-Mar-2019.) |
⊢ 𝐴 = (𝐸‘𝑊) & ⊢ 𝐵 = (𝐹‘𝑊) & ⊢ 𝐶 = (𝐺‘𝑊) & ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝑤 = 𝑊 → ([(𝐸‘𝑤) / 𝑎][(𝐹‘𝑤) / 𝑏][(𝐺‘𝑤) / 𝑐]𝜓 ↔ 𝜑)) | ||
Syntax | csts 17210 | Set components of a structure. |
class sSet | ||
Definition | df-sets 17211* | Set a component of an extensible structure. This function is useful for taking an existing structure and "overriding" one of its components. For example, df-ress 17288 adjusts the base set to match its second argument, which has the effect of making subgroups, subspaces, subrings etc. from the original structures. Or df-mgp 20162, which takes a ring and overrides its addition operation with the multiplicative operation, so that we can consider the "multiplicative group" using group and monoid theorems, which expect the operation to be in the +g slot instead of the .r slot. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ sSet = (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒})) | ||
Theorem | reldmsets 17212 | The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ Rel dom sSet | ||
Theorem | setsvalg 17213 | Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑆 sSet 𝐴) = ((𝑆 ↾ (V ∖ dom {𝐴})) ∪ {𝐴})) | ||
Theorem | setsval 17214 | Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑆 sSet 〈𝐴, 𝐵〉) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐵〉})) | ||
Theorem | fvsetsid 17215 | The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈) → ((𝐹 sSet 〈𝑋, 𝑌〉)‘𝑋) = 𝑌) | ||
Theorem | fsets 17216 | The structure replacement function is a function. (Contributed by SO, 12-Jul-2018.) |
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝐹 sSet 〈𝑋, 𝑌〉):𝐴⟶𝐵) | ||
Theorem | setsdm 17217 | The domain of a structure with replacement is the domain of the original structure extended by the index of the replacement. (Contributed by AV, 7-Jun-2021.) |
⊢ ((𝐺 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → dom (𝐺 sSet 〈𝐼, 𝐸〉) = (dom 𝐺 ∪ {𝐼})) | ||
Theorem | setsfun 17218 | A structure with replacement is a function if the original structure is a function. (Contributed by AV, 7-Jun-2021.) |
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun (𝐺 sSet 〈𝐼, 𝐸〉)) | ||
Theorem | setsfun0 17219 | A structure with replacement without the empty set is a function if the original structure without the empty set is a function. This variant of setsfun 17218 is useful for proofs based on isstruct2 17196 which requires Fun (𝐹 ∖ {∅}) for 𝐹 to be an extensible structure. (Contributed by AV, 7-Jun-2021.) |
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅})) | ||
Theorem | setsn0fun 17220 | The value of the structure replacement function (without the empty set) is a function if the structure (without the empty set) is a function. (Contributed by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.) |
⊢ (𝜑 → 𝑆 Struct 𝑋) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) ⇒ ⊢ (𝜑 → Fun ((𝑆 sSet 〈𝐼, 𝐸〉) ∖ {∅})) | ||
Theorem | setsstruct2 17221 | An extensible structure with a replaced slot is an extensible structure. (Contributed by AV, 14-Nov-2021.) |
⊢ (((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) ∧ 𝑌 = 〈if(𝐼 ≤ (1st ‘𝑋), 𝐼, (1st ‘𝑋)), if(𝐼 ≤ (2nd ‘𝑋), (2nd ‘𝑋), 𝐼)〉) → (𝐺 sSet 〈𝐼, 𝐸〉) Struct 𝑌) | ||
Theorem | setsexstruct2 17222* | An extensible structure with a replaced slot is an extensible structure. (Contributed by AV, 14-Nov-2021.) |
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → ∃𝑦(𝐺 sSet 〈𝐼, 𝐸〉) Struct 𝑦) | ||
Theorem | setsstruct 17223 | An extensible structure with a replaced slot is an extensible structure. (Contributed by AV, 9-Jun-2021.) (Revised by AV, 14-Nov-2021.) |
⊢ ((𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀) ∧ 𝐺 Struct 〈𝑀, 𝑁〉) → (𝐺 sSet 〈𝐼, 𝐸〉) Struct 〈𝑀, if(𝐼 ≤ 𝑁, 𝑁, 𝐼)〉) | ||
Theorem | wunsets 17224 | Closure of structure replacement in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝑆 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑆 sSet 𝐴) ∈ 𝑈) | ||
Theorem | setsres 17225 | The structure replacement function does not affect the value of 𝑆 away from 𝐴. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ (𝑆 ∈ 𝑉 → ((𝑆 sSet 〈𝐴, 𝐵〉) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴}))) | ||
Theorem | setsabs 17226 | Replacing the same components twice yields the same as the second setting only. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ((𝑆 sSet 〈𝐴, 𝐵〉) sSet 〈𝐴, 𝐶〉) = (𝑆 sSet 〈𝐴, 𝐶〉)) | ||
Theorem | setscom 17227 | Different components can be set in any order. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝐵, 𝐷〉) = ((𝑆 sSet 〈𝐵, 𝐷〉) sSet 〈𝐴, 𝐶〉)) | ||
Syntax | cslot 17228 | Extend class notation with the slot function. |
class Slot 𝐴 | ||
Definition | df-slot 17229* |
Define the slot extractor for extensible structures. The class
Slot 𝐴 is a function whose argument can be
any set, although it is
meaningful only if that set is a member of an extensible structure (such
as a partially ordered set (df-poset 18383) or a group (df-grp 18976)).
Note that Slot 𝐴 is implemented as "evaluation at 𝐴". That is, (Slot 𝐴‘𝑆) is defined to be (𝑆‘𝐴), where 𝐴 will typically be an index (which is implemented as a small natural number) of a component of an extensible structure 𝑆. Each extensible structure is a function defined on specific (natural number) "slots", and the function Slot 𝐴 extracts the structure's component as a function value at a particular slot (with index 𝐴). The special "structure" ndx, defined as the identity function restricted to ℕ, can be used to extract the number 𝐴 from a slot, since (Slot 𝐴‘ndx) = 𝐴 (see ndxarg 17243). This is typically used to refer to the number of a slot when defining structures without having to expose the detail of what that number is (for instance, we use the expression (Base‘ndx) in theorems and proofs instead of its hard-coded, numeric value 1), and discourage using the specific definition of slot extractors like Base = Slot 1 (see df-base 17259). Actually, these definitions are used in two basic theorems named *id (theorems of the form 𝐶 = Slot (𝐶‘ndx)) and *ndx (theorems of the form (𝐶‘ndx) = 𝑁) only (see, for example, baseid 17261 and basendx 17267), except additionally in the discouraged theorem baseval 17260 to demonstrate the representations of the value of the base set extractor. The *id theorems are implementation independent equivalents of the definitions by the means of ndxid 17244, but the *ndx theorems still depend on the hard-coded values of the indices. Therefore, the usage of these *ndx theorems is also discouraged (for more details see the section header comment mmtheorems.html#cnx 17244). Example: The group operation is the second component, i.e., the component in the second slot, of a group-like structure 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉} (see grpstr 17343). The slot extractor +g = Slot 2 (see df-plusg 17324) applied on the structure 𝐺 provides the group operation + = (+g‘𝐺). Expanding the definitions, we get + = (Slot 2‘𝐺) = (𝐺‘2) = (𝐺‘(+g‘ndx)) (for the last equation, see plusgndx 17337). The class Slot cannot be defined as (𝑥 ∈ V ↦ (𝑓 ∈ V ↦ (𝑓‘𝑥))) because each Slot 𝐴 is a function on the proper class V so is itself a proper class, and the values of functions are sets (fvex 6933). It is necessary to allow proper classes as values of Slot 𝐴 since for instance the class of all (base sets of) groups is proper. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ Slot 𝐴 = (𝑥 ∈ V ↦ (𝑥‘𝐴)) | ||
Theorem | sloteq 17230 | Equality theorem for the Slot construction. The converse holds if 𝐴 (or 𝐵) is a set. (Contributed by BJ, 27-Dec-2021.) |
⊢ (𝐴 = 𝐵 → Slot 𝐴 = Slot 𝐵) | ||
Theorem | slotfn 17231 | A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐸 = Slot 𝑁 ⇒ ⊢ 𝐸 Fn V | ||
Theorem | strfvnd 17232 | Deduction version of strfvn 17233. (Contributed by Mario Carneiro, 15-Nov-2014.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ (𝜑 → 𝑆 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐸‘𝑆) = (𝑆‘𝑁)) | ||
Theorem | strfvn 17233 |
Value of a structure component extractor 𝐸. Normally, 𝐸 is a
defined constant symbol such as Base (df-base 17259) and 𝑁 is the
index of the component. 𝑆 is a structure, i.e. a specific
member of
a class of structures such as Poset (df-poset 18383) where
𝑆
∈ Poset.
Hint: Do not substitute 𝑁 by a specific (positive) integer to be independent of a hard-coded index value. Often, (𝐸‘ndx) can be used instead of 𝑁. Alternatively, use strfv 17251 instead of strfvn 17233. (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2013.) (New usage is discouraged.) |
⊢ 𝑆 ∈ V & ⊢ 𝐸 = Slot 𝑁 ⇒ ⊢ (𝐸‘𝑆) = (𝑆‘𝑁) | ||
Theorem | strfvss 17234 | A structure component extractor produces a value which is contained in a set dependent on 𝑆, but not 𝐸. This is sometimes useful for showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ 𝐸 = Slot 𝑁 ⇒ ⊢ (𝐸‘𝑆) ⊆ ∪ ran 𝑆 | ||
Theorem | wunstr 17235 | Closure of a structure index in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝑆 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐸‘𝑆) ∈ 𝑈) | ||
Theorem | str0 17236 | All components of the empty set are empty sets. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐹 = Slot 𝐼 ⇒ ⊢ ∅ = (𝐹‘∅) | ||
Theorem | strfvi 17237 | Structure slot extractors cannot distinguish between proper classes and ∅, so they can be protected using the identity function. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑋 = (𝐸‘𝑆) ⇒ ⊢ 𝑋 = (𝐸‘( I ‘𝑆)) | ||
Theorem | fveqprc 17238 | Lemma for showing the equality of values for functions like slot extractors 𝐸 at a proper class. Extracted from several former proofs of lemmas like zlmlem 21550. (Contributed by AV, 31-Oct-2024.) |
⊢ (𝐸‘∅) = ∅ & ⊢ 𝑌 = (𝐹‘𝑋) ⇒ ⊢ (¬ 𝑋 ∈ V → (𝐸‘𝑋) = (𝐸‘𝑌)) | ||
Theorem | oveqprc 17239 | Lemma for showing the equality of values for functions like slot extractors 𝐸 at a proper class. Extracted from several former proofs of lemmas like resvlem 33322. (Contributed by AV, 31-Oct-2024.) |
⊢ (𝐸‘∅) = ∅ & ⊢ 𝑍 = (𝑋𝑂𝑌) & ⊢ Rel dom 𝑂 ⇒ ⊢ (¬ 𝑋 ∈ V → (𝐸‘𝑋) = (𝐸‘𝑍)) | ||
The structure component index extractor ndx, defined in this subsection, is used to get the numeric argument from a defined structure component extractor such as df-base 17259 (see ndxarg 17243). For each defined structure component extractor, there should be a corresponding specific theorem providing its index, like basendx 17267. The usage of these theorems, however, is discouraged since the particular value for the index is an implementation detail. It is generally sufficient to work with (Base‘ndx) instead of the hard-coded index value, and use theorems such as baseid 17261 and basendxnplusgndx 17341. The main circumstance in which it is necessary to look at indices directly is when showing that a set of indices are disjoint (for example in proofs such as cznabel 47983, based on setsnid 17256) or even ordered (in proofs such as lmodstr 17384). The requirement that the indices are distinct is necessary for sets of ordered pairs to be extensible structures, whereas the ordering allows for proofs avoiding the usage of quadradically many inequalities (compare cnfldfun 21401 with cnfldfunALT 21402). As for the inequalities, it is recommended to provide them explicitly as theorems like basendxnplusgndx 17341, whenever they are required. Since these theorems use discouraged slot theorems, they should be placed near the definition of a slot (within the same subsection), so that the range of usages of discouraged theorems is tightly limited. Although there could be quadradically many of them in the total number of indices, much less are actually available (and not much more are expected). As for the ordering, there are some theorems like basendxltplusgndx 17340 providing the less-than relationship between two indices. These theorems are also proved by discouraged theorems, so they should be placed near the definition of a slot (within the same subsection), too. However, since such theorems are rarely used (in structure building theorems *str like rngstr 17357), it is not recommended to provide explicit theorems for all of them, but to use the (discouraged) *ndx theorems as in lmodstr 17384. Therefore, *str theorems generally depend on the hard-coded values of the indices. | ||
Syntax | cnx 17240 | Extend class notation with the structure component index extractor. |
class ndx | ||
Definition | df-ndx 17241 | Define the structure component index extractor. See Theorem ndxarg 17243 to understand its purpose. The restriction to ℕ ensures that ndx is a set. The restriction to some set is necessary since I is a proper class. In principle, we could have chosen ℂ or (if we revise all structure component definitions such as df-base 17259) another set such as the set of finite ordinals ω (df-om 7904). (Contributed by NM, 4-Sep-2011.) |
⊢ ndx = ( I ↾ ℕ) | ||
Theorem | wunndx 17242 | Closure of the index extractor in an infinite weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) ⇒ ⊢ (𝜑 → ndx ∈ 𝑈) | ||
Theorem | ndxarg 17243 | Get the numeric argument from a defined structure component extractor such as df-base 17259. (Contributed by Mario Carneiro, 6-Oct-2013.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐸‘ndx) = 𝑁 | ||
Theorem | ndxid 17244 |
A structure component extractor is defined by its own index. This
theorem, together with strfv 17251 below, is useful for avoiding direct
reference to the hard-coded numeric index in component extractor
definitions, such as the 1 in df-base 17259 and the ;10 in
df-ple 17331, making it easier to change should the need
arise.
For example, we can refer to a specific poset with base set 𝐵 and order relation 𝐿 using {〈(Base‘ndx), 𝐵〉, 〈(le‘ndx), 𝐿〉} rather than {〈1, 𝐵〉, 〈;10, 𝐿〉}. The latter, while shorter to state, requires revision if we later change ;10 to some other number, and it may also be harder to remember. (Contributed by NM, 19-Oct-2012.) (Revised by Mario Carneiro, 6-Oct-2013.) (Proof shortened by BJ, 27-Dec-2021.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ 𝐸 = Slot (𝐸‘ndx) | ||
Theorem | strndxid 17245 | The value of a structure component extractor is the value of the corresponding slot of the structure. (Contributed by AV, 13-Mar-2020.) (New usage is discouraged.) Use strfvnd 17232 directly with 𝑁 set to (𝐸‘ndx) if possible. |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝜑 → (𝑆‘(𝐸‘ndx)) = (𝐸‘𝑆)) | ||
Theorem | setsidvald 17246 |
Value of the structure replacement function, deduction version.
Hint: Do not substitute 𝑁 by a specific (positive) integer to be independent of a hard-coded index value. Often, (𝐸‘ndx) can be used instead of 𝑁. (Contributed by AV, 14-Mar-2020.) (Revised by AV, 17-Oct-2024.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝑆) & ⊢ (𝜑 → 𝑁 ∈ dom 𝑆) ⇒ ⊢ (𝜑 → 𝑆 = (𝑆 sSet 〈𝑁, (𝐸‘𝑆)〉)) | ||
Theorem | setsidvaldOLD 17247 | Obsolete version of setsidvald 17246 as of 17-Oct-2024. (Contributed by AV, 14-Mar-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝑆) & ⊢ (𝜑 → (𝐸‘ndx) ∈ dom 𝑆) ⇒ ⊢ (𝜑 → 𝑆 = (𝑆 sSet 〈(𝐸‘ndx), (𝐸‘𝑆)〉)) | ||
Theorem | strfvd 17248 | Deduction version of strfv 17251. (Contributed by Mario Carneiro, 15-Nov-2014.) |
⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝑆) & ⊢ (𝜑 → 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆)) | ||
Theorem | strfv2d 17249 | Deduction version of strfv2 17250. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → Fun ◡◡𝑆) & ⊢ (𝜑 → 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆)) | ||
Theorem | strfv2 17250 | A variation on strfv 17251 to avoid asserting that 𝑆 itself is a function, which involves sethood of all the ordered pair components of 𝑆. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝑆 ∈ V & ⊢ Fun ◡◡𝑆 & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆 ⇒ ⊢ (𝐶 ∈ 𝑉 → 𝐶 = (𝐸‘𝑆)) | ||
Theorem | strfv 17251 | Extract a structure component 𝐶 (such as the base set) from a structure 𝑆 (such as a member of Poset, df-poset 18383) with a component extractor 𝐸 (such as the base set extractor df-base 17259). By virtue of ndxid 17244, this can be done without having to refer to the hard-coded numeric index of 𝐸. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝑆 Struct 𝑋 & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ {〈(𝐸‘ndx), 𝐶〉} ⊆ 𝑆 ⇒ ⊢ (𝐶 ∈ 𝑉 → 𝐶 = (𝐸‘𝑆)) | ||
Theorem | strfv3 17252 | Variant on strfv 17251 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.) |
⊢ (𝜑 → 𝑈 = 𝑆) & ⊢ 𝑆 Struct 𝑋 & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ {〈(𝐸‘ndx), 𝐶〉} ⊆ 𝑆 & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ 𝐴 = (𝐸‘𝑈) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
Theorem | strssd 17253 | Deduction version of strss 17254. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝑇) & ⊢ (𝜑 → 𝑆 ⊆ 𝑇) & ⊢ (𝜑 → 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸‘𝑇) = (𝐸‘𝑆)) | ||
Theorem | strss 17254 | Propagate component extraction to a structure 𝑇 from a subset structure 𝑆. (Contributed by Mario Carneiro, 11-Oct-2013.) (Revised by Mario Carneiro, 15-Jan-2014.) |
⊢ 𝑇 ∈ V & ⊢ Fun 𝑇 & ⊢ 𝑆 ⊆ 𝑇 & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆 ⇒ ⊢ (𝐸‘𝑇) = (𝐸‘𝑆) | ||
Theorem | setsid 17255 | Value of the structure replacement function at a replaced index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐸 = Slot (𝐸‘ndx) ⇒ ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 = (𝐸‘(𝑊 sSet 〈(𝐸‘ndx), 𝐶〉))) | ||
Theorem | setsnid 17256 | Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 7-Nov-2024.) |
⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ 𝐷 ⇒ ⊢ (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) | ||
Theorem | setsnidOLD 17257 | Obsolete proof of setsnid 17256 as of 7-Nov-2024. Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ 𝐷 ⇒ ⊢ (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉)) | ||
Syntax | cbs 17258 | Extend class notation with the class of all base set extractors. |
class Base | ||
Definition | df-base 17259 | Define the base set (also called underlying set, ground set, carrier set, or carrier) extractor for extensible structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form baseid 17261 instead. (New usage is discouraged.) |
⊢ Base = Slot 1 | ||
Theorem | baseval 17260 | Value of the base set extractor. (Normally it is preferred to work with (Base‘ndx) rather than the hard-coded 1 in order to make structure theorems portable. This is an example of how to obtain it when needed.) (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.) |
⊢ 𝐾 ∈ V ⇒ ⊢ (Base‘𝐾) = (𝐾‘1) | ||
Theorem | baseid 17261 | Utility theorem: index-independent form of df-base 17259. (Contributed by NM, 20-Oct-2012.) |
⊢ Base = Slot (Base‘ndx) | ||
Theorem | basfn 17262 | The base set extractor is a function on V. (Contributed by Stefan O'Rear, 8-Jul-2015.) |
⊢ Base Fn V | ||
Theorem | base0 17263 | The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ ∅ = (Base‘∅) | ||
Theorem | elbasfv 17264 | Utility theorem: reverse closure for any structure defined as a function. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
⊢ 𝑆 = (𝐹‘𝑍) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝑋 ∈ 𝐵 → 𝑍 ∈ V) | ||
Theorem | elbasov 17265 | Utility theorem: reverse closure for any structure defined as a two-argument function. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ Rel dom 𝑂 & ⊢ 𝑆 = (𝑋𝑂𝑌) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝐴 ∈ 𝐵 → (𝑋 ∈ V ∧ 𝑌 ∈ V)) | ||
Theorem | strov2rcl 17266 | Partial reverse closure for any structure defined as a two-argument function. (Contributed by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 2-Dec-2019.) |
⊢ 𝑆 = (𝐼𝐹𝑅) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ Rel dom 𝐹 ⇒ ⊢ (𝑋 ∈ 𝐵 → 𝐼 ∈ V) | ||
Theorem | basendx 17267 | Index value of the base set extractor. (Contributed by Mario Carneiro, 2-Aug-2013.) Use of this theorem is discouraged since the particular value 1 for the index is an implementation detail, see section header comment mmtheorems.html#cnx for more information. (New usage is discouraged.) |
⊢ (Base‘ndx) = 1 | ||
Theorem | basendxnn 17268 | The index value of the base set extractor is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 13-Oct-2024.) |
⊢ (Base‘ndx) ∈ ℕ | ||
Theorem | basendxnnOLD 17269 | Obsolete proof of basendxnn 17268 as of 13-Oct-2024. (Contributed by AV, 23-Sep-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Base‘ndx) ∈ ℕ | ||
Theorem | basndxelwund 17270 | The index of the base set is an element in a weak universe containing the natural numbers. Formerly part of proof for 1strwun 17278. (Contributed by AV, 27-Mar-2020.) (Revised by AV, 17-Oct-2024.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) ⇒ ⊢ (𝜑 → (Base‘ndx) ∈ 𝑈) | ||
Theorem | basprssdmsets 17271 | The pair of the base index and another index is a subset of the domain of the structure obtained by replacing/adding a slot at the other index in a structure having a base slot. (Contributed by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.) |
⊢ (𝜑 → 𝑆 Struct 𝑋) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝑆) ⇒ ⊢ (𝜑 → {(Base‘ndx), 𝐼} ⊆ dom (𝑆 sSet 〈𝐼, 𝐸〉)) | ||
Theorem | opelstrbas 17272 | The base set of a structure with a base set. (Contributed by AV, 10-Nov-2021.) |
⊢ (𝜑 → 𝑆 Struct 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 〈(Base‘ndx), 𝑉〉 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑉 = (Base‘𝑆)) | ||
Theorem | 1strstr 17273 | A constructed one-slot structure. Depending on hard-coded index. Use 1strstr1 17274 instead. (Contributed by AV, 27-Mar-2020.) (New usage is discouraged.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉} ⇒ ⊢ 𝐺 Struct 〈1, 1〉 | ||
Theorem | 1strstr1 17274 | A constructed one-slot structure. (Contributed by AV, 15-Nov-2024.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉} ⇒ ⊢ 𝐺 Struct 〈(Base‘ndx), (Base‘ndx)〉 | ||
Theorem | 1strbas 17275 | The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020.) (Proof shortened by AV, 15-Nov-2024.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉} ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺)) | ||
Theorem | 1strbasOLD 17276 | Obsolete proof of 1strbas 17275 as of 15-Nov-2024. The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉} ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺)) | ||
Theorem | 1strwunbndx 17277 | A constructed one-slot structure in a weak universe containing the index of the base set extractor. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉} & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → (Base‘ndx) ∈ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑈) → 𝐺 ∈ 𝑈) | ||
Theorem | 1strwun 17278 | A constructed one-slot structure in a weak universe. (Contributed by AV, 27-Mar-2020.) (Proof shortened by AV, 17-Oct-2024.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉} & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑈) → 𝐺 ∈ 𝑈) | ||
Theorem | 1strwunOLD 17279 | Obsolete version of 1strwun 17278 as of 17-Oct-2024. A constructed one-slot structure in a weak universe. (Contributed by AV, 27-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉} & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑈) → 𝐺 ∈ 𝑈) | ||
Theorem | 2strstr 17280 | A constructed two-slot structure. Depending on hard-coded indices. Use 2strstr1 17283 instead. (Contributed by Mario Carneiro, 29-Aug-2015.) (New usage is discouraged.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉} & ⊢ 𝐸 = Slot 𝑁 & ⊢ 1 < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ 𝐺 Struct 〈1, 𝑁〉 | ||
Theorem | 2strbas 17281 | The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) Use the index-independent version 2strbas1 17285 instead. (New usage is discouraged.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉} & ⊢ 𝐸 = Slot 𝑁 & ⊢ 1 < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺)) | ||
Theorem | 2strop 17282 | The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) Use the index-independent version 2strop1 17286 instead. (New usage is discouraged.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉} & ⊢ 𝐸 = Slot 𝑁 & ⊢ 1 < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ ( + ∈ 𝑉 → + = (𝐸‘𝐺)) | ||
Theorem | 2strstr1 17283 | A constructed two-slot structure. Version of 2strstr 17280 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Proof shortened by AV, 17-Oct-2024.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈𝑁, + 〉} & ⊢ (Base‘ndx) < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ 𝐺 Struct 〈(Base‘ndx), 𝑁〉 | ||
Theorem | 2strstr1OLD 17284 | Obsolete version of 2strstr1 17283 as of 27-Oct-2024. A constructed two-slot structure. Version of 2strstr 17280 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈𝑁, + 〉} & ⊢ (Base‘ndx) < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ 𝐺 Struct 〈(Base‘ndx), 𝑁〉 | ||
Theorem | 2strbas1 17285 | The base set of a constructed two-slot structure. Version of 2strbas 17281 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈𝑁, + 〉} & ⊢ (Base‘ndx) < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺)) | ||
Theorem | 2strop1 17286 | The other slot of a constructed two-slot structure. Version of 2strop 17282 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈𝑁, + 〉} & ⊢ (Base‘ndx) < 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐸 = Slot 𝑁 ⇒ ⊢ ( + ∈ 𝑉 → + = (𝐸‘𝐺)) | ||
Syntax | cress 17287 | Extend class notation with the extensible structure builder restriction operator. |
class ↾s | ||
Definition | df-ress 17288* |
Define a multifunction restriction operator for extensible structures,
which can be used to turn statements about rings into statements about
subrings, modules into submodules, etc. This definition knows nothing
about individual structures and merely truncates the Base set while
leaving operators alone; individual kinds of structures will need to
handle this behavior, by ignoring operators' values outside the range
(like Ring), defining a function using the base
set and applying
that (like TopGrp), or explicitly truncating the
slot before use
(like MetSp).
(Credit for this operator goes to Mario Carneiro.) See ressbas 17293 for the altered base set, and resseqnbas 17300 (subrg0 20607, ressplusg 17349, subrg1 20610, ressmulr 17366) for the (un)altered other operations. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ ↾s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑥 ∩ (Base‘𝑤))〉))) | ||
Theorem | reldmress 17289 | The structure restriction is a proper operator, so it can be used with ovprc1 7487. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ Rel dom ↾s | ||
Theorem | ressval 17290 | Value of structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) | ||
Theorem | ressid2 17291 | General behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊) | ||
Theorem | ressval2 17292 | Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) | ||
Theorem | ressbas 17293 | Base set of a structure restriction. (Contributed by Stefan O'Rear, 26-Nov-2014.) (Proof shortened by AV, 7-Nov-2024.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) = (Base‘𝑅)) | ||
Theorem | ressbasOLD 17294 | Obsolete proof of ressbas 17293 as of 7-Nov-2024. Base set of a structure restriction. (Contributed by Stefan O'Rear, 26-Nov-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) = (Base‘𝑅)) | ||
Theorem | ressbasssg 17295 | The base set of a restriction to 𝐴 is a subset of 𝐴 and the base set 𝐵 of the original structure. (Contributed by SN, 10-Jan-2025.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (Base‘𝑅) ⊆ (𝐴 ∩ 𝐵) | ||
Theorem | ressbas2 17296 | Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅)) | ||
Theorem | ressbasss 17297 | The base set of a restriction is a subset of the base set of the original structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Proof shortened by SN, 25-Feb-2025.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (Base‘𝑅) ⊆ 𝐵 | ||
Theorem | ressbasssOLD 17298 | Obsolete proof of ressbas 17293 as of 25-Feb-2025. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (Base‘𝑅) ⊆ 𝐵 | ||
Theorem | ressbasss2 17299 | The base set of a restriction to 𝐴 is a subset of 𝐴. (Contributed by SN, 10-Jan-2025.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) ⇒ ⊢ (Base‘𝑅) ⊆ 𝐴 | ||
Theorem | resseqnbas 17300 | The components of an extensible structure except the base set remain unchanged on a structure restriction. (Contributed by Mario Carneiro, 26-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) (Revised by AV, 19-Oct-2024.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐶 = (𝐸‘𝑊) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (Base‘ndx) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐶 = (𝐸‘𝑅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |