P. 172 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17101-17200   *Has distinct variable group(s)

Type	Label	Description
Statement
7.1.1.2  Substitution of components
Syntax	csts 17101	Set components of a structure.
class sSet
Definition	df-sets 17102*	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 17179 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 20030, 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 17103	The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ Rel dom sSet
Theorem	setsvalg 17104	Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑆 sSet 𝐴) = ((𝑆 ↾ (V ∖ dom {𝐴})) ∪ {𝐴}))
Theorem	setsval 17105	Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑆 sSet ⟨𝐴, 𝐵⟩) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐵⟩}))
Theorem	fvsetsid 17106	The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈) → ((𝐹 sSet ⟨𝑋, 𝑌⟩)‘𝑋) = 𝑌)
Theorem	fsets 17107	The structure replacement function is a function. (Contributed by SO, 12-Jul-2018.)
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝐹 sSet ⟨𝑋, 𝑌⟩):𝐴⟶𝐵)
Theorem	setsdm 17108	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 17109	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 17110	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 17109 is useful for proofs based on isstruct2 17087 which requires Fun (𝐹 ∖ {∅}) for 𝐹 to be an extensible structure. (Contributed by AV, 7-Jun-2021.)
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun ((𝐺 sSet ⟨𝐼, 𝐸⟩) ∖ {∅}))
Theorem	setsn0fun 17111	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 17112	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 17113*	An extensible structure with a replaced slot is an extensible structure. (Contributed by AV, 14-Nov-2021.)
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → ∃𝑦(𝐺 sSet ⟨𝐼, 𝐸⟩) Struct 𝑦)
Theorem	setsstruct 17114	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 17115	Closure of structure replacement in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑆 sSet 𝐴) ∈ 𝑈)
Theorem	setsres 17116	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 17117	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 17118	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 ⟨𝐴, 𝐶⟩))
7.1.1.3  Slots
Syntax	cslot 17119	Extend class notation with the slot function.
class Slot 𝐴
Definition	df-slot 17120*	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 18271) or a group (df-grp 18859)). 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 17134). 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 17150). 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 17152 and basendx 17158), except additionally in the discouraged theorem baseval 17151 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 17135, 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 17135). 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 17234). The slot extractor +g = Slot 2 (see df-plusg 17215) applied on the structure 𝐺 provides the group operation + = (+g‘𝐺). Expanding the defintions, we get + = (Slot 2‘𝐺) = (𝐺‘2) = (𝐺‘(+g‘ndx)) (for the last equation, see plusgndx 17228). 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 6905). 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 17121	Equality theorem for the Slot construction. The converse holds if 𝐴 (or 𝐵) is a set. (Contributed by BJ, 27-Dec-2021.)
⊢ (𝐴 = 𝐵 → Slot 𝐴 = Slot 𝐵)
Theorem	slotfn 17122	A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐸 = Slot 𝑁    ⇒   ⊢ 𝐸 Fn V
Theorem	strfvnd 17123	Deduction version of strfvn 17124. (Contributed by Mario Carneiro, 15-Nov-2014.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐸‘𝑆) = (𝑆‘𝑁))
Theorem	strfvn 17124	Value of a structure component extractor 𝐸. Normally, 𝐸 is a defined constant symbol such as Base (df-base 17150) 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 18271) 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 17142 instead of strfvn 17124. (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2013.) (New usage is discouraged.)
⊢ 𝑆 ∈ V    &   ⊢ 𝐸 = Slot 𝑁    ⇒   ⊢ (𝐸‘𝑆) = (𝑆‘𝑁)
Theorem	strfvss 17125	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 17126	Closure of a structure index in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐸‘𝑆) ∈ 𝑈)
Theorem	str0 17127	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 17128	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 17129	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 21286. (Contributed by AV, 31-Oct-2024.)
⊢ (𝐸‘∅) = ∅    &   ⊢ 𝑌 = (𝐹‘𝑋)    ⇒   ⊢ (¬ 𝑋 ∈ V → (𝐸‘𝑋) = (𝐸‘𝑌))
Theorem	oveqprc 17130	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 32712. (Contributed by AV, 31-Oct-2024.)
⊢ (𝐸‘∅) = ∅    &   ⊢ 𝑍 = (𝑋𝑂𝑌)    &   ⊢ Rel dom 𝑂    ⇒   ⊢ (¬ 𝑋 ∈ V → (𝐸‘𝑋) = (𝐸‘𝑍))
7.1.1.4  Structure component indices 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 17150 (see ndxarg 17134). For each defined structure component extractor, there should be a corresponding specific theorem providing its index, like basendx 17158. 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 17152 and basendxnplusgndx 17232. 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 46942, based on setsnid 17147) or even ordered (in proofs such as lmodstr 17275). 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 21157 with cnfldfunALT 21158). As for the inequalities, it is recommended to provide them explicitly as theorems like basendxnplusgndx 17232, 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 17231 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 17248), it is not recommended to provide explicit theorems for all of them, but to use the (discouraged) *ndx theorems as in lmodstr 17275. Therefore, *str theorems generally depend on the hard-coded values of the indices.
Syntax	cnx 17131	Extend class notation with the structure component index extractor.
class ndx
Definition	df-ndx 17132	Define the structure component index extractor. See Theorem ndxarg 17134 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 17150) another set such as the set of finite ordinals ω (df-om 7859). (Contributed by NM, 4-Sep-2011.)
⊢ ndx = ( I ↾ ℕ)
Theorem	wunndx 17133	Closure of the index extractor in an infinite weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    ⇒   ⊢ (𝜑 → ndx ∈ 𝑈)
Theorem	ndxarg 17134	Get the numeric argument from a defined structure component extractor such as df-base 17150. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝐸‘ndx) = 𝑁
Theorem	ndxid 17135	A structure component extractor is defined by its own index. This theorem, together with strfv 17142 below, is useful for avoiding direct reference to the hard-coded numeric index in component extractor definitions, such as the 1 in df-base 17150 and the ;10 in df-ple 17222, 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 17136	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 17123 directly with 𝑁 set to (𝐸‘ndx) if possible.
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝜑 → (𝑆‘(𝐸‘ndx)) = (𝐸‘𝑆))
Theorem	setsidvald 17137	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 17138	Obsolete version of setsidvald 17137 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 17139	Deduction version of strfv 17142. (Contributed by Mario Carneiro, 15-Nov-2014.)
⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝑆)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆))
Theorem	strfv2d 17140	Deduction version of strfv2 17141. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → Fun ◡◡𝑆)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆))
Theorem	strfv2 17141	A variation on strfv 17142 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 17142	Extract a structure component 𝐶 (such as the base set) from a structure 𝑆 (such as a member of Poset, df-poset 18271) with a component extractor 𝐸 (such as the base set extractor df-base 17150). By virtue of ndxid 17135, 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 17143	Variant on strfv 17142 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.)
⊢ (𝜑 → 𝑈 = 𝑆)    &   ⊢ 𝑆 Struct 𝑋    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ {⟨(𝐸‘ndx), 𝐶⟩} ⊆ 𝑆    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ 𝐴 = (𝐸‘𝑈)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	strssd 17144	Deduction version of strss 17145. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝑇)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑇)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐸‘𝑇) = (𝐸‘𝑆))
Theorem	strss 17145	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 17146	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 17147	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 17148	Obsolete proof of setsnid 17147 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 ⟨𝐷, 𝐶⟩))
7.1.1.5  Base sets
Syntax	cbs 17149	Extend class notation with the class of all base set extractors.
class Base
Definition	df-base 17150	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 17152 instead. (New usage is discouraged.)
⊢ Base = Slot 1
Theorem	baseval 17151	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 17152	Utility theorem: index-independent form of df-base 17150. (Contributed by NM, 20-Oct-2012.)
⊢ Base = Slot (Base‘ndx)
Theorem	basfn 17153	The base set extractor is a function on V. (Contributed by Stefan O'Rear, 8-Jul-2015.)
⊢ Base Fn V
Theorem	base0 17154	The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ ∅ = (Base‘∅)
Theorem	elbasfv 17155	Utility theorem: reverse closure for any structure defined as a function. (Contributed by Stefan O'Rear, 24-Aug-2015.)
⊢ 𝑆 = (𝐹‘𝑍)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝑋 ∈ 𝐵 → 𝑍 ∈ V)
Theorem	elbasov 17156	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 17157	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 17158	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 17159	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 17160	Obsolete proof of basendxnn 17159 as of 13-Oct-2024. (Contributed by AV, 23-Sep-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Base‘ndx) ∈ ℕ
Theorem	basndxelwund 17161	The index of the base set is an element in a weak universe containing the natural numbers. Formerly part of proof for 1strwun 17169. (Contributed by AV, 27-Mar-2020.) (Revised by AV, 17-Oct-2024.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    ⇒   ⊢ (𝜑 → (Base‘ndx) ∈ 𝑈)
Theorem	basprssdmsets 17162	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 17163	The base set of a structure with a base set. (Contributed by AV, 10-Nov-2021.)
⊢ (𝜑 → 𝑆 Struct 𝑋)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑌)    &   ⊢ (𝜑 → ⟨(Base‘ndx), 𝑉⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑉 = (Base‘𝑆))
Theorem	1strstr 17164	A constructed one-slot structure. Depending on hard-coded index. Use 1strstr1 17165 instead. (Contributed by AV, 27-Mar-2020.) (New usage is discouraged.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩}    ⇒   ⊢ 𝐺 Struct ⟨1, 1⟩
Theorem	1strstr1 17165	A constructed one-slot structure. (Contributed by AV, 15-Nov-2024.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩}    ⇒   ⊢ 𝐺 Struct ⟨(Base‘ndx), (Base‘ndx)⟩
Theorem	1strbas 17166	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 17167	Obsolete proof of 1strbas 17166 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 17168	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 17169	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 17170	Obsolete version of 1strwun 17169 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 17171	A constructed two-slot structure. Depending on hard-coded indices. Use 2strstr1 17174 instead. (Contributed by Mario Carneiro, 29-Aug-2015.) (New usage is discouraged.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩}    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 1 < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ 𝐺 Struct ⟨1, 𝑁⟩
Theorem	2strbas 17172	The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) Use the index-independent version 2strbas1 17176 instead. (New usage is discouraged.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩}    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 1 < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺))
Theorem	2strop 17173	The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) Use the index-independent version 2strop1 17177 instead. (New usage is discouraged.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩}    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 1 < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ( + ∈ 𝑉 → + = (𝐸‘𝐺))
Theorem	2strstr1 17174	A constructed two-slot structure. Version of 2strstr 17171 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 17175	Obsolete version of 2strstr1 17174 as of 27-Oct-2024. A constructed two-slot structure. Version of 2strstr 17171 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 17176	The base set of a constructed two-slot structure. Version of 2strbas 17172 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 17177	The other slot of a constructed two-slot structure. Version of 2strop 17173 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨𝑁, + ⟩}    &   ⊢ (Base‘ndx) < 𝑁    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐸 = Slot 𝑁    ⇒   ⊢ ( + ∈ 𝑉 → + = (𝐸‘𝐺))
7.1.1.6  Base set restrictions
Syntax	cress 17178	Extend class notation with the extensible structure builder restriction operator.
class ↾s
Definition	df-ress 17179*	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 17184 for the altered base set, and resseqnbas 17191 (subrg0 20470, ressplusg 17240, subrg1 20473, ressmulr 17257) 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 17180	The structure restriction is a proper operator, so it can be used with ovprc1 7451. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ Rel dom ↾s
Theorem	ressval 17181	Value of structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Base‘ndx), (𝐴 ∩ 𝐵)⟩)))
Theorem	ressid2 17182	General behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊)
Theorem	ressval2 17183	Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Base‘ndx), (𝐴 ∩ 𝐵)⟩))
Theorem	ressbas 17184	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 17185	Obsolete proof of ressbas 17184 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 17186	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 17187	Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅))
Theorem	ressbasss 17188	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 17189	Obsolete proof of ressbas 17184 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 17190	The base set of a restriction to 𝐴 is a subset of 𝐴. (Contributed by SN, 10-Jan-2025.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    ⇒   ⊢ (Base‘𝑅) ⊆ 𝐴
Theorem	resseqnbas 17191	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 17192	Obsolete version of resseqnbas 17191 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 17193	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 17194	Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊)
Theorem	ressinbas 17195	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 17196	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	ressval3dOLD 17197	Obsolete version of ressval3d 17196 as of 17-Oct-2024. Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by AV, 3-Jul-2022.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑅 = (𝑆 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐸 = (Base‘ndx)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝑆)    &   ⊢ (𝜑 → 𝐸 ∈ dom 𝑆)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝑅 = (𝑆 sSet ⟨𝐸, 𝐴⟩))
Theorem	ressress 17198	Restriction composition law. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Proof shortened by Mario Carneiro, 2-Dec-2014.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))
Theorem	ressabs 17199	Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐵))
Theorem	wunress 17200	Closure of structure restriction in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 28-Oct-2024.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑊 ↾s 𝐴) ∈ 𝑈)