P. 134 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13301-13400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	scandxnplusgndx 13301	The slot for the scalar field is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|- (Scalar ` ndx ) =/= ( +g ` ndx )
Theorem	scandxnmulrndx 13302	The slot for the scalar field is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)
|- (Scalar ` ndx ) =/= ( .r ` ndx )
Theorem	vscandx 13303	Index value of the df-vsca 13240 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .s ` ndx ) = 6
Theorem	vscaid 13304	Utility theorem: index-independent form of scalar product df-vsca 13240. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- .s = Slot ( .s ` ndx )
Theorem	vscandxnbasendx 13305	The slot for the scalar product is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|- ( .s ` ndx ) =/= ( Base ` ndx )
Theorem	vscandxnplusgndx 13306	The slot for the scalar product is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|- ( .s ` ndx ) =/= ( +g ` ndx )
Theorem	vscandxnmulrndx 13307	The slot for the scalar product is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)
|- ( .s ` ndx ) =/= ( .r ` ndx )
Theorem	vscandxnscandx 13308	The slot for the scalar product is not the slot for the scalar field in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|- ( .s ` ndx ) =/= (Scalar ` ndx )
Theorem	vscaslid 13309	Slot property of .s. (Contributed by Jim Kingdon, 5-Feb-2023.)
|- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
Theorem	lmodstrd 13310	A constructed left module or left vector space is a structure. (Contributed by Mario Carneiro, 1-Oct-2013.) (Revised by Jim Kingdon, 5-Feb-2023.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. X )   &    |- ( ph -> F e. Y )   &    |- ( ph -> .x. e. Z )   =>    |- ( ph -> W Struct <. 1 , 6 >. )
Theorem	lmodbased 13311	The base set of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. X )   &    |- ( ph -> F e. Y )   &    |- ( ph -> .x. e. Z )   =>    |- ( ph -> B = ( Base ` W ) )
Theorem	lmodplusgd 13312	The additive operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. X )   &    |- ( ph -> F e. Y )   &    |- ( ph -> .x. e. Z )   =>    |- ( ph -> .+ = ( +g ` W ) )
Theorem	lmodscad 13313	The set of scalars of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. X )   &    |- ( ph -> F e. Y )   &    |- ( ph -> .x. e. Z )   =>    |- ( ph -> F = (Scalar ` W ) )
Theorem	lmodvscad 13314	The scalar product operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 7-Feb-2023.)
|- W = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , F >. } u. { <. ( .s ` ndx ) , .x. >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. X )   &    |- ( ph -> F e. Y )   &    |- ( ph -> .x. e. Z )   =>    |- ( ph -> .x. = ( .s ` W ) )
Theorem	ipndx 13315	Index value of the df-ip 13241 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( .i ` ndx ) = 8
Theorem	ipid 13316	Utility theorem: index-independent form of df-ip 13241. (Contributed by Mario Carneiro, 6-Oct-2013.)
|- .i = Slot ( .i ` ndx )
Theorem	ipslid 13317	Slot property of .i. (Contributed by Jim Kingdon, 7-Feb-2023.)
|- ( .i = Slot ( .i ` ndx ) /\ ( .i ` ndx ) e. NN )
Theorem	ipndxnbasendx 13318	The slot for the inner product is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.)
|- ( .i ` ndx ) =/= ( Base ` ndx )
Theorem	ipndxnplusgndx 13319	The slot for the inner product is not the slot for the group operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)
|- ( .i ` ndx ) =/= ( +g ` ndx )
Theorem	ipndxnmulrndx 13320	The slot for the inner product is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)
|- ( .i ` ndx ) =/= ( .r ` ndx )
Theorem	slotsdifipndx 13321	The slot for the scalar is not the index of other slots. (Contributed by AV, 12-Nov-2024.)
|- ( ( .s ` ndx ) =/= ( .i ` ndx ) /\ (Scalar ` ndx ) =/= ( .i ` ndx ) )
Theorem	ipsstrd 13322	A constructed inner product space is a structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Q )   &    |- ( ph -> I e. Z )   =>    |- ( ph -> A Struct <. 1 , 8 >. )
Theorem	ipsbased 13323	The base set of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Q )   &    |- ( ph -> I e. Z )   =>    |- ( ph -> B = ( Base ` A ) )
Theorem	ipsaddgd 13324	The additive operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Q )   &    |- ( ph -> I e. Z )   =>    |- ( ph -> .+ = ( +g ` A ) )
Theorem	ipsmulrd 13325	The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Q )   &    |- ( ph -> I e. Z )   =>    |- ( ph -> .X. = ( .r ` A ) )
Theorem	ipsscad 13326	The set of scalars of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 8-Feb-2023.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Q )   &    |- ( ph -> I e. Z )   =>    |- ( ph -> S = (Scalar ` A ) )
Theorem	ipsvscad 13327	The scalar product operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 8-Feb-2023.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Q )   &    |- ( ph -> I e. Z )   =>    |- ( ph -> .x. = ( .s ` A ) )
Theorem	ipsipd 13328	The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 8-Feb-2023.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } )   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> .X. e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> .x. e. Q )   &    |- ( ph -> I e. Z )   =>    |- ( ph -> I = ( .i ` A ) )
Theorem	ressscag 13329	Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- H = ( G ↾s A )   &    |- F = (Scalar ` G )   =>    |- ( ( G e. X /\ A e. V ) -> F = (Scalar ` H ) )
Theorem	ressvscag 13330	.s is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- H = ( G ↾s A )   &    |- .x. = ( .s ` G )   =>    |- ( ( G e. X /\ A e. V ) -> .x. = ( .s ` H ) )
Theorem	ressipg 13331	The inner product is unaffected by restriction. (Contributed by Thierry Arnoux, 16-Jun-2019.)
|- H = ( G ↾s A )   &    |- ., = ( .i ` G )   =>    |- ( ( G e. X /\ A e. V ) -> ., = ( .i ` H ) )
Theorem	tsetndx 13332	Index value of the df-tset 13242 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (TopSet ` ndx ) = 9
Theorem	tsetid 13333	Utility theorem: index-independent form of df-tset 13242. (Contributed by NM, 20-Oct-2012.)
|- TopSet = Slot (TopSet ` ndx )
Theorem	tsetslid 13334	Slot property of TopSet. (Contributed by Jim Kingdon, 9-Feb-2023.)
|- (TopSet = Slot (TopSet ` ndx ) /\ (TopSet ` ndx ) e. NN )
Theorem	tsetndxnn 13335	The index of the slot for the group operation in an extensible structure is a positive integer. (Contributed by AV, 31-Oct-2024.)
|- (TopSet ` ndx ) e. NN
Theorem	basendxlttsetndx 13336	The index of the slot for the base set is less then the index of the slot for the topology in an extensible structure. (Contributed by AV, 31-Oct-2024.)
|- ( Base ` ndx ) < (TopSet ` ndx )
Theorem	tsetndxnbasendx 13337	The slot for the topology is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 31-Oct-2024.)
|- (TopSet ` ndx ) =/= ( Base ` ndx )
Theorem	tsetndxnplusgndx 13338	The slot for the topology is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|- (TopSet ` ndx ) =/= ( +g ` ndx )
Theorem	tsetndxnmulrndx 13339	The slot for the topology is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.)
|- (TopSet ` ndx ) =/= ( .r ` ndx )
Theorem	tsetndxnstarvndx 13340	The slot for the topology is not the slot for the involution in an extensible structure. (Contributed by AV, 11-Nov-2024.)
|- (TopSet ` ndx ) =/= ( *r ` ndx )
Theorem	slotstnscsi 13341	The slots Scalar, .s and .i are different from the slot TopSet. (Contributed by AV, 29-Oct-2024.)
|- ( (TopSet ` ndx ) =/= (Scalar ` ndx ) /\ (TopSet ` ndx ) =/= ( .s ` ndx ) /\ (TopSet ` ndx ) =/= ( .i ` ndx ) )
Theorem	topgrpstrd 13342	A constructed topological group is a structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
|- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (TopSet ` ndx ) , J >. }   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> J e. X )   =>    |- ( ph -> W Struct <. 1 , 9 >. )
Theorem	topgrpbasd 13343	The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
|- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (TopSet ` ndx ) , J >. }   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> J e. X )   =>    |- ( ph -> B = ( Base ` W ) )
Theorem	topgrpplusgd 13344	The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
|- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (TopSet ` ndx ) , J >. }   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> J e. X )   =>    |- ( ph -> .+ = ( +g ` W ) )
Theorem	topgrptsetd 13345	The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
|- W = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. (TopSet ` ndx ) , J >. }   &    |- ( ph -> B e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> J e. X )   =>    |- ( ph -> J = (TopSet ` W ) )
Theorem	plendx 13346	Index value of the df-ple 13243 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
|- ( le ` ndx ) = ; 1 0
Theorem	pleid 13347	Utility theorem: self-referencing, index-independent form of df-ple 13243. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.)
|- le = Slot ( le ` ndx )
Theorem	pleslid 13348	Slot property of le. (Contributed by Jim Kingdon, 9-Feb-2023.)
|- ( le = Slot ( le ` ndx ) /\ ( le ` ndx ) e. NN )
Theorem	plendxnn 13349	The index value of the order slot 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, 30-Oct-2024.)
|- ( le ` ndx ) e. NN
Theorem	basendxltplendx 13350	The index value of the Base slot is less than the index value of the le slot. (Contributed by AV, 30-Oct-2024.)
|- ( Base ` ndx ) < ( le ` ndx )
Theorem	plendxnbasendx 13351	The slot for the order is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 30-Oct-2024.)
|- ( le ` ndx ) =/= ( Base ` ndx )
Theorem	plendxnplusgndx 13352	The slot for the "less than or equal to" ordering is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|- ( le ` ndx ) =/= ( +g ` ndx )
Theorem	plendxnmulrndx 13353	The slot for the "less than or equal to" ordering is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 1-Nov-2024.)
|- ( le ` ndx ) =/= ( .r ` ndx )
Theorem	plendxnscandx 13354	The slot for the "less than or equal to" ordering is not the slot for the scalar in an extensible structure. (Contributed by AV, 1-Nov-2024.)
|- ( le ` ndx ) =/= (Scalar ` ndx )
Theorem	plendxnvscandx 13355	The slot for the "less than or equal to" ordering is not the slot for the scalar product in an extensible structure. (Contributed by AV, 1-Nov-2024.)
|- ( le ` ndx ) =/= ( .s ` ndx )
Theorem	slotsdifplendx 13356	The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.)
|- ( ( *r ` ndx ) =/= ( le ` ndx ) /\ (TopSet ` ndx ) =/= ( le ` ndx ) )
Theorem	ocndx 13357	Index value of the df-ocomp 13244 slot. (Contributed by Mario Carneiro, 25-Oct-2015.) (New usage is discouraged.)
|- ( oc ` ndx ) = ; 1 1
Theorem	ocid 13358	Utility theorem: index-independent form of df-ocomp 13244. (Contributed by Mario Carneiro, 25-Oct-2015.)
|- oc = Slot ( oc ` ndx )
Theorem	basendxnocndx 13359	The slot for the orthocomplementation is not the slot for the base set in an extensible structure. (Contributed by AV, 11-Nov-2024.)
|- ( Base ` ndx ) =/= ( oc ` ndx )
Theorem	plendxnocndx 13360	The slot for the orthocomplementation is not the slot for the order in an extensible structure. (Contributed by AV, 11-Nov-2024.)
|- ( le ` ndx ) =/= ( oc ` ndx )
Theorem	dsndx 13361	Index value of the df-ds 13245 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( dist ` ndx ) = ; 1 2
Theorem	dsid 13362	Utility theorem: index-independent form of df-ds 13245. (Contributed by Mario Carneiro, 23-Dec-2013.)
|- dist = Slot ( dist ` ndx )
Theorem	dsslid 13363	Slot property of dist. (Contributed by Jim Kingdon, 6-May-2023.)
|- ( dist = Slot ( dist ` ndx ) /\ ( dist ` ndx ) e. NN )
Theorem	dsndxnn 13364	The index of the slot for the distance in an extensible structure is a positive integer. (Contributed by AV, 28-Oct-2024.)
|- ( dist ` ndx ) e. NN
Theorem	basendxltdsndx 13365	The index of the slot for the base set is less then the index of the slot for the distance in an extensible structure. (Contributed by AV, 28-Oct-2024.)
|- ( Base ` ndx ) < ( dist ` ndx )
Theorem	dsndxnbasendx 13366	The slot for the distance is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 28-Oct-2024.)
|- ( dist ` ndx ) =/= ( Base ` ndx )
Theorem	dsndxnplusgndx 13367	The slot for the distance function is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|- ( dist ` ndx ) =/= ( +g ` ndx )
Theorem	dsndxnmulrndx 13368	The slot for the distance function is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.)
|- ( dist ` ndx ) =/= ( .r ` ndx )
Theorem	slotsdnscsi 13369	The slots Scalar, .s and .i are different from the slot dist. (Contributed by AV, 29-Oct-2024.)
|- ( ( dist ` ndx ) =/= (Scalar ` ndx ) /\ ( dist ` ndx ) =/= ( .s ` ndx ) /\ ( dist ` ndx ) =/= ( .i ` ndx ) )
Theorem	dsndxntsetndx 13370	The slot for the distance function is not the slot for the topology in an extensible structure. (Contributed by AV, 29-Oct-2024.)
|- ( dist ` ndx ) =/= (TopSet ` ndx )
Theorem	slotsdifdsndx 13371	The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.)
|- ( ( *r ` ndx ) =/= ( dist ` ndx ) /\ ( le ` ndx ) =/= ( dist ` ndx ) )
Theorem	unifndx 13372	Index value of the df-unif 13246 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) (New usage is discouraged.)
|- ( UnifSet ` ndx ) = ; 1 3
Theorem	unifid 13373	Utility theorem: index-independent form of df-unif 13246. (Contributed by Thierry Arnoux, 17-Dec-2017.)
|- UnifSet = Slot ( UnifSet ` ndx )
Theorem	unifndxnn 13374	The index of the slot for the uniform set in an extensible structure is a positive integer. (Contributed by AV, 28-Oct-2024.)
|- ( UnifSet ` ndx ) e. NN
Theorem	basendxltunifndx 13375	The index of the slot for the base set is less then the index of the slot for the uniform set in an extensible structure. (Contributed by AV, 28-Oct-2024.)
|- ( Base ` ndx ) < ( UnifSet ` ndx )
Theorem	unifndxnbasendx 13376	The slot for the uniform set is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.)
|- ( UnifSet ` ndx ) =/= ( Base ` ndx )
Theorem	unifndxntsetndx 13377	The slot for the uniform set is not the slot for the topology in an extensible structure. (Contributed by AV, 28-Oct-2024.)
|- ( UnifSet ` ndx ) =/= (TopSet ` ndx )
Theorem	slotsdifunifndx 13378	The index of the slot for the uniform set is not the index of other slots. (Contributed by AV, 10-Nov-2024.)
|- ( ( ( +g ` ndx ) =/= ( UnifSet ` ndx ) /\ ( .r ` ndx ) =/= ( UnifSet ` ndx ) /\ ( *r ` ndx ) =/= ( UnifSet ` ndx ) ) /\ ( ( le ` ndx ) =/= ( UnifSet ` ndx ) /\ ( dist ` ndx ) =/= ( UnifSet ` ndx ) ) )
Theorem	homndx 13379	Index value of the df-hom 13247 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
|- ( Hom ` ndx ) = ; 1 4
Theorem	homid 13380	Utility theorem: index-independent form of df-hom 13247. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- Hom = Slot ( Hom ` ndx )
Theorem	homslid 13381	Slot property of Hom. (Contributed by Jim Kingdon, 20-Mar-2025.)
|- ( Hom = Slot ( Hom ` ndx ) /\ ( Hom ` ndx ) e. NN )
Theorem	ccondx 13382	Index value of the df-cco 13248 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
|- (comp ` ndx ) = ; 1 5
Theorem	ccoid 13383	Utility theorem: index-independent form of df-cco 13248. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- comp = Slot (comp ` ndx )
Theorem	ccoslid 13384	Slot property of comp. (Contributed by Jim Kingdon, 20-Mar-2025.)
|- (comp = Slot (comp ` ndx ) /\ (comp ` ndx ) e. NN )
6.1.3  Definition of the structure product
Syntax	crest 13385	Extend class notation with the function returning a subspace topology.
class ↾t
Syntax	ctopn 13386	Extend class notation with the topology extractor function.
class TopOpen
Definition	df-rest 13387*	Function returning the subspace topology induced by the topology y and the set x. (Contributed by FL, 20-Sep-2010.) (Revised by Mario Carneiro, 1-May-2015.)
|- ↾t = ( j e. _V , x e. _V |-> ran ( y e. j |-> ( y i^i x ) ) )
Definition	df-topn 13388	Define the topology extractor function. This differs from df-tset 13242 when a structure has been restricted using df-iress 13153; in this case the TopSet component will still have a topology over the larger set, and this function fixes this by restricting the topology as well. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- TopOpen = ( w e. _V |-> ( (TopSet ` w ) ↾t ( Base ` w ) ) )
Theorem	restfn 13389	The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.)
|- ↾t Fn ( _V X. _V )
Theorem	topnfn 13390	The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- TopOpen Fn _V
Theorem	restval 13391*	The subspace topology induced by the topology J on the set A. (Contributed by FL, 20-Sep-2010.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( J e. V /\ A e. W ) -> ( J ↾t A ) = ran ( x e. J |-> ( x i^i A ) ) )
Theorem	elrest 13392*	The predicate "is an open set of a subspace topology". (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- ( ( J e. V /\ B e. W ) -> ( A e. ( J ↾t B ) <-> E. x e. J A = ( x i^i B ) ) )
Theorem	elrestr 13393	Sufficient condition for being an open set in a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- ( ( J e. V /\ S e. W /\ A e. J ) -> ( A i^i S ) e. ( J ↾t S ) )
Theorem	restid2 13394	The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( ( A e. V /\ J C_ ~P A ) -> ( J ↾t A ) = J )
Theorem	restsspw 13395	The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( J ↾t A ) C_ ~P A
Theorem	restid 13396	The subspace topology of the base set is the original topology. (Contributed by Jeff Hankins, 9-Jul-2009.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- X = U. J   =>    |- ( J e. V -> ( J ↾t X ) = J )
Theorem	topnvalg 13397	Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.) (Revised by Jim Kingdon, 11-Feb-2023.)
|- B = ( Base ` W )   &    |- J = (TopSet ` W )   =>    |- ( W e. V -> ( J ↾t B ) = ( TopOpen ` W ) )
Theorem	topnidg 13398	Value of the topology extractor function when the topology is defined over the same set as the base. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- B = ( Base ` W )   &    |- J = (TopSet ` W )   =>    |- ( ( W e. V /\ J C_ ~P B ) -> J = ( TopOpen ` W ) )
Theorem	topnpropgd 13399	The topology extractor function depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Jim Kingdon, 13-Feb-2023.)
|- ( ph -> ( Base ` K ) = ( Base ` L ) )   &    |- ( ph -> (TopSet ` K ) = (TopSet ` L ) )   &    |- ( ph -> K e. V )   &    |- ( ph -> L e. W )   =>    |- ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )
Syntax	ctg 13400	Extend class notation with a function that converts a basis to its corresponding topology.
class topGen