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	⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
	psr1bas2.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	psr1bas2.o	⊢ 𝑂 = ( 1o mPwSer 𝑅 )
Assertion	psr1bas2	⊢ 𝐵 = ( Base ‘ 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		psr1val.1	⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
2		psr1bas2.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
3		psr1bas2.o	⊢ 𝑂 = ( 1o mPwSer 𝑅 )
4	1	psr1val	⊢ 𝑆 = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )
5		0ss	⊢ ∅ ⊆ ( 1o × 1o )
6	5	a1i	⊢ ( ⊤ → ∅ ⊆ ( 1o × 1o ) )
7	3 4 6	opsrbas	⊢ ( ⊤ → ( Base ‘ 𝑂 ) = ( Base ‘ 𝑆 ) )
8	7	mptru	⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝑆 )
9	2 8	eqtr4i	⊢ 𝐵 = ( Base ‘ 𝑂 )