Theorem vr1cl2

Description: The variable X is a member of the power series algebra R [ [ X ] ] . (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypotheses	vr1val.1	|- X = ( var1 ` R )
	vr1cl2.2	|- S = ( PwSer1 ` R )
	vr1cl2.3	|- B = ( Base ` S )
Assertion	vr1cl2	|- ( R e. Ring -> X e. B )

Proof

Step	Hyp	Ref	Expression
1		vr1val.1	|- X = ( var1 ` R )
2		vr1cl2.2	|- S = ( PwSer1 ` R )
3		vr1cl2.3	|- B = ( Base ` S )
4	1	vr1val	|- X = ( ( 1o mVar R ) ` (/) )
5		eqid	|- ( 1o mPwSer R ) = ( 1o mPwSer R )
6		eqid	|- ( 1o mVar R ) = ( 1o mVar R )
7		eqid	|- ( Base ` ( 1o mPwSer R ) ) = ( Base ` ( 1o mPwSer R ) )
8		1on	|- 1o e. On
9	8	a1i	|- ( R e. Ring -> 1o e. On )
10		id	|- ( R e. Ring -> R e. Ring )
11		0lt1o	|- (/) e. 1o
12	11	a1i	|- ( R e. Ring -> (/) e. 1o )
13	5 6 7 9 10 12	mvrcl2	|- ( R e. Ring -> ( ( 1o mVar R ) ` (/) ) e. ( Base ` ( 1o mPwSer R ) ) )
14	2	psr1val	|- S = ( ( 1o ordPwSer R ) ` (/) )
15		0ss	|- (/) C_ ( 1o X. 1o )
16	15	a1i	|- ( R e. Ring -> (/) C_ ( 1o X. 1o ) )
17	5 14 16	opsrbas	|- ( R e. Ring -> ( Base ` ( 1o mPwSer R ) ) = ( Base ` S ) )
18	17 3	eqtr4di	|- ( R e. Ring -> ( Base ` ( 1o mPwSer R ) ) = B )
19	13 18	eleqtrd	|- ( R e. Ring -> ( ( 1o mVar R ) ` (/) ) e. B )
20	4 19	eqeltrid	|- ( R e. Ring -> X e. B )