Theorem opsrbas

Description: The base set of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 30-Aug-2015) (Revised by AV, 1-Nov-2024)

	Ref	Expression
Hypotheses	opsrbas.s	$$⊢S=I\mathrm{mPwSer}R$$
	opsrbas.o	$$⊢O=\left(I\mathrm{ordPwSer}R\right)\left(T\right)$$
	opsrbas.t	$$⊢\phi \to T\subseteq I\times I$$
Assertion	opsrbas	$$⊢\phi \to {\mathrm{Base}}_S={\mathrm{Base}}_O$$

Proof

Step	Hyp	Ref	Expression
1		opsrbas.s	$$⊢S=I\mathrm{mPwSer}R$$
2		opsrbas.o	$$⊢O=\left(I\mathrm{ordPwSer}R\right)\left(T\right)$$
3		opsrbas.t	$$⊢\phi \to T\subseteq I\times I$$
4		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
5		plendxnbasendx	$$⊢{\le }_{\mathrm{ndx}}\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
6	5	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}$$
7	1 2 3 4 6	opsrbaslem	$$⊢\phi \to {\mathrm{Base}}_S={\mathrm{Base}}_O$$