P. 131 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13001-13100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ctiunctlemu2nd 13001*	Lemma for ctiunct 13006. (Contributed by Jim Kingdon, 28-Oct-2023.)
|- ( ph -> S C_ om )   &    |- ( ph -> A. n e. om DECID n e. S )   &    |- ( ph -> F : S -onto-> A )   &    |- ( ( ph /\ x e. A ) -> T C_ om )   &    |- ( ( ph /\ x e. A ) -> A. n e. om DECID n e. T )   &    |- ( ( ph /\ x e. A ) -> G : T -onto-> B )   &    |- ( ph -> J : om -1-1-onto-> ( om X. om ) )   &    |- U = { z e. om | ( ( 1st ` ( J ` z ) ) e. S /\ ( 2nd ` ( J ` z ) ) e. [_ ( F ` ( 1st ` ( J ` z ) ) ) / x ]_ T ) }   &    |- ( ph -> N e. U )   =>    |- ( ph -> ( 2nd ` ( J ` N ) ) e. [_ ( F ` ( 1st ` ( J ` N ) ) ) / x ]_ T )
Theorem	ctiunctlemuom 13002	Lemma for ctiunct 13006. (Contributed by Jim Kingdon, 28-Oct-2023.)
|- ( ph -> S C_ om )   &    |- ( ph -> A. n e. om DECID n e. S )   &    |- ( ph -> F : S -onto-> A )   &    |- ( ( ph /\ x e. A ) -> T C_ om )   &    |- ( ( ph /\ x e. A ) -> A. n e. om DECID n e. T )   &    |- ( ( ph /\ x e. A ) -> G : T -onto-> B )   &    |- ( ph -> J : om -1-1-onto-> ( om X. om ) )   &    |- U = { z e. om | ( ( 1st ` ( J ` z ) ) e. S /\ ( 2nd ` ( J ` z ) ) e. [_ ( F ` ( 1st ` ( J ` z ) ) ) / x ]_ T ) }   =>    |- ( ph -> U C_ om )
Theorem	ctiunctlemudc 13003*	Lemma for ctiunct 13006. (Contributed by Jim Kingdon, 28-Oct-2023.)
|- ( ph -> S C_ om )   &    |- ( ph -> A. n e. om DECID n e. S )   &    |- ( ph -> F : S -onto-> A )   &    |- ( ( ph /\ x e. A ) -> T C_ om )   &    |- ( ( ph /\ x e. A ) -> A. n e. om DECID n e. T )   &    |- ( ( ph /\ x e. A ) -> G : T -onto-> B )   &    |- ( ph -> J : om -1-1-onto-> ( om X. om ) )   &    |- U = { z e. om | ( ( 1st ` ( J ` z ) ) e. S /\ ( 2nd ` ( J ` z ) ) e. [_ ( F ` ( 1st ` ( J ` z ) ) ) / x ]_ T ) }   =>    |- ( ph -> A. n e. om DECID n e. U )
Theorem	ctiunctlemf 13004*	Lemma for ctiunct 13006. (Contributed by Jim Kingdon, 28-Oct-2023.)
|- ( ph -> S C_ om )   &    |- ( ph -> A. n e. om DECID n e. S )   &    |- ( ph -> F : S -onto-> A )   &    |- ( ( ph /\ x e. A ) -> T C_ om )   &    |- ( ( ph /\ x e. A ) -> A. n e. om DECID n e. T )   &    |- ( ( ph /\ x e. A ) -> G : T -onto-> B )   &    |- ( ph -> J : om -1-1-onto-> ( om X. om ) )   &    |- U = { z e. om | ( ( 1st ` ( J ` z ) ) e. S /\ ( 2nd ` ( J ` z ) ) e. [_ ( F ` ( 1st ` ( J ` z ) ) ) / x ]_ T ) }   &    |- H = ( n e. U |-> ( [_ ( F ` ( 1st ` ( J ` n ) ) ) / x ]_ G ` ( 2nd ` ( J ` n ) ) ) )   =>    |- ( ph -> H : U --> U_ x e. A B )
Theorem	ctiunctlemfo 13005*	Lemma for ctiunct 13006. (Contributed by Jim Kingdon, 28-Oct-2023.)
|- ( ph -> S C_ om )   &    |- ( ph -> A. n e. om DECID n e. S )   &    |- ( ph -> F : S -onto-> A )   &    |- ( ( ph /\ x e. A ) -> T C_ om )   &    |- ( ( ph /\ x e. A ) -> A. n e. om DECID n e. T )   &    |- ( ( ph /\ x e. A ) -> G : T -onto-> B )   &    |- ( ph -> J : om -1-1-onto-> ( om X. om ) )   &    |- U = { z e. om | ( ( 1st ` ( J ` z ) ) e. S /\ ( 2nd ` ( J ` z ) ) e. [_ ( F ` ( 1st ` ( J ` z ) ) ) / x ]_ T ) }   &    |- H = ( n e. U |-> ( [_ ( F ` ( 1st ` ( J ` n ) ) ) / x ]_ G ` ( 2nd ` ( J ` n ) ) ) )   &    |- F/_ x H   &    |- F/_ x U   =>    |- ( ph -> H : U -onto-> U_ x e. A B )
Theorem	ctiunct 13006*	A sequence of enumerations gives an enumeration of the union. We refer to "sequence of enumerations" rather than "countably many countable sets" because the hypothesis provides more than countability for each B ( x ): it refers to B ( x ) together with the G ( x ) which enumerates it. Theorem 8.1.19 of [AczelRathjen], p. 74. For "countably many countable sets" the key hypothesis would be ( ph /\ x e. A ) -> E. g g : om -onto-> ( B ⊔ 1o ). This is almost omiunct 13010 (which uses countable choice) although that is for a countably infinite collection not any countable collection. Compare with the case of two sets instead of countably many, as seen at unct 13008, which says that the union of two countable sets is countable . The proof proceeds by mapping a natural number to a pair of natural numbers (by xpomen 12961) and using the first number to map to an element x of A and the second number to map to an element of B(x) . In this way we are able to map to every element of U_ x e. A B. Although it would be possible to work directly with countability expressed as F : om -onto-> ( A ⊔ 1o ), we instead use functions from subsets of the natural numbers via ctssdccl 7274 and ctssdc 7276. (Contributed by Jim Kingdon, 31-Oct-2023.)
|- ( ph -> F : om -onto-> ( A ⊔ 1o ) )   &    |- ( ( ph /\ x e. A ) -> G : om -onto-> ( B ⊔ 1o ) )   =>    |- ( ph -> E. h h : om -onto-> ( U_ x e. A B ⊔ 1o ) )
Theorem	ctiunctal 13007*	Variation of ctiunct 13006 which allows x to be present in ph. (Contributed by Jim Kingdon, 5-May-2024.)
|- ( ph -> F : om -onto-> ( A ⊔ 1o ) )   &    |- ( ph -> A. x e. A G : om -onto-> ( B ⊔ 1o ) )   =>    |- ( ph -> E. h h : om -onto-> ( U_ x e. A B ⊔ 1o ) )
Theorem	unct 13008*	The union of two countable sets is countable. Corollary 8.1.20 of [AczelRathjen], p. 75. (Contributed by Jim Kingdon, 1-Nov-2023.)
|- ( ( E. f f : om -onto-> ( A ⊔ 1o ) /\ E. g g : om -onto-> ( B ⊔ 1o ) ) -> E. h h : om -onto-> ( ( A u. B ) ⊔ 1o ) )
Theorem	omctfn 13009*	Using countable choice to find a sequence of enumerations for a collection of countable sets. Lemma 8.1.27 of [AczelRathjen], p. 77. (Contributed by Jim Kingdon, 19-Apr-2024.)
|- ( ph -> CCHOICE )   &    |- ( ( ph /\ x e. om ) -> E. g g : om -onto-> ( B ⊔ 1o ) )   =>    |- ( ph -> E. f ( f Fn om /\ A. x e. om ( f ` x ) : om -onto-> ( B ⊔ 1o ) ) )
Theorem	omiunct 13010*	The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 13006 which has a stronger hypothesis but does not require countable choice. (Contributed by Jim Kingdon, 5-May-2024.)
|- ( ph -> CCHOICE )   &    |- ( ( ph /\ x e. om ) -> E. g g : om -onto-> ( B ⊔ 1o ) )   =>    |- ( ph -> E. h h : om -onto-> ( U_ x e. om B ⊔ 1o ) )
Theorem	ssomct 13011*	A decidable subset of om is countable. (Contributed by Jim Kingdon, 19-Sep-2024.)
|- ( ( A C_ om /\ A. x e. om DECID x e. A ) -> E. f f : om -onto-> ( A ⊔ 1o ) )
Theorem	ssnnctlemct 13012*	Lemma for ssnnct 13013. The result. (Contributed by Jim Kingdon, 29-Sep-2024.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 1 )   =>    |- ( ( A C_ NN /\ A. x e. NN DECID x e. A ) -> E. f f : om -onto-> ( A ⊔ 1o ) )
Theorem	ssnnct 13013*	A decidable subset of NN is countable. (Contributed by Jim Kingdon, 29-Sep-2024.)
|- ( ( A C_ NN /\ A. x e. NN DECID x e. A ) -> E. f f : om -onto-> ( A ⊔ 1o ) )
Theorem	nninfdclemcl 13014*	Lemma for nninfdc 13019. (Contributed by Jim Kingdon, 25-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> A. m e. NN E. n e. A m < n )   &    |- ( ph -> P e. A )   &    |- ( ph -> Q e. A )   =>    |- ( ph -> ( P ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) Q ) e. A )
Theorem	nninfdclemf 13015*	Lemma for nninfdc 13019. A function from the natural numbers into A. (Contributed by Jim Kingdon, 23-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> A. m e. NN E. n e. A m < n )   &    |- ( ph -> ( J e. A /\ 1 < J ) )   &    |- F = seq 1 ( ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) , ( i e. NN |-> J ) )   =>    |- ( ph -> F : NN --> A )
Theorem	nninfdclemp1 13016*	Lemma for nninfdc 13019. Each element of the sequence F is greater than the previous element. (Contributed by Jim Kingdon, 26-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> A. m e. NN E. n e. A m < n )   &    |- ( ph -> ( J e. A /\ 1 < J ) )   &    |- F = seq 1 ( ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) , ( i e. NN |-> J ) )   &    |- ( ph -> U e. NN )   =>    |- ( ph -> ( F ` U ) < ( F ` ( U + 1 ) ) )
Theorem	nninfdclemlt 13017*	Lemma for nninfdc 13019. The function from nninfdclemf 13015 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> A. m e. NN E. n e. A m < n )   &    |- ( ph -> ( J e. A /\ 1 < J ) )   &    |- F = seq 1 ( ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) , ( i e. NN |-> J ) )   &    |- ( ph -> U e. NN )   &    |- ( ph -> V e. NN )   &    |- ( ph -> U < V )   =>    |- ( ph -> ( F ` U ) < ( F ` V ) )
Theorem	nninfdclemf1 13018*	Lemma for nninfdc 13019. The function from nninfdclemf 13015 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.)
|- ( ph -> A C_ NN )   &    |- ( ph -> A. x e. NN DECID x e. A )   &    |- ( ph -> A. m e. NN E. n e. A m < n )   &    |- ( ph -> ( J e. A /\ 1 < J ) )   &    |- F = seq 1 ( ( y e. NN , z e. NN |-> inf ( ( A i^i ( ZZ>= ` ( y + 1 ) ) ) , RR , < ) ) , ( i e. NN |-> J ) )   =>    |- ( ph -> F : NN -1-1-> A )
Theorem	nninfdc 13019*	An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.)
|- ( ( A C_ NN /\ A. x e. NN DECID x e. A /\ A. m e. NN E. n e. A m < n ) -> om ~<_ A )
Theorem	unbendc 13020*	An unbounded decidable set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Jim Kingdon, 30-Sep-2024.)
|- ( ( A C_ NN /\ A. x e. NN DECID x e. A /\ A. m e. NN E. n e. A m < n ) -> A ~~ NN )
Theorem	prminf 13021	There are an infinite number of primes. Theorem 1.7 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 28-Nov-2012.)
|- Prime ~~ NN
Theorem	infpn2 13022*	There exist infinitely many prime numbers: the set of all primes S is unbounded by infpn 12879, so by unbendc 13020 it is infinite. This is Metamath 100 proof #11. (Contributed by NM, 5-May-2005.)
|- S = { n e. NN | ( 1 < n /\ A. m e. NN ( ( n / m ) e. NN -> ( m = 1 \/ m = n ) ) ) }   =>    |- S ~~ NN
PART 6  BASIC STRUCTURES
6.1  Extensible structures
6.1.1  Basic definitions An "extensible structure" (or "structure" in short, at least in this section) is used to define a specific group, ring, poset, and so on. An extensible structure can contain many components. For example, a group will have at least two components (base set and operation), although it can be further specialized by adding other components such as a multiplicative operation for rings (and still remain a group per our definition). Thus, every ring is also a group. This extensible structure approach allows theorems from more general structures (such as groups) to be reused for more specialized structures (such as rings) without having to reprove anything. Structures are common in mathematics, but in informal (natural language) proofs the details are assumed in ways that we must make explicit. An extensible structure is implemented as a function (a set of ordered pairs) on a finite (and not necessarily sequential) subset of NN. The function's argument is the index of a structure component (such as 1 for the base set of a group), and its value is the component (such as the base set). By convention, we normally avoid direct reference to the hard-coded numeric index and instead use structure component extractors such as ndxid 13051 and strslfv 13072. Using extractors makes it easier to change numeric indices and also makes the components' purpose clearer. See the comment of basendx 13082 for more details on numeric indices versus the structure component extractors. There are many other possible ways to handle structures. We chose this extensible structure approach because this approach (1) results in simpler notation than other approaches we are aware of, and (2) is easier to do proofs with. We cannot use an approach that uses "hidden" arguments; Metamath does not support hidden arguments, and in any case we want nothing hidden. It would be possible to use a categorical approach (e.g., something vaguely similar to Lean's mathlib). However, instances (the chain of proofs that an X is a Y via a bunch of forgetful functors) can cause serious performance problems for automated tooling, and the resulting proofs would be painful to look at directly (in the case of Lean, they are long past the level where people would find it acceptable to look at them directly). Metamath is working under much stricter conditions than this, and it has still managed to achieve about the same level of flexibility through this "extensible structure" approach. To create a substructure of a given extensible structure, you can simply use the multifunction restriction operator for extensible structures ↾s as defined in df-iress 13035. This 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. Extensible structures only work well when they represent concrete categories, where there is a "base set", morphisms are functions, and subobjects are subsets with induced operations. In short, they primarily work well for "sets with (some) extra structure". Extensible structures may not suffice for more complicated situations. For example, in manifolds, ↾s would not work. That said, extensible structures are sufficient for many of the structures that set.mm currently considers, and offer a good compromise for a goal-oriented formalization.
Syntax	cstr 13023	Extend class notation with the class of structures with components numbered below A.
class Struct
Syntax	cnx 13024	Extend class notation with the structure component index extractor.
class ndx
Syntax	csts 13025	Set components of a structure.
class sSet
Syntax	cslot 13026	Extend class notation with the slot function.
class Slot A
Syntax	cbs 13027	Extend class notation with the class of all base set extractors.
class Base
Syntax	cress 13028	Extend class notation with the extensible structure builder restriction operator.
class ↾s
Definition	df-struct 13029*	Define a structure with components in M ... N. 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 5335, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 13040: F Struct X -> Fun ( F \ { (/) } ). Allowing an extensible structure to contain the empty set ensures that expressions like { <. A , B >. , <. C , D >. } are structures without asserting or implying that A, B, C and D are sets (if A or B is a proper class, then <. A , B >. = (/), see opprc 3877). (Contributed by Mario Carneiro, 29-Aug-2015.)
|- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) }
Definition	df-ndx 13030	Define the structure component index extractor. See Theorem ndxarg 13050 to understand its purpose. The restriction to NN 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 CC or (if we revise all structure component definitions such as df-base 13033) another set such as the set of finite ordinals om (df-iom 4682). (Contributed by NM, 4-Sep-2011.)
|- ndx = ( _I |` NN )
Definition	df-slot 13031*	Define the slot extractor for extensible structures. The class Slot A 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 A is implemented as "evaluation at A". That is, (Slot A ` S ) is defined to be ( S ` A ), where A will typically be a small nonzero natural number. Each extensible structure S 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 NN, can be used to extract the number A from a slot, since (Slot A ` ndx ) = A (see ndxarg 13050). 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 ( x e. _V |-> ( f e. _V |-> ( f ` x ) ) ) because each Slot A is a function on the proper class _V so is itself a proper class, and the values of functions are sets (fvex 5646). It is necessary to allow proper classes as values of Slot A since for instance the class of all (base sets of) groups is proper. (Contributed by Mario Carneiro, 22-Sep-2015.)
|- Slot A = ( x e. _V |-> ( x ` A ) )
Theorem	sloteq 13032	Equality theorem for the Slot construction. The converse holds if A (or B) is a set. (Contributed by BJ, 27-Dec-2021.)
|- ( A = B -> Slot A = Slot B )
Definition	df-base 13033	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 13034*	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 13035 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 = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
Definition	df-iress 13035*	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 = ( w e. _V , x e. _V |-> ( w sSet <. ( Base ` ndx ) , ( x i^i ( Base ` w ) ) >. ) )
Theorem	brstruct 13036	The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- Rel Struct
Theorem	isstruct2im 13037	The property of being a structure with components in ( 1st ` X ) ... ( 2nd ` X ). (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
|- ( F Struct X -> ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) )
Theorem	isstruct2r 13038	The property of being a structure with components in ( 1st ` X ) ... ( 2nd ` X ). (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
|- ( ( ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) ) /\ ( F e. V /\ dom F C_ ( ... ` X ) ) ) -> F Struct X )
Theorem	structex 13039	A structure is a set. (Contributed by AV, 10-Nov-2021.)
|- ( G Struct X -> G e. _V )
Theorem	structn0fun 13040	A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021.)
|- ( F Struct X -> Fun ( F \ { (/) } ) )
Theorem	isstructim 13041	The property of being a structure with components in M ... N. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
|- ( F Struct <. M , N >. -> ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( M ... N ) ) )
Theorem	isstructr 13042	The property of being a structure with components in M ... N. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
|- ( ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ ( Fun ( F \ { (/) } ) /\ F e. V /\ dom F C_ ( M ... N ) ) ) -> F Struct <. M , N >. )
Theorem	structcnvcnv 13043	Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- ( F Struct X -> `' `' F = ( F \ { (/) } ) )
Theorem	structfung 13044	The converse of the converse of a structure is a function. Closed form of structfun 13045. (Contributed by AV, 12-Nov-2021.)
|- ( F Struct X -> Fun `' `' F )
Theorem	structfun 13045	Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Proof shortened by AV, 12-Nov-2021.)
|- F Struct X   =>    |- Fun `' `' F
Theorem	structfn 13046	Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.)
|- F Struct <. M , N >.   =>    |- ( Fun `' `' F /\ dom F C_ ( 1 ... N ) )
Theorem	strnfvnd 13047	Deduction version of strnfvn 13048. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 19-Jan-2023.)
|- E = Slot N   &    |- ( ph -> S e. V )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> ( E ` S ) = ( S ` N ) )
Theorem	strnfvn 13048	Value of a structure component extractor E. Normally, E is a defined constant symbol such as Base (df-base 13033) and N is a fixed integer such as 1. S 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 13072. (Contributed by NM, 9-Sep-2011.) (Revised by Jim Kingdon, 19-Jan-2023.) (New usage is discouraged.)
|- S e. _V   &    |- E = Slot N   &    |- N e. NN   =>    |- ( E ` S ) = ( S ` N )
Theorem	strfvssn 13049	A structure component extractor produces a value which is contained in a set dependent on S, but not E. This is sometimes useful for showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Jim Kingdon, 19-Jan-2023.)
|- E = Slot N   &    |- ( ph -> S e. V )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> ( E ` S ) C_ U. ran S )
Theorem	ndxarg 13050	Get the numeric argument from a defined structure component extractor such as df-base 13033. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- E = Slot N   &    |- N e. NN   =>    |- ( E ` ndx ) = N
Theorem	ndxid 13051	A structure component extractor is defined by its own index. This theorem, together with strslfv 13072 below, is useful for avoiding direct reference to the hard-coded numeric index in component extractor definitions, such as the 1 in df-base 13033, 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.)
|- E = Slot N   &    |- N e. NN   =>    |- E = Slot ( E ` ndx )
Theorem	ndxslid 13052	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 13072. (Contributed by Jim Kingdon, 29-Jan-2023.)
|- E = Slot N   &    |- N e. NN   =>    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )
Theorem	slotslfn 13053	A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by Jim Kingdon, 10-Feb-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   =>    |- E Fn _V
Theorem	slotex 13054	Existence of slot value. A corollary of slotslfn 13053. (Contributed by Jim Kingdon, 12-Feb-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   =>    |- ( A e. V -> ( E ` A ) e. _V )
Theorem	strndxid 13055	The value of a structure component extractor is the value of the corresponding slot of the structure. (Contributed by AV, 13-Mar-2020.)
|- ( ph -> S e. V )   &    |- E = Slot N   &    |- N e. NN   =>    |- ( ph -> ( S ` ( E ` ndx ) ) = ( E ` S ) )
Theorem	reldmsets 13056	The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.)
|- Rel dom sSet
Theorem	setsvalg 13057	Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.)
|- ( ( S e. V /\ A e. W ) -> ( S sSet A ) = ( ( S |` ( _V \ dom { A } ) ) u. { A } ) )
Theorem	setsvala 13058	Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 20-Jan-2023.)
|- ( ( S e. V /\ A e. X /\ B e. W ) -> ( S sSet <. A , B >. ) = ( ( S |` ( _V \ { A } ) ) u. { <. A , B >. } ) )
Theorem	setsex 13059	Applying the structure replacement function yields a set. (Contributed by Jim Kingdon, 22-Jan-2023.)
|- ( ( S e. V /\ A e. X /\ B e. W ) -> ( S sSet <. A , B >. ) e. _V )
Theorem	strsetsid 13060	Value of the structure replacement function. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- E = Slot ( E ` ndx )   &    |- ( ph -> S Struct <. M , N >. )   &    |- ( ph -> Fun S )   &    |- ( ph -> ( E ` ndx ) e. dom S )   =>    |- ( ph -> S = ( S sSet <. ( E ` ndx ) , ( E ` S ) >. ) )
Theorem	fvsetsid 13061	The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018.)
|- ( ( F e. V /\ X e. W /\ Y e. U ) -> ( ( F sSet <. X , Y >. ) ` X ) = Y )
Theorem	setsfun 13062	A structure with replacement is a function if the original structure is a function. (Contributed by AV, 7-Jun-2021.)
|- ( ( ( G e. V /\ Fun G ) /\ ( I e. U /\ E e. W ) ) -> Fun ( G sSet <. I , E >. ) )
Theorem	setsfun0 13063	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 13062 is useful for proofs based on isstruct2r 13038 which requires Fun ( F \ { (/) } ) for F to be an extensible structure. (Contributed by AV, 7-Jun-2021.)
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> Fun ( ( G sSet <. I , E >. ) \ { (/) } ) )
Theorem	setsn0fun 13064	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.)
|- ( ph -> S Struct X )   &    |- ( ph -> I e. U )   &    |- ( ph -> E e. W )   =>    |- ( ph -> Fun ( ( S sSet <. I , E >. ) \ { (/) } ) )
Theorem	setsresg 13065	The structure replacement function does not affect the value of S away from A. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 22-Jan-2023.)
|- ( ( S e. V /\ A e. W /\ B e. X ) -> ( ( S sSet <. A , B >. ) |` ( _V \ { A } ) ) = ( S |` ( _V \ { A } ) ) )
Theorem	setsabsd 13066	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.)
|- ( ph -> S e. V )   &    |- ( ph -> A e. W )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. U )   =>    |- ( ph -> ( ( S sSet <. A , B >. ) sSet <. A , C >. ) = ( S sSet <. A , C >. ) )
Theorem	setscom 13067	Different components can be set in any order. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( ( ( S e. V /\ A =/= B ) /\ ( C e. W /\ D e. X ) ) -> ( ( S sSet <. A , C >. ) sSet <. B , D >. ) = ( ( S sSet <. B , D >. ) sSet <. A , C >. ) )
Theorem	setscomd 13068	Different components can be set in any order. (Contributed by Jim Kingdon, 20-Feb-2025.)
|- ( ph -> A e. Y )   &    |- ( ph -> B e. Z )   &    |- ( ph -> S e. V )   &    |- ( ph -> A =/= B )   &    |- ( ph -> C e. W )   &    |- ( ph -> D e. X )   =>    |- ( ph -> ( ( S sSet <. A , C >. ) sSet <. B , D >. ) = ( ( S sSet <. B , D >. ) sSet <. A , C >. ) )
Theorem	strslfvd 13069	Deduction version of strslfv 13072. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( ph -> S e. V )   &    |- ( ph -> Fun S )   &    |- ( ph -> <. ( E ` ndx ) , C >. e. S )   =>    |- ( ph -> C = ( E ` S ) )
Theorem	strslfv2d 13070	Deduction version of strslfv 13072. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( ph -> S e. V )   &    |- ( ph -> Fun `' `' S )   &    |- ( ph -> <. ( E ` ndx ) , C >. e. S )   &    |- ( ph -> C e. W )   =>    |- ( ph -> C = ( E ` S ) )
Theorem	strslfv2 13071	A variation on strslfv 13072 to avoid asserting that S itself is a function, which involves sethood of all the ordered pair components of S. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- S e. _V   &    |- Fun `' `' S   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- <. ( E ` ndx ) , C >. e. S   =>    |- ( C e. V -> C = ( E ` S ) )
Theorem	strslfv 13072	Extract a structure component C (such as the base set) from a structure S with a component extractor E (such as the base set extractor df-base 13033). By virtue of ndxslid 13052, this can be done without having to refer to the hard-coded numeric index of E. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- S Struct X   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- { <. ( E ` ndx ) , C >. } C_ S   =>    |- ( C e. V -> C = ( E ` S ) )
Theorem	strslfv3 13073	Variant on strslfv 13072 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.) (Revised by Jim Kingdon, 30-Jan-2023.)
|- ( ph -> U = S )   &    |- ( ph -> S Struct X )   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( ph -> { <. ( E ` ndx ) , C >. } C_ S )   &    |- ( ph -> C e. V )   &    |- A = ( E ` U )   =>    |- ( ph -> A = C )
Theorem	strslssd 13074	Deduction version of strslss 13075. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 31-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( ph -> T e. V )   &    |- ( ph -> Fun T )   &    |- ( ph -> S C_ T )   &    |- ( ph -> <. ( E ` ndx ) , C >. e. S )   =>    |- ( ph -> ( E ` T ) = ( E ` S ) )
Theorem	strslss 13075	Propagate component extraction to a structure T from a subset structure S. (Contributed by Mario Carneiro, 11-Oct-2013.) (Revised by Jim Kingdon, 31-Jan-2023.)
|- T e. _V   &    |- Fun T   &    |- S C_ T   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- <. ( E ` ndx ) , C >. e. S   =>    |- ( E ` T ) = ( E ` S )
Theorem	strsl0 13076	All components of the empty set are empty sets. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 31-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   =>    |- (/) = ( E ` (/) )
Theorem	base0 13077	The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- (/) = ( Base ` (/) )
Theorem	setsslid 13078	Value of the structure replacement function at a replaced index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   =>    |- ( ( W e. A /\ C e. V ) -> C = ( E ` ( W sSet <. ( E ` ndx ) , C >. ) ) )
Theorem	setsslnid 13079	Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.)
|- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( E ` ndx ) =/= D   &    |- D e. NN   =>    |- ( ( W e. A /\ C e. V ) -> ( E ` W ) = ( E ` ( W sSet <. D , C >. ) ) )
Theorem	baseval 13080	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.)
|- K e. _V   =>    |- ( Base ` K ) = ( K ` 1 )
Theorem	baseid 13081	Utility theorem: index-independent form of df-base 13033. (Contributed by NM, 20-Oct-2012.)
|- Base = Slot ( Base ` ndx )
Theorem	basendx 13082	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 13081 and basendxnn 13083. 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 13192. Although we have a few theorems such as basendxnplusgndx 13153, 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 13083	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 ) e. NN
Theorem	bassetsnn 13084	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.)
|- ( ph -> S Struct X )   &    |- ( ph -> I e. NN )   &    |- ( ph -> E e. W )   &    |- ( ph -> ( Base ` ndx ) e. dom S )   =>    |- ( ph -> { ( Base ` ndx ) , I } C_ dom ( S sSet <. I , E >. ) )
Theorem	baseslid 13085	The base set extractor is a slot. (Contributed by Jim Kingdon, 31-Jan-2023.)
|- ( Base = Slot ( Base ` ndx ) /\ ( Base ` ndx ) e. NN )
Theorem	basfn 13086	The base set extractor is a function on _V. (Contributed by Stefan O'Rear, 8-Jul-2015.)
|- Base Fn _V
Theorem	basmex 13087	A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.)
|- B = ( Base ` G )   =>    |- ( A e. B -> G e. _V )
Theorem	basmexd 13088	A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 28-Nov-2024.)
|- ( ph -> B = ( Base ` G ) )   &    |- ( ph -> A e. B )   =>    |- ( ph -> G e. _V )
Theorem	basm 13089*	A structure whose base is inhabited is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.)
|- B = ( Base ` G )   =>    |- ( A e. B -> E. j j e. G )
Theorem	relelbasov 13090	Utility theorem: reverse closure for any structure defined as a two-argument function. (Contributed by Mario Carneiro, 3-Oct-2015.)
|- Rel dom O   &    |- Rel O   &    |- S = ( X O Y )   &    |- B = ( Base ` S )   =>    |- ( A e. B -> ( X e. _V /\ Y e. _V ) )
Theorem	reldmress 13091	The structure restriction is a proper operator, so it can be used with ovprc1 6037. (Contributed by Stefan O'Rear, 29-Nov-2014.)
|- Rel dom ↾s
Theorem	ressvalsets 13092	Value of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.)
|- ( ( W e. X /\ A e. Y ) -> ( W ↾s A ) = ( W sSet <. ( Base ` ndx ) , ( A i^i ( Base ` W ) ) >. ) )
Theorem	ressex 13093	Existence of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.)
|- ( ( W e. X /\ A e. Y ) -> ( W ↾s A ) e. _V )
Theorem	ressval2 13094	Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.)
|- R = ( W ↾s A )   &    |- B = ( Base ` W )   =>    |- ( ( -. B C_ A /\ W e. X /\ A e. Y ) -> R = ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) )
Theorem	ressbasd 13095	Base set of a structure restriction. (Contributed by Stefan O'Rear, 26-Nov-2014.) (Proof shortened by AV, 7-Nov-2024.)
|- ( ph -> R = ( W ↾s A ) )   &    |- ( ph -> B = ( Base ` W ) )   &    |- ( ph -> W e. X )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( A i^i B ) = ( Base ` R ) )
Theorem	ressbas2d 13096	Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- ( ph -> R = ( W ↾s A ) )   &    |- ( ph -> B = ( Base ` W ) )   &    |- ( ph -> W e. X )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> A = ( Base ` R ) )
Theorem	ressbasssd 13097	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.)
|- ( ph -> R = ( W ↾s A ) )   &    |- ( ph -> B = ( Base ` W ) )   &    |- ( ph -> W e. X )   &    |- ( ph -> A e. V )   =>    |- ( ph -> ( Base ` R ) C_ B )
Theorem	ressbasid 13098	The trivial structure restriction leaves the base set unchanged. (Contributed by Jim Kingdon, 29-Apr-2025.)
|- B = ( Base ` W )   =>    |- ( W e. V -> ( Base ` ( W ↾s B ) ) = B )
Theorem	strressid 13099	Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 17-Jan-2025.)
|- ( ph -> B = ( Base ` W ) )   &    |- ( ph -> W Struct <. M , N >. )   &    |- ( ph -> Fun W )   &    |- ( ph -> ( Base ` ndx ) e. dom W )   =>    |- ( ph -> ( W ↾s B ) = W )
Theorem	ressval3d 13100	Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 17-Jan-2025.)
|- R = ( S ↾s A )   &    |- B = ( Base ` S )   &    |- E = ( Base ` ndx )   &    |- ( ph -> S e. V )   &    |- ( ph -> Fun S )   &    |- ( ph -> E e. dom S )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> R = ( S sSet <. E , A >. ) )