Theorem psr1bas2

Description: The base set of the ring of univariate power series. (Contributed by Mario Carneiro, 3-Jul-2015)

	Ref	Expression
Hypotheses	psr1val.1	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
	psr1bas2.b	$$⊢B={\mathrm{Base}}_S$$
	psr1bas2.o	$$⊢O=1_{𝑜}\mathrm{mPwSer}R$$
Assertion	psr1bas2	$$⊢B={\mathrm{Base}}_O$$

Proof

Step	Hyp	Ref	Expression
1		psr1val.1	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
2		psr1bas2.b	$$⊢B={\mathrm{Base}}_S$$
3		psr1bas2.o	$$⊢O=1_{𝑜}\mathrm{mPwSer}R$$
4	1	psr1val	$$⊢S=\left(1_{𝑜}\mathrm{ordPwSer}R\right)\left(\varnothing \right)$$
5		0ss	$$⊢\varnothing \subseteq 1_{𝑜}\times 1_{𝑜}$$
6	5	a1i	$$⊢\top \to \varnothing \subseteq 1_{𝑜}\times 1_{𝑜}$$
7	3 4 6	opsrbas	$$⊢\top \to {\mathrm{Base}}_O={\mathrm{Base}}_S$$
8	7	mptru	$$⊢{\mathrm{Base}}_O={\mathrm{Base}}_S$$
9	2 8	eqtr4i	$$⊢B={\mathrm{Base}}_O$$