Theorem psr1bas

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

	Ref	Expression
Hypotheses	psr1val.1	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
	psr1bas2.b	$$⊢B={\mathrm{Base}}_S$$
	psr1bas.k	$$⊢K={\mathrm{Base}}_R$$
Assertion	psr1bas	$$⊢B=K^{\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)}$$

Proof

Step	Hyp	Ref	Expression
1		psr1val.1	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
2		psr1bas2.b	$$⊢B={\mathrm{Base}}_S$$
3		psr1bas.k	$$⊢K={\mathrm{Base}}_R$$
4		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}R=1_{𝑜}\mathrm{mPwSer}R$$
5		psr1baslem	$$⊢{{\mathbb{N}}_0}^{1_{𝑜}}=\left\{f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
6	1 2 4	psr1bas2	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
7		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
8	7	a1i	$$⊢\top \to 1_{𝑜}\in \mathrm{On}$$
9	4 3 5 6 8	psrbas	$$⊢\top \to B=K^{\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)}$$
10	9	mptru	$$⊢B=K^{\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)}$$