Theorem psr1bas

Description: The base set of the ring of univariate power series. (Contributed by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypotheses	psr1val.1	⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
	psr1bas2.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	psr1bas.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
Assertion	psr1bas	⊢ 𝐵 = ( 𝐾 ↑m ( ℕ0 ↑m 1o ) )

Proof

Step	Hyp	Ref	Expression
1		psr1val.1	⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
2		psr1bas2.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
3		psr1bas.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		eqid	⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
5		psr1baslem	⊢ ( ℕ0 ↑m 1o ) = { 𝑓 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
6	1 2 4	psr1bas2	⊢ 𝐵 = ( Base ‘ ( 1o mPwSer 𝑅 ) )
7		1on	⊢ 1o ∈ On
8	7	a1i	⊢ ( ⊤ → 1o ∈ On )
9	4 3 5 6 8	psrbas	⊢ ( ⊤ → 𝐵 = ( 𝐾 ↑m ( ℕ0 ↑m 1o ) ) )
10	9	mptru	⊢ 𝐵 = ( 𝐾 ↑m ( ℕ0 ↑m 1o ) )