Theorem psr1bascl

Description: A univariate power series is a multivariate power series on one index. (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Hypotheses	psr1rcl.p	⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
	psr1rcl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion	psr1bascl	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		psr1rcl.p	⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
2		psr1rcl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		id	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ 𝐵 )
4		eqid	⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
5	1 2 4	psr1bas2	⊢ 𝐵 = ( Base ‘ ( 1o mPwSer 𝑅 ) )
6	3 5	eleqtrdi	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) )