P. 130 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12901-13000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	topgrptsetd 12901	The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.)
⊢ 𝑊 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩}    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐽 = (TopSet‘𝑊))
Theorem	plendx 12902	Index value of the df-ple 12800 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.)
⊢ (le‘ndx) = ;10
Theorem	pleid 12903	Utility theorem: self-referencing, index-independent form of df-ple 12800. (Contributed by NM, 9-Nov-2012.) (Revised by AV, 9-Sep-2021.)
⊢ le = Slot (le‘ndx)
Theorem	pleslid 12904	Slot property of le. (Contributed by Jim Kingdon, 9-Feb-2023.)
⊢ (le = Slot (le‘ndx) ∧ (le‘ndx) ∈ ℕ)
Theorem	plendxnn 12905	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) ∈ ℕ
Theorem	basendxltplendx 12906	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 12907	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 12908	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 12909	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 12910	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 12911	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) ≠ ( ·𝑠 ‘ndx)
Theorem	slotsdifplendx 12912	The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.)
⊢ ((*𝑟‘ndx) ≠ (le‘ndx) ∧ (TopSet‘ndx) ≠ (le‘ndx))
Theorem	ocndx 12913	Index value of the df-ocomp 12801 slot. (Contributed by Mario Carneiro, 25-Oct-2015.) (New usage is discouraged.)
⊢ (oc‘ndx) = ;11
Theorem	ocid 12914	Utility theorem: index-independent form of df-ocomp 12801. (Contributed by Mario Carneiro, 25-Oct-2015.)
⊢ oc = Slot (oc‘ndx)
Theorem	basendxnocndx 12915	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 12916	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 12917	Index value of the df-ds 12802 slot. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (dist‘ndx) = ;12
Theorem	dsid 12918	Utility theorem: index-independent form of df-ds 12802. (Contributed by Mario Carneiro, 23-Dec-2013.)
⊢ dist = Slot (dist‘ndx)
Theorem	dsslid 12919	Slot property of dist. (Contributed by Jim Kingdon, 6-May-2023.)
⊢ (dist = Slot (dist‘ndx) ∧ (dist‘ndx) ∈ ℕ)
Theorem	dsndxnn 12920	The index of the slot for the distance in an extensible structure is a positive integer. (Contributed by AV, 28-Oct-2024.)
⊢ (dist‘ndx) ∈ ℕ
Theorem	basendxltdsndx 12921	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 12922	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 12923	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 12924	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 12925	The slots Scalar, ·𝑠 and ·𝑖 are different from the slot dist. (Contributed by AV, 29-Oct-2024.)
⊢ ((dist‘ndx) ≠ (Scalar‘ndx) ∧ (dist‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (dist‘ndx) ≠ (·𝑖‘ndx))
Theorem	dsndxntsetndx 12926	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 12927	The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.)
⊢ ((*𝑟‘ndx) ≠ (dist‘ndx) ∧ (le‘ndx) ≠ (dist‘ndx))
Theorem	unifndx 12928	Index value of the df-unif 12803 slot. (Contributed by Thierry Arnoux, 17-Dec-2017.) (New usage is discouraged.)
⊢ (UnifSet‘ndx) = ;13
Theorem	unifid 12929	Utility theorem: index-independent form of df-unif 12803. (Contributed by Thierry Arnoux, 17-Dec-2017.)
⊢ UnifSet = Slot (UnifSet‘ndx)
Theorem	unifndxnn 12930	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) ∈ ℕ
Theorem	basendxltunifndx 12931	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 12932	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 12933	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 12934	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) ∧ (*𝑟‘ndx) ≠ (UnifSet‘ndx)) ∧ ((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠ (UnifSet‘ndx)))
Theorem	homndx 12935	Index value of the df-hom 12804 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
⊢ (Hom ‘ndx) = ;14
Theorem	homid 12936	Utility theorem: index-independent form of df-hom 12804. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ Hom = Slot (Hom ‘ndx)
Theorem	homslid 12937	Slot property of Hom. (Contributed by Jim Kingdon, 20-Mar-2025.)
⊢ (Hom = Slot (Hom ‘ndx) ∧ (Hom ‘ndx) ∈ ℕ)
Theorem	ccondx 12938	Index value of the df-cco 12805 slot. (Contributed by Mario Carneiro, 7-Jan-2017.) (New usage is discouraged.)
⊢ (comp‘ndx) = ;15
Theorem	ccoid 12939	Utility theorem: index-independent form of df-cco 12805. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ comp = Slot (comp‘ndx)
Theorem	ccoslid 12940	Slot property of comp. (Contributed by Jim Kingdon, 20-Mar-2025.)
⊢ (comp = Slot (comp‘ndx) ∧ (comp‘ndx) ∈ ℕ)
6.1.3  Definition of the structure product
Syntax	crest 12941	Extend class notation with the function returning a subspace topology.
class ↾t
Syntax	ctopn 12942	Extend class notation with the topology extractor function.
class TopOpen
Definition	df-rest 12943*	Function returning the subspace topology induced by the topology 𝑦 and the set 𝑥. (Contributed by FL, 20-Sep-2010.) (Revised by Mario Carneiro, 1-May-2015.)
⊢ ↾t = (𝑗 ∈ V, 𝑥 ∈ V ↦ ran (𝑦 ∈ 𝑗 ↦ (𝑦 ∩ 𝑥)))
Definition	df-topn 12944	Define the topology extractor function. This differs from df-tset 12799 when a structure has been restricted using df-iress 12711; 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 = (𝑤 ∈ V ↦ ((TopSet‘𝑤) ↾t (Base‘𝑤)))
Theorem	restfn 12945	The subspace topology operator is a function on pairs. (Contributed by Mario Carneiro, 1-May-2015.)
⊢ ↾t Fn (V × V)
Theorem	topnfn 12946	The topology extractor function is a function on the universe. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ TopOpen Fn V
Theorem	restval 12947*	The subspace topology induced by the topology 𝐽 on the set 𝐴. (Contributed by FL, 20-Sep-2010.) (Revised by Mario Carneiro, 1-May-2015.)
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)))
Theorem	elrest 12948*	The predicate "is an open set of a subspace topology". (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (𝐽 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐽 𝐴 = (𝑥 ∩ 𝐵)))
Theorem	elrestr 12949	Sufficient condition for being an open set in a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐴 ∈ 𝐽) → (𝐴 ∩ 𝑆) ∈ (𝐽 ↾t 𝑆))
Theorem	restid2 12950	The subspace topology over a subset of the base set is the original topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐴) → (𝐽 ↾t 𝐴) = 𝐽)
Theorem	restsspw 12951	The subspace topology is a collection of subsets of the restriction set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴
Theorem	restid 12952	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.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ 𝑉 → (𝐽 ↾t 𝑋) = 𝐽)
Theorem	topnvalg 12953	Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.) (Revised by Jim Kingdon, 11-Feb-2023.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopSet‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑉 → (𝐽 ↾t 𝐵) = (TopOpen‘𝑊))
Theorem	topnidg 12954	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.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopSet‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑉 ∧ 𝐽 ⊆ 𝒫 𝐵) → 𝐽 = (TopOpen‘𝑊))
Theorem	topnpropgd 12955	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.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (TopSet‘𝐾) = (TopSet‘𝐿))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))
Syntax	ctg 12956	Extend class notation with a function that converts a basis to its corresponding topology.
class topGen
Syntax	cpt 12957	Extend class notation with a function whose value is a product topology.
class ∏t
Syntax	c0g 12958	Extend class notation with group identity element.
class 0g
Syntax	cgsu 12959	Extend class notation to include finitely supported group sums.
class Σg
Definition	df-0g 12960*	Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-igsum 12961. The related theorems will be provided later. (Contributed by NM, 20-Aug-2011.)
⊢ 0g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥))))
Definition	df-igsum 12961*	Define a finite group sum (also called "iterated sum") of a structure. Given 𝐺 Σg 𝐹 where 𝐹:𝐴⟶(Base‘𝐺), the set of indices is 𝐴 and the values are given by 𝐹 at each index. A group sum over a multiplicative group may be viewed as a product. The definition is meaningful in different contexts, depending on the size of the index set 𝐴 and each demanding different properties of 𝐺. 1. If 𝐴 = ∅ and 𝐺 has an identity element, then the sum equals this identity. 2. If 𝐴 = (𝑀...𝑁) and 𝐺 is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e., ((𝐹‘1) + (𝐹‘2)) + (𝐹‘3), etc. 3. This definition does not handle other cases. (Contributed by FL, 5-Sep-2010.) (Revised by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 27-Jun-2025.)
⊢ Σg = (𝑤 ∈ V, 𝑓 ∈ V ↦ (℩𝑥((dom 𝑓 = ∅ ∧ 𝑥 = (0g‘𝑤)) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)))))
Definition	df-topgen 12962*	Define a function that converts a basis to its corresponding topology. Equivalent to the definition of a topology generated by a basis in [Munkres] p. 78. (Contributed by NM, 16-Jul-2006.)
⊢ topGen = (𝑥 ∈ V ↦ {𝑦 ∣ 𝑦 ⊆ ∪ (𝑥 ∩ 𝒫 𝑦)})
Definition	df-pt 12963*	Define the product topology on a collection of topologies. For convenience, it is defined on arbitrary collections of sets, expressed as a function from some index set to the subbases of each factor space. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ ∏t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))}))
Theorem	tgval 12964*	The topology generated by a basis. See also tgval2 14371 and tgval3 14378. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)})
Theorem	tgvalex 12965	The topology generated by a basis is a set. (Contributed by Jim Kingdon, 4-Mar-2023.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) ∈ V)
Theorem	ptex 12966	Existence of the product topology. (Contributed by Jim Kingdon, 19-Mar-2025.)
⊢ (𝐹 ∈ 𝑉 → (∏t‘𝐹) ∈ V)
Syntax	cprds 12967	The function constructing structure products.
class Xs
Syntax	cpws 12968	The function constructing structure powers.
class ↑s
Definition	df-prds 12969*	Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ Xs = (𝑠 ∈ V, 𝑟 ∈ V ↦ ⦋X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ ((2nd ‘𝑎)ℎ𝑐), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})))
Theorem	reldmprds 12970	The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.)
⊢ Rel dom Xs
Theorem	prdsex 12971	Existence of the structure product. (Contributed by Jim Kingdon, 18-Mar-2025.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑆Xs𝑅) ∈ V)
Theorem	imasvalstrd 12972	An image structure value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝑈 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), 𝐿⟩, ⟨(dist‘ndx), 𝐷⟩})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → × ∈ 𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑍)    &   ⊢ (𝜑 → , ∈ 𝑃)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑄)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑈 Struct ⟨1, ;12⟩)
Theorem	prdsvalstrd 12973	Structure product value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → + ∈ 𝑊)    &   ⊢ (𝜑 → × ∈ 𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑌)    &   ⊢ (𝜑 → · ∈ 𝑍)    &   ⊢ (𝜑 → , ∈ 𝑃)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑄)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑅)    &   ⊢ (𝜑 → 𝐷 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑇)    &   ⊢ (𝜑 → ∙ ∈ 𝑈)    ⇒   ⊢ (𝜑 → (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), 𝐿⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})) Struct ⟨1, ;15⟩)
Theorem	prdsvallem 12974*	Lemma for prdsval 12975. (Contributed by Stefan O'Rear, 3-Jan-2015.) Extracted from the former proof of prdsval 12975, dependency on df-hom 12804 removed. (Revised by AV, 13-Oct-2024.)
⊢ (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) ∈ V
Theorem	prdsval 12975*	Value of the structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    &   ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))    &   ⊢ (𝜑 → + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))))    &   ⊢ (𝜑 → × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))))    &   ⊢ (𝜑 → · = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))    &   ⊢ (𝜑 → , = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))    &   ⊢ (𝜑 → 𝑂 = (∏t‘(TopOpen ∘ 𝑅)))    &   ⊢ (𝜑 → ≤ = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})    &   ⊢ (𝜑 → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )))    &   ⊢ (𝜑 → 𝐻 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))))    &   ⊢ (𝜑 → ∙ = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))))    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝑃 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))
Theorem	prdsbaslemss 12976	Lemma for prdsbas 12978 and similar theorems. (Contributed by Jim Kingdon, 10-Nov-2025.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐴 = (𝐸‘𝑃)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ∈ ℕ    &   ⊢ (𝜑 → 𝑇 ∈ 𝑋)    &   ⊢ (𝜑 → {⟨(𝐸‘ndx), 𝑇⟩} ⊆ 𝑃)    ⇒   ⊢ (𝜑 → 𝐴 = 𝑇)
Theorem	prdssca 12977	Scalar ring of a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝑆 = (Scalar‘𝑃))
Theorem	prdsbas 12978*	Base set of a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    ⇒   ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
Theorem	prdsplusg 12979*	Addition in a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    &   ⊢ + = (+g‘𝑃)    ⇒   ⊢ (𝜑 → + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
Theorem	prdsmulr 12980*	Multiplication in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    &   ⊢ · = (.r‘𝑃)    ⇒   ⊢ (𝜑 → · = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
Theorem	prdsbas2 12981*	The base set of a structure product is an indexed set product. (Contributed by Stefan O'Rear, 10-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    ⇒   ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
Theorem	prdsbasmpt 12982*	A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ 𝑈) ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐼 𝑈 ∈ (Base‘(𝑅‘𝑥))))
Theorem	prdsbasfn 12983	Points in the structure product are functions; use this with dffn5im 5609 to establish equalities. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑇 Fn 𝐼)
Theorem	prdsbasprj 12984	Each point in a structure product restricts on each coordinate to the relevant base set. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑇‘𝐽) ∈ (Base‘(𝑅‘𝐽)))
Theorem	prdsplusgval 12985*	Value of a componentwise sum in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ + = (+g‘𝑌)    ⇒   ⊢ (𝜑 → (𝐹 + 𝐺) = (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)(+g‘(𝑅‘𝑥))(𝐺‘𝑥))))
Theorem	prdsplusgfval 12986	Value of a structure product sum at a single coordinate. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ + = (+g‘𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐹 + 𝐺)‘𝐽) = ((𝐹‘𝐽)(+g‘(𝑅‘𝐽))(𝐺‘𝐽)))
Theorem	prdsmulrval 12987*	Value of a componentwise ring product in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ · = (.r‘𝑌)    ⇒   ⊢ (𝜑 → (𝐹 · 𝐺) = (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)(.r‘(𝑅‘𝑥))(𝐺‘𝑥))))
Theorem	prdsmulrfval 12988	Value of a structure product's ring product at a single coordinate. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ · = (.r‘𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐹 · 𝐺)‘𝐽) = ((𝐹‘𝐽)(.r‘(𝑅‘𝐽))(𝐺‘𝐽)))
Theorem	prdsbas3 12989*	The base set of an indexed structure product. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 𝐾)
Theorem	prdsbasmpt2 12990*	A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Mario Carneiro, 3-Jul-2015.) (Revised by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ 𝑈) ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐼 𝑈 ∈ 𝐾))
Theorem	prdsbascl 12991*	An element of the base has projections closed in the factors. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝐹‘𝑥) ∈ 𝐾)
Definition	df-pws 12992*	Define a structure power, which is just a structure product where all the factors are the same. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ ↑s = (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟})))
Theorem	pwsval 12993	Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐹 = (Scalar‘𝑅)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑌 = (𝐹Xs(𝐼 × {𝑅})))
Theorem	pwsbas 12994	Base set of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐵 ↑𝑚 𝐼) = (Base‘𝑌))
Theorem	pwselbasb 12995	Membership in the base set of a structure product. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑉 = (Base‘𝑌)    ⇒   ⊢ ((𝑅 ∈ 𝑊 ∧ 𝐼 ∈ 𝑍) → (𝑋 ∈ 𝑉 ↔ 𝑋:𝐼⟶𝐵))
Theorem	pwselbas 12996	An element of a structure power is a function from the index set to the base set of the structure. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 5-Jun-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑉 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑋:𝐼⟶𝐵)
Theorem	pwsplusgval 12997	Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = (+g‘𝑌)    ⇒   ⊢ (𝜑 → (𝐹 ✚ 𝐺) = (𝐹 ∘𝑓 + 𝐺))
Theorem	pwsmulrval 12998	Value of multiplication in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑌)    ⇒   ⊢ (𝜑 → (𝐹 ∙ 𝐺) = (𝐹 ∘𝑓 · 𝐺))
Theorem	pwsdiagel 12999	Membership of diagonal elements in the structure power base set. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑌)    ⇒   ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝐴 ∈ 𝐵) → (𝐼 × {𝐴}) ∈ 𝐶)
Theorem	pwssnf1o 13000*	Triviality of singleton powers: set equipollence. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s {𝐼})    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ({𝐼} × {𝑥}))    &   ⊢ 𝐶 = (Base‘𝑌)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵–1-1-onto→𝐶)