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	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	vr1cl2.2	⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
	vr1cl2.3	⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion	vr1cl2	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		vr1val.1	⊢ 𝑋 = ( var1 ‘ 𝑅 )
2		vr1cl2.2	⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
3		vr1cl2.3	⊢ 𝐵 = ( Base ‘ 𝑆 )
4	1	vr1val	⊢ 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )
5		eqid	⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
6		eqid	⊢ ( 1o mVar 𝑅 ) = ( 1o mVar 𝑅 )
7		eqid	⊢ ( Base ‘ ( 1o mPwSer 𝑅 ) ) = ( Base ‘ ( 1o mPwSer 𝑅 ) )
8		1on	⊢ 1o ∈ On
9	8	a1i	⊢ ( 𝑅 ∈ Ring → 1o ∈ On )
10		id	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Ring )
11		0lt1o	⊢ ∅ ∈ 1o
12	11	a1i	⊢ ( 𝑅 ∈ Ring → ∅ ∈ 1o )
13	5 6 7 9 10 12	mvrcl2	⊢ ( 𝑅 ∈ Ring → ( ( 1o mVar 𝑅 ) ‘ ∅ ) ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) )
14	2	psr1val	⊢ 𝑆 = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )
15		0ss	⊢ ∅ ⊆ ( 1o × 1o )
16	15	a1i	⊢ ( 𝑅 ∈ Ring → ∅ ⊆ ( 1o × 1o ) )
17	5 14 16	opsrbas	⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( 1o mPwSer 𝑅 ) ) = ( Base ‘ 𝑆 ) )
18	17 3	eqtr4di	⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( 1o mPwSer 𝑅 ) ) = 𝐵 )
19	13 18	eleqtrd	⊢ ( 𝑅 ∈ Ring → ( ( 1o mVar 𝑅 ) ‘ ∅ ) ∈ 𝐵 )
20	4 19	eqeltrid	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )