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 = ( PwSer1 ` R )
	psr1bas2.b	|- B = ( Base ` S )
	psr1bas2.o	|- O = ( 1o mPwSer R )
Assertion	psr1bas2	|- B = ( Base ` O )

Proof

Step	Hyp	Ref	Expression
1		psr1val.1	|- S = ( PwSer1 ` R )
2		psr1bas2.b	|- B = ( Base ` S )
3		psr1bas2.o	|- O = ( 1o mPwSer R )
4	1	psr1val	|- S = ( ( 1o ordPwSer R ) ` (/) )
5		0ss	|- (/) C_ ( 1o X. 1o )
6	5	a1i	|- ( T. -> (/) C_ ( 1o X. 1o ) )
7	3 4 6	opsrbas	|- ( T. -> ( Base ` O ) = ( Base ` S ) )
8	7	mptru	|- ( Base ` O ) = ( Base ` S )
9	2 8	eqtr4i	|- B = ( Base ` O )