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	strfvn 17201	Value of a structure component extractor 𝐸. Normally, 𝐸 is a defined constant symbol such as Base (df-base 17227) 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 18351) 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 17219 instead of strfvn 17201. (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2013.) (New usage is discouraged.)
⊢ 𝑆 ∈ V    &   ⊢ 𝐸 = Slot 𝑁    ⇒   ⊢ (𝐸‘𝑆) = (𝑆‘𝑁)
Theorem	strfvss 17202	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 17203	Closure of a structure index in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐸‘𝑆) ∈ 𝑈)
Theorem	str0 17204	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 17205	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 17206	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 21518. (Contributed by AV, 31-Oct-2024.)
⊢ (𝐸‘∅) = ∅    &   ⊢ 𝑌 = (𝐹‘𝑋)    ⇒   ⊢ (¬ 𝑋 ∈ V → (𝐸‘𝑋) = (𝐸‘𝑌))
Theorem	oveqprc 17207	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 33267. (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 17227 (see ndxarg 17211). For each defined structure component extractor, there should be a corresponding specific theorem providing its index, like basendx 17235. 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 17229 and basendxnplusgndx 17309. 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 47759, based on setsnid 17224) or even ordered (in proofs such as lmodstr 17352). 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 21369 with cnfldfunALT 21370). As for the inequalities, it is recommended to provide them explicitly as theorems like basendxnplusgndx 17309, 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 17308 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 17325), it is not recommended to provide explicit theorems for all of them, but to use the (discouraged) *ndx theorems as in lmodstr 17352. Therefore, *str theorems generally depend on the hard-coded values of the indices.
Syntax	cnx 17208	Extend class notation with the structure component index extractor.
class ndx
Definition	df-ndx 17209	Define the structure component index extractor. See Theorem ndxarg 17211 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 17227) another set such as the set of finite ordinals ω (df-om 7882). (Contributed by NM, 4-Sep-2011.)
⊢ ndx = ( I ↾ ℕ)
Theorem	wunndx 17210	Closure of the index extractor in an infinite weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    ⇒   ⊢ (𝜑 → ndx ∈ 𝑈)
Theorem	ndxarg 17211	Get the numeric argument from a defined structure component extractor such as df-base 17227. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝐸‘ndx) = 𝑁
Theorem	ndxid 17212	A structure component extractor is defined by its own index. This theorem, together with strfv 17219 below, is useful for avoiding direct reference to the hard-coded numeric index in component extractor definitions, such as the 1 in df-base 17227 and the ;10 in df-ple 17299, 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 17213	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 17200 directly with 𝑁 set to (𝐸‘ndx) if possible.
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝜑 → (𝑆‘(𝐸‘ndx)) = (𝐸‘𝑆))
Theorem	setsidvald 17214	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 17215	Obsolete version of setsidvald 17214 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 17216	Deduction version of strfv 17219. (Contributed by Mario Carneiro, 15-Nov-2014.)
⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝑆)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆))
Theorem	strfv2d 17217	Deduction version of strfv2 17218. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → Fun ◡◡𝑆)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆))
Theorem	strfv2 17218	A variation on strfv 17219 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 17219	Extract a structure component 𝐶 (such as the base set) from a structure 𝑆 (such as a member of Poset, df-poset 18351) with a component extractor 𝐸 (such as the base set extractor df-base 17227). By virtue of ndxid 17212, 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 17220	Variant on strfv 17219 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.)
⊢ (𝜑 → 𝑈 = 𝑆)    &   ⊢ 𝑆 Struct 𝑋    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ {⟨(𝐸‘ndx), 𝐶⟩} ⊆ 𝑆    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ 𝐴 = (𝐸‘𝑈)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	strssd 17221	Deduction version of strss 17222. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝑇)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑇)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐸‘𝑇) = (𝐸‘𝑆))
Theorem	strss 17222	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 17223	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 17224	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 17225	Obsolete proof of setsnid 17224 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 17226	Extend class notation with the class of all base set extractors.
class Base
Definition	df-base 17227	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 17229 instead. (New usage is discouraged.)
⊢ Base = Slot 1
Theorem	baseval 17228	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 17229	Utility theorem: index-independent form of df-base 17227. (Contributed by NM, 20-Oct-2012.)
⊢ Base = Slot (Base‘ndx)
Theorem	basfn 17230	The base set extractor is a function on V. (Contributed by Stefan O'Rear, 8-Jul-2015.)
⊢ Base Fn V
Theorem	base0 17231	The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ ∅ = (Base‘∅)
Theorem	elbasfv 17232	Utility theorem: reverse closure for any structure defined as a function. (Contributed by Stefan O'Rear, 24-Aug-2015.)
⊢ 𝑆 = (𝐹‘𝑍)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝑋 ∈ 𝐵 → 𝑍 ∈ V)
Theorem	elbasov 17233	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 17234	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 17235	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 17236	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 17237	Obsolete proof of basendxnn 17236 as of 13-Oct-2024. (Contributed by AV, 23-Sep-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Base‘ndx) ∈ ℕ
Theorem	basndxelwund 17238	The index of the base set is an element in a weak universe containing the natural numbers. Formerly part of proof for 1strwun 17246. (Contributed by AV, 27-Mar-2020.) (Revised by AV, 17-Oct-2024.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    ⇒   ⊢ (𝜑 → (Base‘ndx) ∈ 𝑈)
Theorem	basprssdmsets 17239	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 17240	The base set of a structure with a base set. (Contributed by AV, 10-Nov-2021.)
⊢ (𝜑 → 𝑆 Struct 𝑋)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑌)    &   ⊢ (𝜑 → ⟨(Base‘ndx), 𝑉⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝑉 = (Base‘𝑆))
Theorem	1strstr 17241	A constructed one-slot structure. Depending on hard-coded index. Use 1strstr1 17242 instead. (Contributed by AV, 27-Mar-2020.) (New usage is discouraged.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩}    ⇒   ⊢ 𝐺 Struct ⟨1, 1⟩
Theorem	1strstr1 17242	A constructed one-slot structure. (Contributed by AV, 15-Nov-2024.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩}    ⇒   ⊢ 𝐺 Struct ⟨(Base‘ndx), (Base‘ndx)⟩
Theorem	1strbas 17243	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 17244	Obsolete proof of 1strbas 17243 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 17245	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 17246	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 17247	Obsolete version of 1strwun 17246 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 17248	A constructed two-slot structure. Depending on hard-coded indices. Use 2strstr1 17251 instead. (Contributed by Mario Carneiro, 29-Aug-2015.) (New usage is discouraged.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩}    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 1 < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ 𝐺 Struct ⟨1, 𝑁⟩
Theorem	2strbas 17249	The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) Use the index-independent version 2strbas1 17253 instead. (New usage is discouraged.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩}    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 1 < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺))
Theorem	2strop 17250	The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) Use the index-independent version 2strop1 17254 instead. (New usage is discouraged.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩}    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 1 < 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ( + ∈ 𝑉 → + = (𝐸‘𝐺))
Theorem	2strstr1 17251	A constructed two-slot structure. Version of 2strstr 17248 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 17252	Obsolete version of 2strstr1 17251 as of 27-Oct-2024. A constructed two-slot structure. Version of 2strstr 17248 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 17253	The base set of a constructed two-slot structure. Version of 2strbas 17249 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 17254	The other slot of a constructed two-slot structure. Version of 2strop 17250 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 17255	Extend class notation with the extensible structure builder restriction operator.
class ↾s
Definition	df-ress 17256*	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 17261 for the altered base set, and resseqnbas 17268 (subrg0 20575, ressplusg 17317, subrg1 20578, ressmulr 17334) 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 17257	The structure restriction is a proper operator, so it can be used with ovprc1 7466. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ Rel dom ↾s
Theorem	ressval 17258	Value of structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Base‘ndx), (𝐴 ∩ 𝐵)⟩)))
Theorem	ressid2 17259	General behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊)
Theorem	ressval2 17260	Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Base‘ndx), (𝐴 ∩ 𝐵)⟩))
Theorem	ressbas 17261	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 17262	Obsolete proof of ressbas 17261 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 17263	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 17264	Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅))
Theorem	ressbasss 17265	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 17266	Obsolete proof of ressbas 17261 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 17267	The base set of a restriction to 𝐴 is a subset of 𝐴. (Contributed by SN, 10-Jan-2025.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    ⇒   ⊢ (Base‘𝑅) ⊆ 𝐴
Theorem	resseqnbas 17268	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 17269	Obsolete version of resseqnbas 17268 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 17270	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 17271	Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊)
Theorem	ressinbas 17272	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 17273	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 17274	Obsolete version of ressval3d 17273 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 17275	Restriction composition law. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Proof shortened by Mario Carneiro, 2-Dec-2014.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))
Theorem	ressabs 17276	Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐵))
Theorem	wunress 17277	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 17278	Obsolete proof of wunress 17277 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 𝐴) ∈ 𝑈)
7.1.2  Slot definitions
Syntax	cplusg 17279	Extend class notation with group (addition) operation.
class +g
Syntax	cmulr 17280	Extend class notation with ring multiplication.
class .r
Syntax	cstv 17281	Extend class notation with involution.
class *𝑟
Syntax	csca 17282	Extend class notation with scalar field.
class Scalar
Syntax	cvsca 17283	Extend class notation with scalar product.
class ·𝑠
Syntax	cip 17284	Extend class notation with Hermitian form (inner product).
class ·𝑖
Syntax	cts 17285	Extend class notation with the topology component of a topological space.
class TopSet
Syntax	cple 17286	Extend class notation with "less than or equal to" for posets.
class le
Syntax	coc 17287	Extend class notation with the class of orthocomplementation extractors.
class oc
Syntax	cds 17288	Extend class notation with the metric space distance function.
class dist
Syntax	cunif 17289	Extend class notation with the uniform structure.
class UnifSet
Syntax	chom 17290	Extend class notation with the hom-set structure.
class Hom
Syntax	cco 17291	Extend class notation with the composition operation.
class comp
Definition	df-plusg 17292	Define group operation. In the context of less restrictive structures, this operation is also called magma, semigroup or monoid operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form plusgid 17306 instead. (New usage is discouraged.)
⊢ +g = Slot 2
Definition	df-mulr 17293	Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form mulrid 11263 instead. (New usage is discouraged.)
⊢ .r = Slot 3
Definition	df-starv 17294	Define the involution function of a *-ring. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form starvid 17330 instead. (New usage is discouraged.)
⊢ *𝑟 = Slot 4
Definition	df-sca 17295	Define scalar field component of a vector space 𝑣. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form scaid 17342 instead. (New usage is discouraged.)
⊢ Scalar = Slot 5
Definition	df-vsca 17296	Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form vscaid 17347 instead. (New usage is discouraged.)
⊢ ·𝑠 = Slot 6
Definition	df-ip 17297	Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form ipid 17358 instead. (New usage is discouraged.)
⊢ ·𝑖 = Slot 8
Definition	df-tset 17298	Define the topology component of a topological space (structure). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form tsetid 17380 instead. (New usage is discouraged.)
⊢ TopSet = Slot 9
Definition	df-ple 17299	Define "less than or equal to" ordering extractor for posets and related structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) Use its index-independent form pleid 17394 instead. (New usage is discouraged.)
⊢ le = Slot ;10
Definition	df-ocomp 17300	Define the orthocomplementation extractor for posets and related structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form ocid 17409 instead. (New usage is discouraged.)
⊢ oc = Slot ;11