P. 173 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17201-17300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	structn0fun 17201	A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021.)
⊢ (𝐹 Struct 𝑋 → Fun (𝐹 ∖ {∅}))
Theorem	isstruct 17202	The property of being a structure with components in 𝑀...𝑁. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ (𝐹 Struct ⟨𝑀, 𝑁⟩ ↔ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (𝑀...𝑁)))
Theorem	structcnvcnv 17203	Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ (𝐹 Struct 𝑋 → ◡◡𝐹 = (𝐹 ∖ {∅}))
Theorem	structfung 17204	The converse of the converse of a structure is a function. Closed form of structfun 17205. (Contributed by AV, 12-Nov-2021.)
⊢ (𝐹 Struct 𝑋 → Fun ◡◡𝐹)
Theorem	structfun 17205	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 17206	Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐹 Struct ⟨𝑀, 𝑁⟩    ⇒   ⊢ (Fun ◡◡𝐹 ∧ dom 𝐹 ⊆ (1...𝑁))
Theorem	strleun 17207	Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐹 Struct ⟨𝐴, 𝐵⟩    &   ⊢ 𝐺 Struct ⟨𝐶, 𝐷⟩    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ (𝐹 ∪ 𝐺) Struct ⟨𝐴, 𝐷⟩
Theorem	strle1 17208	Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    ⇒   ⊢ {⟨𝐴, 𝑋⟩} Struct ⟨𝐼, 𝐼⟩
Theorem	strle2 17209	Make a structure from a pair. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    &   ⊢ 𝐼 < 𝐽    &   ⊢ 𝐽 ∈ ℕ    &   ⊢ 𝐵 = 𝐽    ⇒   ⊢ {⟨𝐴, 𝑋⟩, ⟨𝐵, 𝑌⟩} Struct ⟨𝐼, 𝐽⟩
Theorem	strle3 17210	Make a structure from a triple. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐼 ∈ ℕ    &   ⊢ 𝐴 = 𝐼    &   ⊢ 𝐼 < 𝐽    &   ⊢ 𝐽 ∈ ℕ    &   ⊢ 𝐵 = 𝐽    &   ⊢ 𝐽 < 𝐾    &   ⊢ 𝐾 ∈ ℕ    &   ⊢ 𝐶 = 𝐾    ⇒   ⊢ {⟨𝐴, 𝑋⟩, ⟨𝐵, 𝑌⟩, ⟨𝐶, 𝑍⟩} Struct ⟨𝐼, 𝐾⟩
Theorem	sbcie2s 17211*	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 17212*	A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 15-Mar-2019.)
⊢ 𝐴 = (𝐸‘𝑊)    &   ⊢ 𝐵 = (𝐹‘𝑊)    &   ⊢ 𝐶 = (𝐺‘𝑊)    &   ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑤 = 𝑊 → ([(𝐸‘𝑤) / 𝑎][(𝐹‘𝑤) / 𝑏][(𝐺‘𝑤) / 𝑐]𝜓 ↔ 𝜑))
7.1.1.2  Substitution of components
Syntax	csts 17213	Set components of a structure.
class sSet
Definition	df-sets 17214*	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 17281 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 20208, 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 17215	The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ Rel dom sSet
Theorem	setsvalg 17216	Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑆 sSet 𝐴) = ((𝑆 ↾ (V ∖ dom {𝐴})) ∪ {𝐴}))
Theorem	setsval 17217	Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑆 sSet ⟨𝐴, 𝐵⟩) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐵⟩}))
Theorem	fvsetsid 17218	The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈) → ((𝐹 sSet ⟨𝑋, 𝑌⟩)‘𝑋) = 𝑌)
Theorem	fsets 17219	The structure replacement function is a function. (Contributed by SO, 12-Jul-2018.)
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝐹 sSet ⟨𝑋, 𝑌⟩):𝐴⟶𝐵)
Theorem	setsdm 17220	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 17221	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 17222	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 17221 is useful for proofs based on isstruct2 17199 which requires Fun (𝐹 ∖ {∅}) for 𝐹 to be an extensible structure. (Contributed by AV, 7-Jun-2021.)
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun ((𝐺 sSet ⟨𝐼, 𝐸⟩) ∖ {∅}))
Theorem	setsn0fun 17223	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 17224	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 17225*	An extensible structure with a replaced slot is an extensible structure. (Contributed by AV, 14-Nov-2021.)
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → ∃𝑦(𝐺 sSet ⟨𝐼, 𝐸⟩) Struct 𝑦)
Theorem	setsstruct 17226	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 17227	Closure of structure replacement in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑆 sSet 𝐴) ∈ 𝑈)
Theorem	setsres 17228	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 17229	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 17230	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 17231	Extend class notation with the slot function.
class Slot 𝐴
Definition	df-slot 17232*	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 18993)). 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 17246). 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 17260). 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 17262 and basendx 17268), except additionally in the discouraged theorem baseval 17261 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 17247, 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 17247). 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), + ⟩}. The slot extractor +g = Slot 2 (see df-plusg 17313) 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 17326). 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 6884). 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 17233	Equality theorem for the Slot construction. The converse holds if 𝐴 (or 𝐵) is a set. (Contributed by BJ, 27-Dec-2021.)
⊢ (𝐴 = 𝐵 → Slot 𝐴 = Slot 𝐵)
Theorem	slotfn 17234	A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐸 = Slot 𝑁    ⇒   ⊢ 𝐸 Fn V
Theorem	strfvnd 17235	Deduction version of strfvn 17236. (Contributed by Mario Carneiro, 15-Nov-2014.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐸‘𝑆) = (𝑆‘𝑁))
Theorem	strfvn 17236	Value of a structure component extractor 𝐸. Normally, 𝐸 is a defined constant symbol such as Base (df-base 17260) 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 17253 instead of strfvn 17236. (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2013.) (New usage is discouraged.)
⊢ 𝑆 ∈ V    &   ⊢ 𝐸 = Slot 𝑁    ⇒   ⊢ (𝐸‘𝑆) = (𝑆‘𝑁)
Theorem	strfvss 17237	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 17238	Closure of a structure index in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐸‘𝑆) ∈ 𝑈)
Theorem	str0 17239	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 17240	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 17241	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 21626. (Contributed by AV, 31-Oct-2024.)
⊢ (𝐸‘∅) = ∅    &   ⊢ 𝑌 = (𝐹‘𝑋)    ⇒   ⊢ (¬ 𝑋 ∈ V → (𝐸‘𝑋) = (𝐸‘𝑌))
Theorem	oveqprc 17242	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 33568. (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 17260 (see ndxarg 17246). For each defined structure component extractor, there should be a corresponding specific theorem providing its index, like basendx 17268. 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 17262 and basendxnplusgndx 17330. 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 48880, based on setsnid 17258) or even ordered (in proofs such as lmodstr 17368). 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 21496 with cnfldfunALT 21497). As for the inequalities, it is recommended to provide them explicitly as theorems like basendxnplusgndx 17330, 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 17329 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 17341), it is not recommended to provide explicit theorems for all of them, but to use the (discouraged) *ndx theorems as in lmodstr 17368. Therefore, *str theorems generally depend on the hard-coded values of the indices.
Syntax	cnx 17243	Extend class notation with the structure component index extractor.
class ndx
Definition	df-ndx 17244	Define the structure component index extractor. See Theorem ndxarg 17246 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 17260) another set such as the set of finite ordinals ω (df-om 7851). (Contributed by NM, 4-Sep-2011.)
⊢ ndx = ( I ↾ ℕ)
Theorem	wunndx 17245	Closure of the index extractor in an infinite weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    ⇒   ⊢ (𝜑 → ndx ∈ 𝑈)
Theorem	ndxarg 17246	Get the numeric argument from a defined structure component extractor such as df-base 17260. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝐸‘ndx) = 𝑁
Theorem	ndxid 17247	A structure component extractor is defined by its own index. This theorem, together with strfv 17253 below, is useful for avoiding direct reference to the hard-coded numeric index in component extractor definitions, such as the 1 in df-base 17260 and the ;10 in df-ple 17320, 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 17248	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 17235 directly with 𝑁 set to (𝐸‘ndx) if possible.
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝜑 → (𝑆‘(𝐸‘ndx)) = (𝐸‘𝑆))
Theorem	setsidvald 17249	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 17250	Deduction version of strfv 17253. (Contributed by Mario Carneiro, 15-Nov-2014.)
⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝑆)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆))
Theorem	strfv2d 17251	Deduction version of strfv2 17252. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → Fun ◡◡𝑆)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆))
Theorem	strfv2 17252	A variation on strfv 17253 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 17253	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 17260). By virtue of ndxid 17247, 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 17254	Variant on strfv 17253 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.)
⊢ (𝜑 → 𝑈 = 𝑆)    &   ⊢ 𝑆 Struct 𝑋    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ {⟨(𝐸‘ndx), 𝐶⟩} ⊆ 𝑆    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ 𝐴 = (𝐸‘𝑈)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	strssd 17255	Deduction version of strss 17256. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝑇)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑇)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐸‘𝑇) = (𝐸‘𝑆))
Theorem	strss 17256	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 17257	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 17258	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 ⟨𝐷, 𝐶⟩))
7.1.1.5  Base sets
Syntax	cbs 17259	Extend class notation with the class of all base set extractors.
class Base
Definition	df-base 17260	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 17262 instead. (New usage is discouraged.)
⊢ Base = Slot 1
Theorem	baseval 17261	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 17262	Utility theorem: index-independent form of df-base 17260. (Contributed by NM, 20-Oct-2012.)
⊢ Base = Slot (Base‘ndx)
Theorem	basfn 17263	The base set extractor is a function on V. (Contributed by Stefan O'Rear, 8-Jul-2015.)
⊢ Base Fn V
Theorem	base0 17264	The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ ∅ = (Base‘∅)
Theorem	elbasfv 17265	Utility theorem: reverse closure for any structure defined as a function. (Contributed by Stefan O'Rear, 24-Aug-2015.)
⊢ 𝑆 = (𝐹‘𝑍)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝑋 ∈ 𝐵 → 𝑍 ∈ V)
Theorem	elbasov 17266	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 17267	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 17268	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 17269	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 17270	The index of the base set is an element in a weak universe containing the natural numbers. Formerly part of proof for 1strwun 17276. (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. (Contributed by AV, 15-Nov-2024.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩}    ⇒   ⊢ 𝐺 Struct ⟨(Base‘ndx), (Base‘ndx)⟩
Theorem	1strbas 17274	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	1strwunbndx 17275	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 17276	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 17277	A constructed two-slot structure 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	2strbas 17278	The base set of a constructed two-slot structure not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨𝑁, + ⟩}    &   ⊢ (Base‘ndx) < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺))
Theorem	2strop 17279	The other slot of a constructed two-slot structure 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 17280	Extend class notation with the extensible structure builder restriction operator.
class ↾s
Definition	df-ress 17281*	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 17286 for the altered base set, and resseqnbas 17292 (subrg0 20655, ressplusg 17334, subrg1 20658, ressmulr 17350) 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 17282	The structure restriction is a proper operator, so it can be used with ovprc1 7439. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ Rel dom ↾s
Theorem	ressval 17283	Value of structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Base‘ndx), (𝐴 ∩ 𝐵)⟩)))
Theorem	ressid2 17284	General behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊)
Theorem	ressval2 17285	Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Base‘ndx), (𝐴 ∩ 𝐵)⟩))
Theorem	ressbas 17286	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	ressbasssg 17287	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 17288	Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅))
Theorem	ressbasss 17289	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 17290	Obsolete version of ressbas 17286 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 17291	The base set of a restriction to 𝐴 is a subset of 𝐴. (Contributed by SN, 10-Jan-2025.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    ⇒   ⊢ (Base‘𝑅) ⊆ 𝐴
Theorem	resseqnbas 17292	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	ress0 17293	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 17294	Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊)
Theorem	ressinbas 17295	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 17296	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 17297	Restriction composition law. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Proof shortened by Mario Carneiro, 2-Dec-2014.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))
Theorem	ressabs 17298	Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐵))
Theorem	wunress 17299	Closure of structure restriction in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 28-Oct-2024.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝑊 ↾s 𝐴) ∈ 𝑈)
7.1.2  Slot definitions
Syntax	cplusg 17300	Extend class notation with group (addition) operation.
class +g