| Metamath
Proof Explorer Theorem List (p. 173 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 | ||
| Definition | df-sets 17201* | 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 17275 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 20138, 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 17202 | The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
| ⊢ Rel dom sSet | ||
| Theorem | setsvalg 17203 | Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.) |
| ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑆 sSet 𝐴) = ((𝑆 ↾ (V ∖ dom {𝐴})) ∪ {𝐴})) | ||
| Theorem | setsval 17204 | Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
| ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑆 sSet 〈𝐴, 𝐵〉) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐵〉})) | ||
| Theorem | fvsetsid 17205 | The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018.) |
| ⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈) → ((𝐹 sSet 〈𝑋, 𝑌〉)‘𝑋) = 𝑌) | ||
| Theorem | fsets 17206 | The structure replacement function is a function. (Contributed by SO, 12-Jul-2018.) |
| ⊢ (((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝐹 sSet 〈𝑋, 𝑌〉):𝐴⟶𝐵) | ||
| Theorem | setsdm 17207 | 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 17208 | 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 17209 | 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 17208 is useful for proofs based on isstruct2 17186 which requires Fun (𝐹 ∖ {∅}) for 𝐹 to be an extensible structure. (Contributed by AV, 7-Jun-2021.) |
| ⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅})) | ||
| Theorem | setsn0fun 17210 | 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 17211 | 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 17212* | An extensible structure with a replaced slot is an extensible structure. (Contributed by AV, 14-Nov-2021.) |
| ⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → ∃𝑦(𝐺 sSet 〈𝐼, 𝐸〉) Struct 𝑦) | ||
| Theorem | setsstruct 17213 | 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 17214 | Closure of structure replacement in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝑆 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑆 sSet 𝐴) ∈ 𝑈) | ||
| Theorem | setsres 17215 | 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 17216 | 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 17217 | 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 17218 | Extend class notation with the slot function. |
| class Slot 𝐴 | ||
| Definition | df-slot 17219* |
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 18359) or a group (df-grp 18954)).
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 17233). 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 17248). 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 17250 and basendx 17256), except additionally in the discouraged theorem baseval 17249 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 17234, 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 17234). 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 17328). The slot extractor +g = Slot 2 (see df-plusg 17310) 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 17323). 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 6919). 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 17220 | Equality theorem for the Slot construction. The converse holds if 𝐴 (or 𝐵) is a set. (Contributed by BJ, 27-Dec-2021.) |
| ⊢ (𝐴 = 𝐵 → Slot 𝐴 = Slot 𝐵) | ||
| Theorem | slotfn 17221 | A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.) |
| ⊢ 𝐸 = Slot 𝑁 ⇒ ⊢ 𝐸 Fn V | ||
| Theorem | strfvnd 17222 | Deduction version of strfvn 17223. (Contributed by Mario Carneiro, 15-Nov-2014.) |
| ⊢ 𝐸 = Slot 𝑁 & ⊢ (𝜑 → 𝑆 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐸‘𝑆) = (𝑆‘𝑁)) | ||
| Theorem | strfvn 17223 |
Value of a structure component extractor 𝐸. Normally, 𝐸 is a
defined constant symbol such as Base (df-base 17248) 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 18359) 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 17240 instead of strfvn 17223. (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2013.) (New usage is discouraged.) |
| ⊢ 𝑆 ∈ V & ⊢ 𝐸 = Slot 𝑁 ⇒ ⊢ (𝐸‘𝑆) = (𝑆‘𝑁) | ||
| Theorem | strfvss 17224 | 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 17225 | Closure of a structure index in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ 𝐸 = Slot 𝑁 & ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → 𝑆 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐸‘𝑆) ∈ 𝑈) | ||
| Theorem | str0 17226 | 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 17227 | 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 17228 | 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 21527. (Contributed by AV, 31-Oct-2024.) |
| ⊢ (𝐸‘∅) = ∅ & ⊢ 𝑌 = (𝐹‘𝑋) ⇒ ⊢ (¬ 𝑋 ∈ V → (𝐸‘𝑋) = (𝐸‘𝑌)) | ||
| Theorem | oveqprc 17229 | 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 33357. (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 17248 (see ndxarg 17233). For each defined structure component extractor, there should be a corresponding specific theorem providing its index, like basendx 17256. 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 17250 and basendxnplusgndx 17327. 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 48176, based on setsnid 17245) or even ordered (in proofs such as lmodstr 17369). 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 21378 with cnfldfunALT 21379). As for the inequalities, it is recommended to provide them explicitly as theorems like basendxnplusgndx 17327, 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 17326 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 17342), it is not recommended to provide explicit theorems for all of them, but to use the (discouraged) *ndx theorems as in lmodstr 17369. Therefore, *str theorems generally depend on the hard-coded values of the indices. | ||
| Syntax | cnx 17230 | Extend class notation with the structure component index extractor. |
| class ndx | ||
| Definition | df-ndx 17231 | Define the structure component index extractor. See Theorem ndxarg 17233 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 17248) another set such as the set of finite ordinals ω (df-om 7888). (Contributed by NM, 4-Sep-2011.) |
| ⊢ ndx = ( I ↾ ℕ) | ||
| Theorem | wunndx 17232 | Closure of the index extractor in an infinite weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) ⇒ ⊢ (𝜑 → ndx ∈ 𝑈) | ||
| Theorem | ndxarg 17233 | Get the numeric argument from a defined structure component extractor such as df-base 17248. (Contributed by Mario Carneiro, 6-Oct-2013.) |
| ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐸‘ndx) = 𝑁 | ||
| Theorem | ndxid 17234 |
A structure component extractor is defined by its own index. This
theorem, together with strfv 17240 below, is useful for avoiding direct
reference to the hard-coded numeric index in component extractor
definitions, such as the 1 in df-base 17248 and the ;10 in
df-ple 17317, 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 17235 | 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 17222 directly with 𝑁 set to (𝐸‘ndx) if possible. |
| ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝜑 → (𝑆‘(𝐸‘ndx)) = (𝐸‘𝑆)) | ||
| Theorem | setsidvald 17236 |
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 | strfvd 17237 | Deduction version of strfv 17240. (Contributed by Mario Carneiro, 15-Nov-2014.) |
| ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝑆) & ⊢ (𝜑 → 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆)) | ||
| Theorem | strfv2d 17238 | Deduction version of strfv2 17239. (Contributed by Mario Carneiro, 30-Apr-2015.) |
| ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → Fun ◡◡𝑆) & ⊢ (𝜑 → 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆)) | ||
| Theorem | strfv2 17239 | A variation on strfv 17240 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 17240 | Extract a structure component 𝐶 (such as the base set) from a structure 𝑆 (such as a member of Poset, df-poset 18359) with a component extractor 𝐸 (such as the base set extractor df-base 17248). By virtue of ndxid 17234, 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 17241 | Variant on strfv 17240 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.) |
| ⊢ (𝜑 → 𝑈 = 𝑆) & ⊢ 𝑆 Struct 𝑋 & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ {〈(𝐸‘ndx), 𝐶〉} ⊆ 𝑆 & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ 𝐴 = (𝐸‘𝑈) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
| Theorem | strssd 17242 | Deduction version of strss 17243. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
| ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝑇) & ⊢ (𝜑 → 𝑆 ⊆ 𝑇) & ⊢ (𝜑 → 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸‘𝑇) = (𝐸‘𝑆)) | ||
| Theorem | strss 17243 | 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 17244 | 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 17245 | 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 17246 | Obsolete version of setsnid 17245 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 17247 | Extend class notation with the class of all base set extractors. |
| class Base | ||
| Definition | df-base 17248 | 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 17250 instead. (New usage is discouraged.) |
| ⊢ Base = Slot 1 | ||
| Theorem | baseval 17249 | 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 17250 | Utility theorem: index-independent form of df-base 17248. (Contributed by NM, 20-Oct-2012.) |
| ⊢ Base = Slot (Base‘ndx) | ||
| Theorem | basfn 17251 | The base set extractor is a function on V. (Contributed by Stefan O'Rear, 8-Jul-2015.) |
| ⊢ Base Fn V | ||
| Theorem | base0 17252 | The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.) |
| ⊢ ∅ = (Base‘∅) | ||
| Theorem | elbasfv 17253 | Utility theorem: reverse closure for any structure defined as a function. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
| ⊢ 𝑆 = (𝐹‘𝑍) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝑋 ∈ 𝐵 → 𝑍 ∈ V) | ||
| Theorem | elbasov 17254 | 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 17255 | 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 17256 | 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 17257 | 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 | basndxelwund 17258 | The index of the base set is an element in a weak universe containing the natural numbers. Formerly part of proof for 1strwun 17266. (Contributed by AV, 27-Mar-2020.) (Revised by AV, 17-Oct-2024.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) ⇒ ⊢ (𝜑 → (Base‘ndx) ∈ 𝑈) | ||
| Theorem | basprssdmsets 17259 | 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 17260 | The base set of a structure with a base set. (Contributed by AV, 10-Nov-2021.) |
| ⊢ (𝜑 → 𝑆 Struct 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 〈(Base‘ndx), 𝑉〉 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑉 = (Base‘𝑆)) | ||
| Theorem | 1strstr 17261 | A constructed one-slot structure. Depending on hard-coded index. Use 1strstr1 17262 instead. (Contributed by AV, 27-Mar-2020.) (New usage is discouraged.) |
| ⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉} ⇒ ⊢ 𝐺 Struct 〈1, 1〉 | ||
| Theorem | 1strstr1 17262 | A constructed one-slot structure. (Contributed by AV, 15-Nov-2024.) |
| ⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉} ⇒ ⊢ 𝐺 Struct 〈(Base‘ndx), (Base‘ndx)〉 | ||
| Theorem | 1strbas 17263 | 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 17264 | Obsolete version of 1strbas 17263 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 17265 | 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 17266 | 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 | 2strstr 17267 | A constructed two-slot structure. Depending on hard-coded indices. Use 2strstr1 17270 instead. (Contributed by Mario Carneiro, 29-Aug-2015.) (New usage is discouraged.) |
| ⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉} & ⊢ 𝐸 = Slot 𝑁 & ⊢ 1 < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ 𝐺 Struct 〈1, 𝑁〉 | ||
| Theorem | 2strbas 17268 | The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) Use the index-independent version 2strbas1 17272 instead. (New usage is discouraged.) |
| ⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉} & ⊢ 𝐸 = Slot 𝑁 & ⊢ 1 < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺)) | ||
| Theorem | 2strop 17269 | The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) Use the index-independent version 2strop1 17273 instead. (New usage is discouraged.) |
| ⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉} & ⊢ 𝐸 = Slot 𝑁 & ⊢ 1 < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ ( + ∈ 𝑉 → + = (𝐸‘𝐺)) | ||
| Theorem | 2strstr1 17270 | A constructed two-slot structure. Version of 2strstr 17267 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 17271 | Obsolete version of 2strstr1 17270 as of 27-Oct-2024. A constructed two-slot structure. Version of 2strstr 17267 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 17272 | The base set of a constructed two-slot structure. Version of 2strbas 17268 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 17273 | The other slot of a constructed two-slot structure. Version of 2strop 17269 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 17274 | Extend class notation with the extensible structure builder restriction operator. |
| class ↾s | ||
| Definition | df-ress 17275* |
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 17280 for the altered base set, and resseqnbas 17287 (subrg0 20579, ressplusg 17334, subrg1 20582, ressmulr 17351) 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 17276 | The structure restriction is a proper operator, so it can be used with ovprc1 7470. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
| ⊢ Rel dom ↾s | ||
| Theorem | ressval 17277 | Value of structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
| ⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉))) | ||
| Theorem | ressid2 17278 | General behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
| ⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊) | ||
| Theorem | ressval2 17279 | Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
| ⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) | ||
| Theorem | ressbas 17280 | 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 17281 | Obsolete version of ressbas 17280 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 17282 | 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 17283 | Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.) |
| ⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅)) | ||
| Theorem | ressbasss 17284 | 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 17285 | Obsolete version of ressbas 17280 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 17286 | The base set of a restriction to 𝐴 is a subset of 𝐴. (Contributed by SN, 10-Jan-2025.) |
| ⊢ 𝑅 = (𝑊 ↾s 𝐴) ⇒ ⊢ (Base‘𝑅) ⊆ 𝐴 | ||
| Theorem | resseqnbas 17287 | 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) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐶 = (𝐸‘𝑅)) | ||
| Theorem | resslemOLD 17288 | Obsolete version of resseqnbas 17287 as of 21-Oct-2024. (Contributed by Mario Carneiro, 26-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐶 = (𝐸‘𝑊) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 1 < 𝑁 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐶 = (𝐸‘𝑅)) | ||
| Theorem | ress0 17289 | All restrictions of the null set are trivial. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
| ⊢ (∅ ↾s 𝐴) = ∅ | ||
| Theorem | ressid 17290 | Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
| ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊) | ||
| Theorem | ressinbas 17291 | Restriction only cares about the part of the second set which intersects the base of the first. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
| ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝐴 ∈ 𝑋 → (𝑊 ↾s 𝐴) = (𝑊 ↾s (𝐴 ∩ 𝐵))) | ||
| Theorem | ressval3d 17292 | Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by AV, 3-Jul-2022.) (Proof shortened by AV, 17-Oct-2024.) |
| ⊢ 𝑅 = (𝑆 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐸 = (Base‘ndx) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝑆) & ⊢ (𝜑 → 𝐸 ∈ dom 𝑆) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝑅 = (𝑆 sSet 〈𝐸, 𝐴〉)) | ||
| Theorem | ressress 17293 | Restriction composition law. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Proof shortened by Mario Carneiro, 2-Dec-2014.) |
| ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) | ||
| Theorem | ressabs 17294 | Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015.) |
| ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐵)) | ||
| Theorem | wunress 17295 | Closure of structure restriction in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 28-Oct-2024.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑊 ↾s 𝐴) ∈ 𝑈) | ||
| Theorem | wunressOLD 17296 | Obsolete version of wunress 17295 as of 28-Oct-2024. Closure of structure restriction in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑊 ↾s 𝐴) ∈ 𝑈) | ||
| Syntax | cplusg 17297 | Extend class notation with group (addition) operation. |
| class +g | ||
| Syntax | cmulr 17298 | Extend class notation with ring multiplication. |
| class .r | ||
| Syntax | cstv 17299 | Extend class notation with involution. |
| class *𝑟 | ||
| Syntax | csca 17300 | Extend class notation with scalar field. |
| class Scalar | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |