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)

	Ref	Expression
Hypotheses	opsrbas.s	|- S = ( I mPwSer R )
	opsrbas.o	|- O = ( ( I ordPwSer R ) ` T )
	opsrbas.t	|- ( ph -> T C_ ( I X. I ) )
Assertion	opsrbas	|- ( ph -> ( Base ` S ) = ( Base ` O ) )

Proof

Step	Hyp	Ref	Expression
1		opsrbas.s	|- S = ( I mPwSer R )
2		opsrbas.o	|- O = ( ( I ordPwSer R ) ` T )
3		opsrbas.t	|- ( ph -> T C_ ( I X. I ) )
4		df-base	|- Base = Slot 1
5		1nn	|- 1 e. NN
6		1lt10	|- 1 < ; 1 0
7	1 2 3 4 5 6	opsrbaslem	|- ( ph -> ( Base ` S ) = ( Base ` O ) )