P. 133 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13201-13300   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cbs 13201	Extend class notation with the class of all base set extractors.
class Base
Syntax	cress 13202	Extend class notation with the extensible structure builder restriction operator.
class ↾s
Definition	df-struct 13203*	Define a structure with components in 𝑀...𝑁. This is not a requirement for groups, posets, etc., but it is a useful assumption for component extraction theorems. As mentioned in the section header, an "extensible structure should be implemented as a function (a set of ordered pairs)". The current definition, however, is less restrictive: it allows for classes which contain the empty set ∅ to be extensible structures. Because of 0nelfun 5369, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 13214: 𝐹 Struct 𝑋 → Fun (𝐹 ∖ {∅}). Allowing an extensible structure to contain the empty set ensures that expressions like {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} are structures without asserting or implying that 𝐴, 𝐵, 𝐶 and 𝐷 are sets (if 𝐴 or 𝐵 is a proper class, then ⟨𝐴, 𝐵⟩ = ∅, see opprc 3903). (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}
Definition	df-ndx 13204	Define the structure component index extractor. See Theorem ndxarg 13224 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 13207) another set such as the set of finite ordinals ω (df-iom 4712). (Contributed by NM, 4-Sep-2011.)
⊢ ndx = ( I ↾ ℕ)
Definition	df-slot 13205*	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 or a group). Note that Slot 𝐴 is implemented as "evaluation at 𝐴". That is, (Slot 𝐴‘𝑆) is defined to be (𝑆‘𝐴), where 𝐴 will typically be a small nonzero natural number. Each extensible structure 𝑆 is a function defined on specific natural number "slots", and this function extracts the value at a particular slot. 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 13224). 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 value 1). 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 5689). 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 13206	Equality theorem for the Slot construction. The converse holds if 𝐴 (or 𝐵) is a set. (Contributed by BJ, 27-Dec-2021.)
⊢ (𝐴 = 𝐵 → Slot 𝐴 = Slot 𝐵)
Definition	df-base 13207	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.)
⊢ Base = Slot 1
Definition	df-sets 13208*	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-iress 13209 adjusts the base set to match its second argument, which has the effect of making subgroups, subspaces, subrings etc. from the original structures. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ sSet = (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒}))
Definition	df-iress 13209*	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, defining a function using the base set and applying that, or explicitly truncating the slot before use. (Credit for this operator, as well as the 2023 modification for iset.mm, goes to Mario Carneiro.) (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 7-Oct-2023.)
⊢ ↾s = (𝑤 ∈ V, 𝑥 ∈ V ↦ (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩))
Theorem	brstruct 13210	The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ Rel Struct
Theorem	isstruct2im 13211	The property of being a structure with components in (1st ‘𝑋)...(2nd ‘𝑋). (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
⊢ (𝐹 Struct 𝑋 → (𝑋 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)))
Theorem	isstruct2r 13212	The property of being a structure with components in (1st ‘𝑋)...(2nd ‘𝑋). (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
⊢ (((𝑋 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝐹 ∖ {∅})) ∧ (𝐹 ∈ 𝑉 ∧ dom 𝐹 ⊆ (...‘𝑋))) → 𝐹 Struct 𝑋)
Theorem	structex 13213	A structure is a set. (Contributed by AV, 10-Nov-2021.)
⊢ (𝐺 Struct 𝑋 → 𝐺 ∈ V)
Theorem	structn0fun 13214	A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021.)
⊢ (𝐹 Struct 𝑋 → Fun (𝐹 ∖ {∅}))
Theorem	isstructim 13215	The property of being a structure with components in 𝑀...𝑁. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
⊢ (𝐹 Struct ⟨𝑀, 𝑁⟩ → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (𝑀...𝑁)))
Theorem	isstructr 13216	The property of being a structure with components in 𝑀...𝑁. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ (Fun (𝐹 ∖ {∅}) ∧ 𝐹 ∈ 𝑉 ∧ dom 𝐹 ⊆ (𝑀...𝑁))) → 𝐹 Struct ⟨𝑀, 𝑁⟩)
Theorem	structcnvcnv 13217	Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ (𝐹 Struct 𝑋 → ◡◡𝐹 = (𝐹 ∖ {∅}))
Theorem	structfung 13218	The converse of the converse of a structure is a function. Closed form of structfun 13219. (Contributed by AV, 12-Nov-2021.)
⊢ (𝐹 Struct 𝑋 → Fun ◡◡𝐹)
Theorem	structfun 13219	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 13220	Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐹 Struct ⟨𝑀, 𝑁⟩    ⇒   ⊢ (Fun ◡◡𝐹 ∧ dom 𝐹 ⊆ (1...𝑁))
Theorem	strnfvnd 13221	Deduction version of strnfvn 13222. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 19-Jan-2023.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐸‘𝑆) = (𝑆‘𝑁))
Theorem	strnfvn 13222	Value of a structure component extractor 𝐸. Normally, 𝐸 is a defined constant symbol such as Base (df-base 13207) and 𝑁 is a fixed integer such as 1. 𝑆 is a structure, i.e. a specific member of a class of structures. Note: Normally, this theorem shouldn't be used outside of this section, because it requires hard-coded index values. Instead, use strslfv 13246. (Contributed by NM, 9-Sep-2011.) (Revised by Jim Kingdon, 19-Jan-2023.) (New usage is discouraged.)
⊢ 𝑆 ∈ V    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝐸‘𝑆) = (𝑆‘𝑁)
Theorem	strfvssn 13223	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.) (Revised by Jim Kingdon, 19-Jan-2023.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐸‘𝑆) ⊆ ∪ ran 𝑆)
Theorem	ndxarg 13224	Get the numeric argument from a defined structure component extractor such as df-base 13207. (Contributed by Mario Carneiro, 6-Oct-2013.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝐸‘ndx) = 𝑁
Theorem	ndxid 13225	A structure component extractor is defined by its own index. This theorem, together with strslfv 13246 below, is useful for avoiding direct reference to the hard-coded numeric index in component extractor definitions, such as the 1 in df-base 13207, making it easier to change should the need arise. (Contributed by NM, 19-Oct-2012.) (Revised by Mario Carneiro, 6-Oct-2013.) (Proof shortened by BJ, 27-Dec-2021.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ 𝐸 = Slot (𝐸‘ndx)
Theorem	ndxslid 13226	A structure component extractor is defined by its own index. That the index is a natural number will also be needed in quite a few contexts so it is included in the conclusion of this theorem which can be used as a hypothesis of theorems like strslfv 13246. (Contributed by Jim Kingdon, 29-Jan-2023.)
⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)
Theorem	slotslfn 13227	A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by Jim Kingdon, 10-Feb-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    ⇒   ⊢ 𝐸 Fn V
Theorem	slotex 13228	Existence of slot value. A corollary of slotslfn 13227. (Contributed by Jim Kingdon, 12-Feb-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐸‘𝐴) ∈ V)
Theorem	strndxid 13229	The value of a structure component extractor is the value of the corresponding slot of the structure. (Contributed by AV, 13-Mar-2020.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ 𝐸 = Slot 𝑁    &   ⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝜑 → (𝑆‘(𝐸‘ndx)) = (𝐸‘𝑆))
Theorem	reldmsets 13230	The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.)
⊢ Rel dom sSet
Theorem	setsvalg 13231	Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑆 sSet 𝐴) = ((𝑆 ↾ (V ∖ dom {𝐴})) ∪ {𝐴}))
Theorem	setsvala 13232	Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 20-Jan-2023.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑊) → (𝑆 sSet ⟨𝐴, 𝐵⟩) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {⟨𝐴, 𝐵⟩}))
Theorem	setsex 13233	Applying the structure replacement function yields a set. (Contributed by Jim Kingdon, 22-Jan-2023.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑊) → (𝑆 sSet ⟨𝐴, 𝐵⟩) ∈ V)
Theorem	strsetsid 13234	Value of the structure replacement function. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 30-Jan-2023.)
⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝜑 → 𝑆 Struct ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → Fun 𝑆)    &   ⊢ (𝜑 → (𝐸‘ndx) ∈ dom 𝑆)    ⇒   ⊢ (𝜑 → 𝑆 = (𝑆 sSet ⟨(𝐸‘ndx), (𝐸‘𝑆)⟩))
Theorem	fvsetsid 13235	The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈) → ((𝐹 sSet ⟨𝑋, 𝑌⟩)‘𝑋) = 𝑌)
Theorem	setsfun 13236	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 13237	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 13236 is useful for proofs based on isstruct2r 13212 which requires Fun (𝐹 ∖ {∅}) for 𝐹 to be an extensible structure. (Contributed by AV, 7-Jun-2021.)
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun ((𝐺 sSet ⟨𝐼, 𝐸⟩) ∖ {∅}))
Theorem	setsn0fun 13238	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	setsresg 13239	The structure replacement function does not affect the value of 𝑆 away from 𝐴. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 22-Jan-2023.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ((𝑆 sSet ⟨𝐴, 𝐵⟩) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴})))
Theorem	setsabsd 13240	Replacing the same components twice yields the same as the second setting only. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Jim Kingdon, 22-Jan-2023.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ((𝑆 sSet ⟨𝐴, 𝐵⟩) sSet ⟨𝐴, 𝐶⟩) = (𝑆 sSet ⟨𝐴, 𝐶⟩))
Theorem	setscom 13241	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 ⟨𝐴, 𝐶⟩))
Theorem	setscomd 13242	Different components can be set in any order. (Contributed by Jim Kingdon, 20-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝐵, 𝐷⟩) = ((𝑆 sSet ⟨𝐵, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩))
Theorem	strslfvd 13243	Deduction version of strslfv 13246. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 30-Jan-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝑆)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆))
Theorem	strslfv2d 13244	Deduction version of strslfv 13246. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → Fun ◡◡𝑆)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆))
Theorem	strslfv2 13245	A variation on strslfv 13246 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.) (Revised by Jim Kingdon, 30-Jan-2023.)
⊢ 𝑆 ∈ V    &   ⊢ Fun ◡◡𝑆    &   ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆    ⇒   ⊢ (𝐶 ∈ 𝑉 → 𝐶 = (𝐸‘𝑆))
Theorem	strslfv 13246	Extract a structure component 𝐶 (such as the base set) from a structure 𝑆 with a component extractor 𝐸 (such as the base set extractor df-base 13207). By virtue of ndxslid 13226, this can be done without having to refer to the hard-coded numeric index of 𝐸. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Jim Kingdon, 30-Jan-2023.)
⊢ 𝑆 Struct 𝑋    &   ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ {⟨(𝐸‘ndx), 𝐶⟩} ⊆ 𝑆    ⇒   ⊢ (𝐶 ∈ 𝑉 → 𝐶 = (𝐸‘𝑆))
Theorem	strslfv3 13247	Variant on strslfv 13246 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.) (Revised by Jim Kingdon, 30-Jan-2023.)
⊢ (𝜑 → 𝑈 = 𝑆)    &   ⊢ (𝜑 → 𝑆 Struct 𝑋)    &   ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ (𝜑 → {⟨(𝐸‘ndx), 𝐶⟩} ⊆ 𝑆)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ 𝐴 = (𝐸‘𝑈)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐶)
Theorem	strslssd 13248	Deduction version of strslss 13249. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 31-Jan-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝑇)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑇)    &   ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝐸‘𝑇) = (𝐸‘𝑆))
Theorem	strslss 13249	Propagate component extraction to a structure 𝑇 from a subset structure 𝑆. (Contributed by Mario Carneiro, 11-Oct-2013.) (Revised by Jim Kingdon, 31-Jan-2023.)
⊢ 𝑇 ∈ V    &   ⊢ Fun 𝑇    &   ⊢ 𝑆 ⊆ 𝑇    &   ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆    ⇒   ⊢ (𝐸‘𝑇) = (𝐸‘𝑆)
Theorem	strsl0 13250	All components of the empty set are empty sets. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 31-Jan-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    ⇒   ⊢ ∅ = (𝐸‘∅)
Theorem	base0 13251	The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ ∅ = (Base‘∅)
Theorem	setsslid 13252	Value of the structure replacement function at a replaced index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    ⇒   ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 = (𝐸‘(𝑊 sSet ⟨(𝐸‘ndx), 𝐶⟩)))
Theorem	setsslnid 13253	Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.)
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    &   ⊢ (𝐸‘ndx) ≠ 𝐷    &   ⊢ 𝐷 ∈ ℕ    ⇒   ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩)))
Theorem	baseval 13254	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 13255	Utility theorem: index-independent form of df-base 13207. (Contributed by NM, 20-Oct-2012.)
⊢ Base = Slot (Base‘ndx)
Theorem	basendx 13256	Index value of the base set extractor. Use of this theorem is discouraged since the particular value 1 for the index is an implementation detail. It is generally sufficient to work with (Base‘ndx) and use theorems such as baseid 13255 and basendxnn 13257. The main circumstance in which it is necessary to look at indices directly is when showing that a set of indices are disjoint, in proofs such as lmodstrd 13366. Although we have a few theorems such as basendxnplusgndx 13327, we do not intend to add such theorems for every pair of indices (which would be quadradically many in the number of indices). (New usage is discouraged.) (Contributed by Mario Carneiro, 2-Aug-2013.)
⊢ (Base‘ndx) = 1
Theorem	basendxnn 13257	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.)
⊢ (Base‘ndx) ∈ ℕ
Theorem	bassetsnn 13258	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	baseslid 13259	The base set extractor is a slot. (Contributed by Jim Kingdon, 31-Jan-2023.)
⊢ (Base = Slot (Base‘ndx) ∧ (Base‘ndx) ∈ ℕ)
Theorem	basfn 13260	The base set extractor is a function on V. (Contributed by Stefan O'Rear, 8-Jul-2015.)
⊢ Base Fn V
Theorem	basmex 13261	A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝐵 → 𝐺 ∈ V)
Theorem	basmexd 13262	A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 28-Nov-2024.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐺 ∈ V)
Theorem	basm 13263*	A structure whose base is inhabited is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝐵 → ∃𝑗 𝑗 ∈ 𝐺)
Theorem	relelbasov 13264	Utility theorem: reverse closure for any structure defined as a two-argument function. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ Rel dom 𝑂    &   ⊢ Rel 𝑂    &   ⊢ 𝑆 = (𝑋𝑂𝑌)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝐴 ∈ 𝐵 → (𝑋 ∈ V ∧ 𝑌 ∈ V))
Theorem	reldmress 13265	The structure restriction is a proper operator, so it can be used with ovprc1 6086. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ Rel dom ↾s
Theorem	ressvalsets 13266	Value of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.)
⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → (𝑊 ↾s 𝐴) = (𝑊 sSet ⟨(Base‘ndx), (𝐴 ∩ (Base‘𝑊))⟩))
Theorem	ressex 13267	Existence of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.)
⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → (𝑊 ↾s 𝐴) ∈ V)
Theorem	ressval2 13268	Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
⊢ 𝑅 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Base‘ndx), (𝐴 ∩ 𝐵)⟩))
Theorem	ressbasd 13269	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	ressbas2d 13270	Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ (𝜑 → 𝑅 = (𝑊 ↾s 𝐴))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = (Base‘𝑅))
Theorem	ressbasssd 13271	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.)
⊢ (𝜑 → 𝑅 = (𝑊 ↾s 𝐴))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Base‘𝑅) ⊆ 𝐵)
Theorem	ressbasid 13272	The trivial structure restriction leaves the base set unchanged. (Contributed by Jim Kingdon, 29-Apr-2025.)
⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑉 → (Base‘(𝑊 ↾s 𝐵)) = 𝐵)
Theorem	strressid 13273	Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 17-Jan-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝑊))    &   ⊢ (𝜑 → 𝑊 Struct ⟨𝑀, 𝑁⟩)    &   ⊢ (𝜑 → Fun 𝑊)    &   ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝑊)    ⇒   ⊢ (𝜑 → (𝑊 ↾s 𝐵) = 𝑊)
Theorem	ressval3d 13274	Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 17-Jan-2025.)
⊢ 𝑅 = (𝑆 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐸 = (Base‘ndx)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝑆)    &   ⊢ (𝜑 → 𝐸 ∈ dom 𝑆)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → 𝑅 = (𝑆 sSet ⟨𝐸, 𝐴⟩))
Theorem	resseqnbasd 13275	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) ∈ ℕ)    &   ⊢ (𝐸‘ndx) ≠ (Base‘ndx)    &   ⊢ (𝜑 → 𝑊 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐸‘𝑅))
Theorem	ressinbasd 13276	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	ressressg 13277	Restriction composition law. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Proof shortened by Mario Carneiro, 2-Dec-2014.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑊 ∈ 𝑍) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵)))
Theorem	ressabsg 13278	Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐵))
6.1.2  Slot definitions
Syntax	cplusg 13279	Extend class notation with group (addition) operation.
class +g
Syntax	cmulr 13280	Extend class notation with ring multiplication.
class .r
Syntax	cstv 13281	Extend class notation with involution.
class *𝑟
Syntax	csca 13282	Extend class notation with scalar field.
class Scalar
Syntax	cvsca 13283	Extend class notation with scalar product.
class ·𝑠
Syntax	cip 13284	Extend class notation with Hermitian form (inner product).
class ·𝑖
Syntax	cts 13285	Extend class notation with the topology component of a topological space.
class TopSet
Syntax	cple 13286	Extend class notation with "less than or equal to" for posets.
class le
Syntax	coc 13287	Extend class notation with the class of orthocomplementation extractors.
class oc
Syntax	cds 13288	Extend class notation with the metric space distance function.
class dist
Syntax	cunif 13289	Extend class notation with the uniform structure.
class UnifSet
Syntax	chom 13290	Extend class notation with the hom-set structure.
class Hom
Syntax	cco 13291	Extend class notation with the composition operation.
class comp
Definition	df-plusg 13292	Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ +g = Slot 2
Definition	df-mulr 13293	Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ .r = Slot 3
Definition	df-starv 13294	Define the involution function of a *-ring. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ *𝑟 = Slot 4
Definition	df-sca 13295	Define scalar field component of a vector space 𝑣. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ Scalar = Slot 5
Definition	df-vsca 13296	Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ ·𝑠 = Slot 6
Definition	df-ip 13297	Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ ·𝑖 = Slot 8
Definition	df-tset 13298	Define the topology component of a topological space (structure). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ TopSet = Slot 9
Definition	df-ple 13299	Define "less than or equal to" ordering extractor for posets and related structures. We use ;10 for the index to avoid conflict with 1 through 9 used for other purposes. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
⊢ le = Slot ;10
Definition	df-ocomp 13300	Define the orthocomplementation extractor for posets and related structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ oc = Slot ;11